cadiback.cpp

// clang-format off

static const char * usage =

"usage: cadiback [ <option> ... ] [ <dimacs> [ <backbone> ] ]\n"
"\n"
"where '<option>' is one of the following:\n"
"\n"
"  -c | --check       check that backbones are really backbones\n"
"  -f | --force       force writing backbone to CNF alike path\n"
"  -h | --help        print this command line option summary\n"
"  -l | --logging     extensive logging for debugging\n"
"  -n | --no-print    do not print backbone\n"
"  -q | --quiet       disable all messages\n"
"  -r | --report      report what the SAT solver is doing\n"
"  -s | --statistics  always print full statistics (not only with '-v')\n"
"  -v | --verbose     increase verbosity (SAT solver needs three)\n"
"  -V | --version     print version and exit\n"
"\n"
"  --no-constrain     use activation literals instead of 'constrain'\n"
"  --no-filter        do not filter additional candidates\n"
"  --no-fixed         do not use root-level fixed literal information\n"
#ifndef NFLIP
"  --no-flip          do not try to find flippable candidates in models\n"
"  --really-flip      actually flip flippable candidates in models\n"
#endif
"  --no-inprocessing  disable any preprocessing and inprocessing\n"
"\n"
"  --chunking         increase constraint size by factor 10 if successful\n"
"  --cores            use core based algorithm as preprocessing step\n"
"  --one-by-one       try candidates one-by-one (do not use 'constrain')\n"
"  --set-phase        force phases to satisfy negation of candidates\n"
"\n"
"  --big              search for backbones in the BIG first\n"
"  --big-no-els       do not apply ELS to the BIG before extracting backbones\n"
"  --big-roots        only probe the roots of the ELS\n"
"\n"
"  --default          set optimization options to the default\n"
"  --plain            disable all optimizations, which is the same as:\n"
"\n"
"                       --no-filter --no-fixed"
#ifndef NFLIP
" --no-flip"
#endif
"\n"
"                       --no-inprocessing --one-by-one\n"
"\n"

"The first argument '<dimacs>' is a formula in DIMACS format for which\n"
"the backbone is determined and then printed (unless '-n' is specified).\n"
"If a second file argument '<backbone>' is given it specifies a file\n"
"to which the backbones are written.  If no file argument is given the\n"
"formula is read from '<stdin>'.  The same can be achieved by using '-'\n"
"as first argument. For reading all compressed file types supported by\n"
"'CaDiCaL' are supported.\n"

;

// clang-format on

#include <cassert>
#include <cctype>
#include <climits>
#include <cstdarg>
#include <cstdio>
#include <cstdlib>
#include <cstring>

#include <algorithm>
#include <numeric>

// Include the main 'CaDiCaL' API from 'cadical.hpp', but also some helper
// code from its library (from the 'CaDiCaL' source code directory').

#include "cadical.hpp"   // Main 'CaDiCaL' API.
#include "resources.hpp" // Get time and memory usage.
#include "signal.hpp"    // To set up a signal handler.
#include "version.hpp"   // Print 'CaDiCaL' version too.

// 'CadiBack' build information is generated by './generate'.

#include "config.hpp"

// Verbosity level: -1=quiet, 0=default, 1=verbose, INT_MAX=logging.

static int verbosity;

// Checker solver to check that backbones are really back-bones, enabled by
// '-c' or '--check' (and quite expensive but useful for debugging).
//
static const char *check;
static CaDiCaL::Solver *checker;

// Force writing to CNF alike output file.
//
static const char *force;

// Print backbones by default. Otherwise only produce statistics.
//
static const char *no_print;

// Disable by default  printing those 'c <character> ...' lines
// in the solver.  If enabled is useful to see what is going on.
//
static bool report = false;

// From command line option '-s'.
//
static bool always_print_statistics;

// Use activation literals instead of 'constrain' API call.
//
static const char *no_constrain;

// Do not filter candidates by obtained models.
//
static const char *no_filter;

#ifndef NFLIP

// There is an extension of CaDiCaL with 'bool flippable (int lit)' and
// 'bool flip (lit)' API calls which allow check whether a literal can be
// flipped in the given model without falsifying the formula.  The first
// 'flippable' function only checks this and 'flip' actually does it.
// We can use both to remove backbone candidates.
//
static const char *no_flip;     // No use of flippable information.
static const char *really_flip; // Also actually flip flippable.

#endif

// The solver can give back information about root-level fixed literals
// which can cheaply be used to remove candidates or determine backbones.
//
static const char *no_fixed;

// Disable preprocessing and inprocessing.
//
static const char *no_inprocessing;

// Force the SAT solver to assign decisions to a value which would make the
// remaining backbone candidate literals false.  This is a very natural idea
// but actual had negative effects and thus is now disabled by default.
//
static bool set_phase;

// Try each candidate after each other with a single assumption, i.e., do
// not use the 'constrain' optimization.
//
static const char *one_by_one;

// If we use constraints ('one-by-one' is off) then we might want to limit
// the size of the constraints.  On success (solver returns 'unsatisfiable')
// we increase the constraint size by factor of 10 and on failure (solver
// finds a model) we reset constraint size to '1'.
//
static const char *chunking;

// If the following option is enabled we try to compute cores as in
// 'MiniBones', which assumes the conjunction of the complement of
// all the remaining backbone candidates.  If solving under this
// assumption is satisfiable all the backbones which were assumed
// negatively are not backbones.  Otherwise if it is unsatisfiable
// (the expected case) we check the failed literal among the assumptions,
// aka the (literal) core of the query.  If that core has one element
// its negation is fixed and a backbone literal. Otherwise we remove
// from the set of assumed assumptions the core literals and try again until
// the set of assumptions becomes empty, in which case we fall back
// to the iterative algorithms.
//
static const char *cores;

// If this option is enable CadiBack will initially run our algorithm KB3 to
// search for Backbones that can be identified in the BIG (Binary
// Implication Graph) alone. This can be useful to find a (sometimes large)
// subset of backbones early on. If CadiBack is not used in an
// anytime-context this option usally doesn't yield any benefit, however it
// also usually doesn't cost much. See our FMCAD'23 paper on Big Backbones
// for a description of the algorithm and experimental resutls.
static const char *big;

// Applying ELS (Equivalent literal substitution) turns the BIG into a DAG.
// This isn't necessary for KB3 but can increase performance.
static const char *big_no_els;

// KB3 probes individual literals by propagating them in the BIG. To find
// all Backbones in the BIG it is sufficent to only probe the roots of the
// BIG. This can however have detrimental effects for KB3 and is disabled by
// default. This option requires ELS.
static const char *big_roots;

static int vars;        // The number of variables in the CNF.
static int *fixed;      // The resulting fixed backbone literals.
static int *candidates; // The backbone candidates (if non-zero).
static int *constraint; // Literals to constrain.
static int *core;       // Remaining core literals.
static char *marked;    // Flag used for ELS and BIG propagation.

// Here we have the files on which the tool operators. The first file
// argument is the '<dimacs>' if specified. Otherwise we will use '<stdin>'.
// If a second argument is specified we write the backbones to that file
// instead of printing them on '<stdout>'.

struct {
  struct {
    bool close;
    FILE *file;
    const char *path;
  } dimacs, backbone;
} files;

// The actual incrementally used solver for backbone computation is a global
// variable such that it can be accessed by the signal handler to print
// statistics even if execution is interrupted or an error occurs.
//
static CaDiCaL::Solver *solver;

// Some statistics are collected here.

static struct {
  size_t backbones;     // Number of backbones found.
  size_t dropped;       // Number of non-backbones found.
  size_t filtered;      // Number of candidates with two models.
  size_t checked;       // How often checked model or backbone.
  size_t fixed;         // Number of fixed variables.
  size_t failed;        // Failed literals during core based approach.
  size_t core;          // Set by core based approach.
  size_t big_backbones; // Number of backbones found.
  struct {
    size_t sat;     // Calls with result SAT to SAT solver.
    size_t unsat;   // Calls with result UNSAT to SAT solver.
    size_t unknown; // Interrupted solver calls.
    size_t total;   // Calls to SAT solver.
  } calls;
#ifndef NFLIP
  size_t flipped;   // How often 'solver->flip (lit)' succeeded.
  size_t flippable; // How often 'solver->flip (lit)' succeeded.
#endif
} statistics;

// Some time profiling information is collected here.

static double first_time, sat_time, unsat_time, solving_time, unknown_time;
static double satmax_time, unsatmax_time, flip_time, check_time;
static double big_search_time, big_read_time, big_els_time, big_check_time,
    big_extension_time;
static volatile double *started, start_time;

// Declaring these with '__attribute__ ...' gives nice warnings.

static void die (const char *, ...) __attribute__ ((format (printf, 1, 2)));
static void msg (const char *, ...) __attribute__ ((format (printf, 1, 2)));

static void fatal (const char *, ...)
    __attribute__ ((format (printf, 1, 2)));

// Actual message printing code starts here.

static void msg (const char *fmt, ...) {
  if (verbosity < 0)
    return;
  fputs ("c ", stdout);
  va_list ap;
  va_start (ap, fmt);
  vprintf (fmt, ap);
  va_end (ap);
  fputc ('\n', stdout);
  fflush (stdout);
}

static void line () {
  if (verbosity < 0)
    return;
  fputs ("c\n", stdout);
  fflush (stdout);
}

static void die (const char *fmt, ...) {
  fputs ("cadiback: error: ", stderr);
  va_list ap;
  va_start (ap, fmt);
  vfprintf (stderr, fmt, ap);
  va_end (ap);
  fputc ('\n', stderr);
  exit (1);
}

static void dbg (const char *fmt, ...) {
  if (verbosity < INT_MAX)
    return;
  fputs ("c CADIBACK ", stdout);
  va_list ap;
  va_start (ap, fmt);
  vprintf (fmt, ap);
  va_end (ap);
  fputc ('\n', stdout);
  fflush (stdout);
}

static void fatal (const char *fmt, ...) {
  fputs ("cadiback: fatal error: ", stderr);
  va_list ap;
  va_start (ap, fmt);
  vfprintf (stderr, fmt, ap);
  va_end (ap);
  fputc ('\n', stderr);
  fflush (stderr);
  abort ();
}

static double average (double a, double b) { return b ? a / b : 0; }
static double percent (double a, double b) { return average (100 * a, b); }

static double time () { return CaDiCaL::absolute_process_time (); }

static void start_timer (double *timer) {
  assert (!started);
  start_time = time ();
  started = timer;
}

static double stop_timer () {
  assert (started);
  double *timer = (double *) started;
  started = 0;
  double end = time ();
  double delta = end - start_time;
  *timer += delta;
  return delta;
}

static void print_statistics () {
  if (verbosity < 0)
    return;
  solver->prefix ("c ");
  double total_time = time ();
  volatile double *timer = started;
  if (started) {
    double delta = stop_timer ();
    if (timer == &solving_time) {
      statistics.calls.unknown++;
      unknown_time += delta;
    }
  }
  printf ("c\n");
  printf ("c --- [ backbone statistics ] ");
  printf ("------------------------------------------------\n");
  printf ("c\n");
  printf ("c found         %9zu backbones     %3.0f%%\n",
          statistics.backbones, percent (statistics.backbones, vars));
  printf ("c dropped       %9zu candidates    %3.0f%%\n",
          statistics.dropped, percent (statistics.dropped, vars));
  printf ("c\n");
  printf ("c filtered      %9zu candidates    %3.0f%%\n",
          statistics.filtered, percent (statistics.filtered, vars));
#ifndef NFLIP
  printf ("c flippable     %9zu candidates    %3.0f%%\n",
          statistics.flippable, percent (statistics.flippable, vars));
  printf ("c flipped       %9zu candidates    %3.0f%%\n",
          statistics.flipped, percent (statistics.flipped, vars));
#endif
  printf ("c fixed         %9zu candidates    %3.0f%%\n", statistics.fixed,
          percent (statistics.fixed, vars));
  printf ("c core          %9zu candidates    %3.0f%%\n", statistics.core,
          percent (statistics.core, vars));
  printf ("c found         %9zu big_backbone %3.0f%%\n",
          statistics.big_backbones,
          percent (statistics.big_backbones, statistics.backbones));
  printf ("c failed        %9zu candidates    %3.0f%%\n", statistics.failed,
          percent (statistics.failed, vars));
  printf ("c\n");
  printf ("c called solver %9zu times         %3.0f%%\n",
          statistics.calls.total,
          percent (statistics.calls.total, vars + 1));
  printf ("c satisfiable   %9zu times         %3.0f%%\n",
          statistics.calls.sat,
          percent (statistics.calls.sat, statistics.calls.total));
  printf ("c unsatisfiable %9zu times         %3.0f%%\n",
          statistics.calls.unsat,
          percent (statistics.calls.unsat, statistics.calls.total));
  printf ("c\n");
  printf ("c --- [ backbone profiling ] ");
  printf ("-------------------------------------------------\n");
  printf ("c\n");
  if (always_print_statistics || verbosity > 0 || first_time)
    printf ("c   %10.2f %6.2f %% first\n", first_time,
            percent (first_time, total_time));
  if (verbosity > 0 || sat_time)
    printf ("c   %10.2f %6.2f %% sat\n", sat_time,
            percent (sat_time, total_time));
  if (verbosity > 0 || unsat_time)
    printf ("c   %10.2f %6.2f %% unsat\n", unsat_time,
            percent (unsat_time, total_time));
  if (verbosity > 0 || satmax_time)
    printf ("c   %10.2f %6.2f %% satmax\n", satmax_time,
            percent (satmax_time, total_time));
  if (verbosity > 0 || unsatmax_time)
    printf ("c   %10.2f %6.2f %% unsatmax\n", unsatmax_time,
            percent (unsatmax_time, total_time));
  if (verbosity > 0 || unknown_time)
    printf ("c   %10.2f %6.2f %% unknown\n", unknown_time,
            percent (unknown_time, total_time));
  if (verbosity > 0 || solving_time)
    printf ("c   %10.2f %6.2f %% solving\n", solving_time,
            percent (solving_time, total_time));
  if (verbosity > 0 || flip_time)
    printf ("c   %10.2f %6.2f %% flip\n", flip_time,
            percent (flip_time, total_time));

  if (big && (verbosity > 0 || big_read_time))
    printf ("c   %10.2f %6.2f %% big_read\n", big_read_time,
            percent (big_read_time, total_time));
  if (big && (verbosity > 0 || big_els_time))
    printf ("c   %10.2f %6.2f %% big_no_els\n", big_els_time,
            percent (big_els_time, total_time));
  if (big && (verbosity > 0 || big_search_time))
    printf ("c   %10.2f %6.2f %% big_search\n", big_search_time,
            percent (big_search_time, total_time));
  if (big && (verbosity > 0 || big_extension_time))
    printf ("c   %10.2f %6.2f %% big_extension\n", big_extension_time,
            percent (big_extension_time, total_time));
  if (big && (verbosity > 0 || big_check_time))
    printf ("c   %10.2f %6.2f %% big_check\n", big_check_time,
            percent (big_check_time, total_time));

  if (verbosity > 0 || check_time)
    printf ("c   %10.2f %6.2f %% check\n", check_time,
            percent (check_time, total_time));
  printf ("c ====================================\n");
  printf ("c   %10.2f 100.00 %% total\n", total_time);
  printf ("c\n");
  printf ("c\n");
  fflush (stdout);
  if (!solver)
    return;
  if (always_print_statistics || verbosity > 0)
    solver->statistics ();
  solver->resources ();
}

class CadiBackSignalHandler : public CaDiCaL::Handler {
  virtual void catch_signal (int sig) {
    if (verbosity < 0)
      return;
    printf ("c caught signal %d\n", sig);
    print_statistics ();
  }
};

static int remaining_candidates () {
  size_t determined = statistics.dropped + statistics.backbones;
  assert (determined <= (size_t) vars);
  return vars - determined;
}

// Provide a wrapper function for calling the main solver.

static int solve () {
  assert (solver);
  start_timer (&solving_time);
  statistics.calls.total++;
  {
    char prefix[32];
    snprintf (prefix, sizeof prefix, "c #%zu ", statistics.calls.total);
    solver->prefix (prefix);
  }
  int remain = remaining_candidates ();
  if (report || verbosity > 1) {
    line ();
    msg ("---- [ "
         "SAT solver call #%zu (%d candidates remain %.0f%%)"
         " ] ----",
         statistics.calls.total, remain, percent (remain, vars));
    line ();
  } else if (verbosity > 0)
    msg ("SAT solver call %zu (%d candidates remain %0.f%%)",
         statistics.calls.total, remain, percent (remain, vars));
  int res = solver->solve ();
  if (res == 10) {
    statistics.calls.sat++;
  } else {
    assert (res == 20);
    statistics.calls.unsat++;
  }
  double delta = stop_timer ();
  if (statistics.calls.total == 1)
    first_time = delta;
  if (res == 10) {
    sat_time += delta;
    if (delta > satmax_time)
      satmax_time = delta;
  } else {
    unsat_time += delta;
    if (delta > unsatmax_time)
      unsatmax_time = delta;
  }
  return res;
}

// If 'check' is set (through '-c' or '--check') then we check all literals
// to either be a backbone literal or that they have a model.  The cost for
// doing this is expensive and needs one call to the checker SAT solver for
// each literal.  The checker solver is copied from the main incremental
// solver after parsing. The first model of the main solver is not checked.

static void inc_checked () {
  assert (checker);
  statistics.checked++;
  char prefix[32];
  snprintf (prefix, sizeof prefix, "c C%zu ", statistics.checked);
  checker->prefix (prefix);
}

static void check_model (int lit) {
  double *timer = (double *) started;
  if (timer)
    stop_timer ();
  start_timer (&check_time);
  inc_checked ();
  dbg ("checking that there is a model with %d", lit);
  checker->assume (lit);
  int tmp = checker->solve ();
  if (tmp != 10)
    fatal ("checking claimed model for %d failed", lit);
  stop_timer ();
  if (timer)
    start_timer (timer);
}

static void check_backbone (int lit) {
  start_timer (&check_time);
  inc_checked ();
  dbg ("checking that there is no model with %d", -lit);
  checker->assume (-lit);
  int tmp = checker->solve ();
  if (tmp != 20)
    fatal ("checking %d backbone failed", -lit);
  stop_timer ();
}

// The given variable was proven not be a backbone variable.

static void drop_candidate (int idx) {
  int lit = candidates[idx];
  dbg ("dropping candidate literal %d", lit);
  assert (lit);
  candidates[idx] = 0;
  assert (!fixed[idx]);
  assert (statistics.dropped < (size_t) vars);
  statistics.dropped++;
  if (set_phase)
    solver->unphase (idx);
  if (check)
    check_model (-lit);
}

#ifndef NFLIP

// This is a technique first implemented in 'Kitten' for SAT sweeping within
// 'Kissat', which checks whether it is possible to flip the value of a
// literal in a model of the formula without making the formula false.  It
// goes over the watches of the literal and checks if all watched clauses
// are double satisfied.

// This requires support by 'CaDiCaL' via the 'bool flippable (int lit)' or
// 'bool flip (int lit)' functions function, which is slightly more
// expensive than the one in 'Kitten' as in essence it is compatible with
// blocking literals (used in 'CaDiCaL' but not in 'Kitten').  The first
// check for flipping a literal will need to propagate all the assigned
// literals and find replacement watches while ignoring blocking literals.

// We check all remaining backbone candidate literals until none can be
// flipped anymore.  This optimization pays off if on average close to one
// literal can be flipped but still is pretty cheap if not.

// As only more recent versions of CaDiCaL (starting with '1.5.4-rc.2')
// support flipping we keep it under compile time control too (beside
// allowing to disable it during run-time).

static void try_to_flip_remaining (int start) {

  if (no_flip)
    return;

  start_timer (&flip_time);

  for (int idx = start; idx <= vars; idx++) {
    int lit = candidates[idx];
    if (!lit)
      continue;
    if (really_flip) {
      if (!solver->flip (lit))
        continue;
      dbg ("flipped literal %d", lit);
      statistics.flipped++;
    } else {
      if (!solver->flippable (lit))
        continue;
      dbg ("literal %d can be flipped", lit);
      statistics.flippable++;
    }
    drop_candidate (idx);
  }

  stop_timer ();
}

#else

#define try_to_flip_remaining(START) \
  do { \
  } while (0)

#endif

// If the SAT solver has a model in which the candidate backbone literal for
// the given variable index is false, we drop it as a backbone candidate.

static bool filter_candidate (int idx) {
  assert (!no_filter);
  int lit = candidates[idx];
  if (!lit)
    return false;
  int val = solver->val (idx) < 0 ? -idx : idx; // Legacy support.
  assert (val == idx || val == -idx);
  if (lit == val)
    return false;
  assert (lit == -val);
  dbg ("model also satisfies negation %d "
       "of backbone candidate %d thus dropping %d",
       -lit, lit, lit);
  statistics.filtered++;
  drop_candidate (idx);
  return true;
}

// Try dropping as many variables as possible from 'start' to 'vars' based
// on the value of the remaining candidates in the current model.

static void filter_candidates (int start) {

  if (no_filter || start > vars)
    return;

  unsigned res = 0;
  for (int idx = start; idx <= vars; idx++)
    if (filter_candidate (idx), !res)
      res++;

  assert (res);
  (void) res;
}

// Drop the first candidate refuted by the current model and drop it.  In
// principle we could have merged this logic with 'filter_candidates' but we
// want to distinguish the one guaranteed dropped candidate if we find a
// model from the additional ones filtered by the model both with respect to
// statistics as well as supporting '--no-filter'.

static int drop_first_candidate (int start) {
  assert (start <= vars);
  int idx = start, lit = 0, val = 0;
  for (;; idx++) {
    assert (idx <= vars);
    lit = candidates[idx];
    if (!lit)
      continue;
    val = solver->val (idx) < 0 ? -idx : idx; // Legacy support.
    assert (val == idx || val == -idx);
    if (lit == -val)
      break;
  }
  assert (lit);
  assert (lit == -val);
  assert (idx <= vars);
  assert (candidates[idx] == lit);
  dbg ("model satisfies negation %d "
       "of backbone candidate %d thus dropping %d",
       -lit, lit, lit);
  drop_candidate (idx);
  return idx;
}

// Assume the given variable is a backbone variable with its candidate
// literal as backbone literal.  Optionally print, check and count it.

static bool backbone_variable (int idx) {
  int lit = candidates[idx];
  if (!lit)
    return false;
  fixed[idx] = lit;
  candidates[idx] = 0;
  if (!no_print) {
    fprintf (files.backbone.file, "b %d\n", lit);
    fflush (files.backbone.file);
  }
  if (checker)
    check_backbone (lit);
  assert (statistics.backbones < (size_t) vars);
  statistics.backbones++;
  return true;
}

static bool fix_candidate (int idx) {

  assert (!no_fixed);
  int lit = candidates[idx];
  assert (lit);

  int tmp = solver->fixed (lit);
  if (!tmp)
    return false;

  if (tmp > 0) {
    dbg ("found fixed backbone %d", lit);
    backbone_variable (idx);
  }

  if (tmp < 0) {
    dbg ("removing fixed backbone %d candidate", lit);
    drop_candidate (idx);
  }

  statistics.fixed++;
  return true;
}

// Force all variables from 'start' to 'vars' to be backbones unless they
// were already dropped.  This is used for 'constrain'.

static void backbone_variables (int assumed) {
  int count = 0;
  for (int i = 0; i != assumed; i++) {
    int lit = constraint[i];
    int idx = abs (lit);
    if (backbone_variable (idx))
      count++;
  }
  assert (count);
  (void) count;
}

// Want to make sure not to overwrite accidentally (without '--force') files
// which look like CNF files (as this happened to me all the time).

static bool match_until_dot (const char *str, const char *pattern) {
  assert (str);
  assert (pattern);
  const char *p = str, *q = pattern;
  while (*q) {
    if (tolower (*p) != tolower (*q))
      return false;
    p++, q++;
  }
  return !*p || *p == '.';
}

static bool looks_like_a_dimacs_file (const char *path) {
  const char *dots[2] = {0, 0};
  char ch;
  for (const char *p = path; (ch = *p); p++)
    if (ch == '.')
      dots[0] = dots[1], dots[1] = p + 1;

  const char *suffix = dots[1];
  if (!suffix)
    return false;

  if (match_until_dot (suffix, "gz") || match_until_dot (suffix, "bz2") ||
      match_until_dot (suffix, "xz") || match_until_dot (suffix, "lzma"))
    suffix = dots[0];

  if (!suffix)
    return false;

  return match_until_dot (suffix, "dimacs") ||
         match_until_dot (suffix, "cnf");
}

int ind (int i) {
  assert (i);
  return (abs (i) << 1) - 1 - (i > 0);
}
int lit (int i) { return ((i >> 1) + 1) * ((i & 1) ? -1 : 1); }
int var (int i) { return (i >> 1) + 1; }
int neg (int i) { return i ^ 1; }

class BigDegreeIterator : public CaDiCaL::ClauseIterator {
public:
  int num_edges = 0;
  std::vector<int> &f;
  BigDegreeIterator (std::vector<int> &f) : f (f) {}
  bool clause (const std::vector<int> &c) {
    if (c.size () != 2)
      return true;
    num_edges += 2;
    ++f[neg (ind (c[0])) + 2];
    ++f[neg (ind (c[1])) + 2];
    return true;
  }
};

class BigEdgeIterator : public CaDiCaL::ClauseIterator {
public:
  std::vector<int> &f, &e;
  BigEdgeIterator (std::vector<int> &f, std::vector<int> &e)
      : f (f), e (e) {}
  bool clause (const std::vector<int> &c) {
    if (c.size () != 2)
      return true;
    const int u = ind (c[0]);
    const int v = ind (c[1]);
    e[f[neg (u) + 1]++] = v;
    e[f[neg (v) + 1]++] = u;
    return true;
  }
};

static void big_extract (int num_nodes, std::vector<int> &f,
                         std::vector<int> &e) {
  f.resize (num_nodes + 2);
  BigDegreeIterator fillF (f);
  solver->traverse_clauses (fillF);
  e.resize (fillF.num_edges);
  for (size_t i = 1; i < f.size (); i++)
    f[i] += f[i - 1];
  BigEdgeIterator fillE (f, e);
  solver->traverse_clauses (fillE);
  f.pop_back ();
  assert (f.size () == static_cast<size_t> (num_nodes + 1));
  msg ("read BIG with %d nodes and %d edges", num_nodes, fillF.num_edges);
}

static int big_els (std::vector<int> &f, std::vector<int> &e,
                    std::vector<int> &extension, bool check_only = false) {
  if (e.empty ())
    return 0;
  // tarjan
  const unsigned INV = UINT_MAX;
  // using MSB as closed flag
  const unsigned MSB = 1 << (sizeof (unsigned) * 8 - 1);
  const int n = f.size () - 1;
  std::vector<unsigned> rep (n, INV);
  std::vector<int> work, scc;
  unsigned i = 0;
  for (int u = 0; u < n; u++) {
    if (rep[u] != INV)
      continue;
    work = {u};
    while (work.size () > 0) {
      int u = work.back ();
      if (u == static_cast<int> (INV)) {
        work.pop_back ();
        int u = work.back ();
        work.pop_back ();
        bool closed_scc = true;
        for (int v = f[u]; v < f[u + 1]; v++) {
          if (rep[u] > rep[e[v]]) {
            rep[u] = rep[e[v]];
            closed_scc = false;
          }
        }
        if (closed_scc) {
          size_t entry = scc.size () - 1;
          int min_lit = scc[entry];
          while (scc[entry] != u) {
            entry--;
            min_lit = std::min (min_lit, scc[entry]);
          }
          assert (scc[entry] == u);
          for (size_t i = entry; i < scc.size (); ++i) {
            int v = scc[i];
            if (neg (min_lit) == v)
              return 20; // unsatisfiable
            assert (rep[v] < MSB);
            rep[v] = min_lit | MSB;
          }
          scc.resize (entry);
          assert (scc.size () == 0 or scc.back () != u);
        }
      } else if (rep[u] == INV) {
        scc.push_back (u);
        rep[u] = i++;
        work.push_back (INV);
        for (int v = f[u]; v < f[u + 1]; v++) {
          if (rep[e[v]] == INV) {
            work.push_back (e[v]);
          }
        }
      } else {
        work.pop_back ();
      }
    }
    assert (scc.size () == 0);
  }
  std::transform (rep.begin (), rep.end (), rep.begin (),
                  [] (int x) { return x ^ MSB; });
  assert (std::all_of (rep.begin (), rep.end (),
                       [] (unsigned n) { return n < MSB; }));

  if (check_only)
    return 0;
  // sort (stable) node indices by their rep
  std::vector<int> sccs (n);
  std::iota (sccs.begin (), sccs.end (), 0);
  std::stable_sort (sccs.begin (), sccs.end (),
                    [&] (int a, int b) { return rep[a] < rep[b]; });

  // substitute
  int r = -1, u_prime = -1, l = 0;
  std::vector<int> f_prime (n + 1), e_prime, edges;
  e_prime.reserve (n);
  for (int u : sccs) {
    int r_prime = rep[u];
    if (r_prime != r) {
      if (l) {
        l = 0;
        extension.push_back (-1);
      } else if (r != -1)
        extension.pop_back ();
      r = r_prime;
      for (int v : edges) {
        marked[v] = false;
        e_prime.push_back (v);
      }
      assert (static_cast<size_t> (u_prime + 1) < f_prime.size ());
      f_prime.at (u_prime + 1) = edges.size (); // needs prefix sum
      edges.clear ();
      u_prime = r;
    } else
      l++;
    extension.push_back (u);
    assert (static_cast<int> (rep[u]) == r);

    for (int i = f[u]; i < f[u + 1]; ++i) {
      const int v = rep[e[i]];
      if (v == r)
        continue;
      if (!marked[v]) {
        edges.push_back (v);
        marked[v] = true;
      }
    }
  }
  if (l) {
    l = 0;
    extension.push_back (-1);
  } else
    extension.pop_back ();
  if (edges.size ()) {
    for (int v : edges) {
      marked[v] = false;
      e_prime.push_back (v);
    }
    f_prime[u_prime + 1] = edges.size (); // needs prefix sum
    edges.clear ();
  }

  for (size_t i = 1; i < f_prime.size (); i++)
    f_prime[i] += f_prime[i - 1];

  assert (f_prime.size () == static_cast<size_t> (n + 1));
  assert (e_prime.size () == static_cast<size_t> (f_prime.back ()));

  f = std::move (f_prime);
  e = std::move (e_prime);
  return 0;
}

static bool big_backbone_node (int node) {
  int literal = lit (node);
  int idx = var (node);
  if (!literal)
    return false;
  fixed[idx] = literal;
  if (!no_print) {
    fprintf (files.backbone.file, "b %d\n", literal);
    fflush (files.backbone.file);
  }
  solver->add (literal);
  solver->add (0);
  assert (statistics.backbones < (size_t) vars);
  statistics.backbones++;
  statistics.big_backbones++;
  return true;
}

static void big_backbone_base (const std::vector<int> &f,
                               const std::vector<int> &e) {
  msg ("BIG base searching for backbones after %.2f seconds", time ());
  const int n = f.size () - 1;
  for (int c = 0; c < n; ++c) {
    if (fixed[var (c)])
      continue;
    marked[c] = true;
    std::vector<int> tree{c};
    size_t i = 0;
    while (i < tree.size ()) {
      const int u = tree[i++];
      for (int j = f[u]; j < f[u + 1]; ++j) {
        const int v = e[j];
        if (marked[v])
          continue;
        if (marked[neg (v)]) {
          big_backbone_node (neg (c));
          i = tree.size ();
          break;
        }
        marked[v] = true;
        tree.push_back (v);
      }
    }
    for (size_t i = 0; i < tree.size (); ++i)
      marked[tree[i]] = false;
  }
}

static bool big_propagate (const std::vector<int> &f,
                           const std::vector<int> &e,
                           std::vector<int> &tree, int root) {
  size_t i = tree.size ();
  marked[root] = true;
  tree.push_back (root);
  while (i < tree.size ()) {
    const int u = tree[i++];
    assert (marked[u]);
    for (int j = f[u]; j < f[u + 1]; ++j) {
      int v = e[j];
      if (marked[v])
        continue;
      assert (!fixed[var (v)]);
      if (marked[neg (v)])
        return true;
      marked[v] = true;
      tree.push_back (v);
    }
  }
  return false;
}

template <bool big_roots>
static void big_backbone (const std::vector<int> &f,
                          const std::vector<int> &e) {
  msg ("BIG searching for backbones after %.2f seconds", time ());
  const int n = f.size () - 1;
  std::vector<int> candidates, tree, new_candidates, backbones;
  if (big_roots) {
    for (int u = 0; u < n - 1; u += 2) {
      const bool out = f[u + 1] > f[u];
      const bool in = f[u + 2] > f[u + 1];
      if (out ^ in)
        candidates.push_back (out ? u : neg (u));
    }
  } else {
    candidates.resize (n);
    std::iota (candidates.begin (), candidates.end (), 0);
  }
  msg ("BIG found %ld initial candidates", candidates.size ());
  assert (backbones.empty ());
  while (candidates.size ()) {
    const auto end = candidates.end ();
    auto j = candidates.begin ();
    for (auto i = j; i != end; i++) {
      const int save_tree = tree.size ();
      int c = *i;
      if (fixed[var (c)] || marked[c])
        continue;
      if (marked[neg (c)]) {
        *j++ = c; // delay candidate
        continue;
      }
      const bool conflict = big_propagate (f, e, tree, c);
      if (conflict) { // partial backtrack
        for (size_t i = save_tree; i < tree.size (); ++i)
          marked[tree[i]] = false;
        tree.resize (save_tree);
        const int backbone = neg (c);
        big_backbone_node (backbone);
        backbones.push_back (backbone);
        marked[backbone] = true;
        { // propagate backbone
          std::vector<int> q{backbone};
          int i = 0;
          while (static_cast<size_t> (i) < q.size ()) {
            const int u = q[i++];
            if (big_roots) {
              for (int i = f[neg (u)]; i < f[neg (u) + 1]; i++) {
                int v = e[i];
                new_candidates.push_back (v);
              }
            }
            for (int j = f[u]; j < f[u + 1]; ++j) {
              const int v = e[j];
              if (fixed[var (v)])
                continue;
              big_backbone_node (v);
              backbones.push_back (v);
              marked[v] = true;
              q.push_back (v);
            }
          }
        }
      }
    }
    candidates.resize (j - candidates.begin ());
    if (big_roots) {
      candidates.insert (candidates.end (), new_candidates.begin (),
                         new_candidates.end ());
      new_candidates.clear ();
    }
    if (candidates.empty ())
      break;
    for (int u : tree)
      marked[u] = false;
    for (int u : backbones)
      marked[u] = true;
    backbones.clear ();
    tree.clear ();
  }
}

int main (int argc, char **argv) {

  for (int i = 1; i != argc; i++) {
    const char *arg = argv[i];
    if (!strcmp (arg, "-h")) {
      fputs (usage, stdout);
      exit (0);
    } else if (!strcmp (arg, "-V") || !strcmp (arg, "--version")) {
      fputs (VERSION, stdout);
      fputc ('\n', stdout);
      exit (0);
    } else if (!strcmp (arg, "-c") || !strcmp (arg, "--check")) {
      check = arg;
    } else if (!strcmp (arg, "-f") || !strcmp (arg, "--force")) {
      force = arg;
    } else if (!strcmp (arg, "-l") || !strcmp (arg, "--logging")) {
      verbosity = INT_MAX;
    } else if (!strcmp (arg, "-n") || !strcmp (arg, "--no-print")) {
      no_print = arg;
    } else if (!strcmp (arg, "-q") || !strcmp (arg, "--quiet")) {
      verbosity = -1;
    } else if (!strcmp (arg, "-r") || !strcmp (arg, "--report")) {
      report = true;
    } else if (!strcmp (arg, "-s") || !strcmp (arg, "--statistics")) {
      always_print_statistics = true;
    } else if (!strcmp (arg, "-v") || !strcmp (arg, "--verbose")) {
      if (verbosity < 0)
        verbosity = 1;
      else if (verbosity < INT_MAX)
        verbosity++;
    } else if (!strcmp (arg, "--no-constrain")) {
      no_constrain = arg;
    } else if (!strcmp (arg, "--no-filter")) {
      no_filter = arg;
    } else if (!strcmp (arg, "--no-fixed")) {
      no_fixed = arg;
    } else if (!strcmp (arg, "--no-flip")) {
#ifndef NFLIP
      no_flip = arg;
#else
    NO_CADICAL_SUPPORT_FOR_FLIPPING:
      die ("invalid option '%s' (CaDiCaL does not support flipping)" arg);
#endif
    } else if (!strcmp (arg, "--really-flip")) {
#ifndef NFLIP
      really_flip = arg;
#else
      goto NO_CADICAL_SUPPORT_FOR_FLIPPING;
#endif
    } else if (!strcmp (arg, "--no-inprocessing")) {
      no_inprocessing = arg;
    } else if (!strcmp (arg, "--one-by-one")) {
      one_by_one = arg;
    } else if (!strcmp (arg, "--cores")) {
      cores = arg;
    } else if (!strcmp (arg, "--chunking")) {
      chunking = arg;
    } else if (!strcmp (arg, "--set-phase")) {
      set_phase = true;
    } else if (!strcmp (arg, "--big")) {
      big = arg;
    } else if (!strcmp (arg, "--big-no-els")) {
      big_no_els = arg;
      if (!big)
        big = arg;
    } else if (!strcmp (arg, "--big-roots")) {
      big_roots = arg;
      if (!big)
        big = arg;
    } else if (!strcmp (arg, "--default")) {
      no_filter = no_fixed = no_inprocessing = one_by_one = 0;
#ifndef NFLIP
      no_flip = 0;
#endif
    } else if (!strcmp (arg, "--plain")) {
      no_filter = no_fixed = no_inprocessing = one_by_one = arg;
#ifndef NFLIP
      no_flip = arg;
#endif
    } else if (arg[0] == '-' && arg[1])
      die ("invalid option '%s' (try '-h')", arg);
    else if (files.backbone.path)
      die ("too many arguments '%s', '%s' and '%s'", files.dimacs.path,
           files.backbone.path, arg);
    else if (files.dimacs.path)
      files.backbone.path = arg;
    else
      files.dimacs.path = arg;
  }

  if (files.backbone.path) {
    if (no_print)
      die ("writing backbone to '%s' and '%s' does not make sense",
           files.backbone.path, no_print);
    if (!force && looks_like_a_dimacs_file (files.backbone.path))
      die ("will not write to CNF alike backbone file '%s' "
           "without '--force'",
           files.backbone.path);
  } else if (force)
    die ("'%s' does not make sense without backbone file argument", force);

  if (one_by_one && chunking)
    die ("'%s' does not make sense with '%s'", chunking, one_by_one);

  if (one_by_one && no_constrain)
    die ("'%s' does not make sense with '%s'", no_constrain, one_by_one);

#ifndef NFLIP
  if (no_flip && really_flip)
    die ("'%s' does not make sense in combination with '%s'", really_flip,
         no_flip);
#endif

  if (big_no_els && big_roots)
    die ("'%s' does not make sense in combination with '%s'", big_no_els,
         big_roots);

  msg ("CadiBack BackBone Extractor");
  msg ("Copyright (c) 2023 Armin Biere University of Freiburg");
  msg ("Version " VERSION " " GITID);
  msg ("CaDiCaL %s %s", CaDiCaL::version (), CaDiCaL::identifier ());
  msg ("Compiled with '%s'", BUILD);
  line ();

  if (files.backbone.path && strcmp (files.backbone.path, "-")) {
    if (!(files.backbone.file = fopen (files.backbone.path, "w")))
      die ("can not write backbone to '%s'", files.backbone.path);
    files.backbone.close = true;
  } else {
    files.backbone.file = stdout;
    files.backbone.path = "<stdout>";
    assert (!files.backbone.close);
  }
  msg ("writing backbones to '%s'", files.backbone.path);

  if (check) {
    checker = new CaDiCaL::Solver ();
    msg ("checking models with copy of main solver by '%s'", check);
  } else
    msg ("not checking models and backbones "
         "(enable with '--check')");

  if (cores)
    msg ("using core base preprocessing by '%s'", cores);
  else
    msg ("core based preprocessing disabled (enable with '--cores')");

  if (no_constrain)
    msg ("using 'constrain' interface disabled by '%s'", no_constrain);
  else
    msg ("using 'constrain' interface (disable with '--no-constrain')");

  if (no_filter)
    msg ("filtering backbones by models disabled by '%s'", no_filter);
  else
    msg ("filtering backbones by models (disable with '--no-filter')");

  if (no_fixed)
    msg ("using root-level fixed literals disabled by '%s'", no_fixed);
  else
    msg ("using root-level fixed literals (disable with '--no-fixed')");

#ifndef NFLIP
  if (no_flip)
    msg ("trying to use flippable literals disabled by '%s'", no_flip);
  else
    msg ("trying to use flippable literals (disable with '--no-flip')");

  if (really_flip)
    msg ("will actually flip flippable literals by '%s'", really_flip);
  else
    msg ("only dropping flippable candidates without flipping them");
#endif

  if (no_inprocessing)
    msg ("SAT solver inprocessing disabled by '%s'", no_inprocessing);
  else
    msg ("SAT solver inprocessing (disable with '--no-inprocessing')");

  if (one_by_one)
    msg ("backbone candidates checked one-by-one by '%s'", one_by_one);
  else
    msg ("backbone candidates checked all-at-once "
         "(disable with '--one-by-one')");

  if (set_phase)
    msg ("phases explicitly forced by '--set-phase'");
  else
    msg ("phases picked by SAT solver "
         "(force with '--set-phase')");
  line ();

  solver = new CaDiCaL::Solver ();
  if (no_inprocessing)
    solver->set ("inprocessing", 0);

  if (verbosity < 0)
    solver->set ("quiet", 1);
  else if (verbosity > 1)
    solver->set ("verbose", verbosity - 2);
  if (report || verbosity > 1)
    solver->set ("report", 1);

  int res = 0;
  {
    CadiBackSignalHandler handler;
    CaDiCaL::Signal::set (&handler);
    dbg ("initialized solver");
    {
      const char *err;
      if (files.dimacs.path && strcmp (files.dimacs.path, "-")) {
        msg ("reading from '%s'", files.dimacs.path);
        err = solver->read_dimacs (files.dimacs.path, vars);
      } else {
        msg ("reading from '<stdin>");
        err = solver->read_dimacs (stdin, "<stdin>", vars);
      }
      if (err)
        die ("%s", err);

      // Computing 'vars + 1' as well as the idiom 'idx <= vars' in 'for'
      // loops requires 'vars' to be less than 'INT_MAX' to avoid
      // overflows. For simplicity we force having less variables here.
      //
      if (vars == INT_MAX) {
        die ("can not support 'INT_MAX == %d' variables", vars);
      }
    }
    msg ("found %d variables", vars);

    if (big) {
      msg ("starting BIG search after %.2f seconds", time ());
      std::vector<int> f, e;
      const int num_nodes = 2 * vars;
      start_timer (&big_read_time);
      big_extract (num_nodes, f, e);
      marked = new char[num_nodes];
      if (!marked)
        fatal ("out-of-memory allocating marked flag for BIG nodes");
      for (int u = 0; u < num_nodes; u++)
        marked[u] = false;
      stop_timer ();

      // Keeps track of the ELS groups.
      // If the representative of a group of literals is found to be a
      // backbone all literals in the group need to be marked as a backbone.
      std::vector<int> extension;
      start_timer (&big_els_time);
      if (!big_no_els)
        res = big_els (f, e, extension);
      stop_timer ();

      if (res) {
        assert (res == 20);
        msg ("Unsatisfiability determined by ELS");
        printf ("s UNSATISFIABLE\n");
        if (files.backbone.close)
          fclose (files.backbone.file);
        print_statistics ();
        if (check)
          assert (solve () == 20);
        dbg ("deleting solver");
        CaDiCaL::Signal::reset ();
        delete solver;
        line ();
        msg ("exit %d", res);
        return res;
      }

      fixed = new int[vars + 1];
      if (!fixed)
        fatal ("out-of-memory allocating backbone result array");
      for (int idx = 1; idx <= vars; idx++)
        fixed[idx] = 0;

      start_timer (&big_search_time);
      if (big_roots)
        big_backbone<true> (f, e);
      else
        big_backbone<false> (f, e);
      stop_timer ();
      if (check) {
        start_timer (&big_check_time);
        std::vector<int> backbone, backbone_base, dummy;
        if (!big_no_els || !big_els (f, e, dummy, true)) {
          for (int idx = 1; idx <= vars; idx++) {
            if (fixed[idx])
              backbone.push_back (fixed[idx]);
            fixed[idx] = 0;
          }
          for (size_t u = 0; u < f.size () - 1; u++)
            marked[u] = false;
          statistics.backbones = 0, statistics.big_backbones = 0;
          big_backbone_base (f, e);
          for (int idx = 1; idx <= vars; idx++)
            if (fixed[idx])
              backbone_base.push_back (fixed[idx]);
          assert (backbone == backbone_base);
        }
        stop_timer ();
      }

      // extending backbones to their scc
      start_timer (&big_extension_time);
      int fixed_val = 0;
      for (int u : extension) {
        if (u == -1)
          fixed_val = 0;
        else if (fixed_val)
          big_backbone_node (u);
        else {
          const int val = fixed[var (u)];
          if (val == lit (u))
            fixed_val = val;
        }
      }
      stop_timer ();

      msg ("BIG found %ld backbones after %.2f seconds",
           statistics.big_backbones, time ());
      delete[] marked;
    }

    // Determine first model or that formula is unsatisfiable.

    line ();
    msg ("starting solving after %.2f seconds", time ());
    res = solve ();
    assert (res == 10 || res == 20);

    if (checker) {
      dbg ("copying checker after first model");
      solver->copy (*checker);
    }

    if (res == 10) {

      msg ("solver determined first model after %.2f seconds", time ());
      if (report || verbosity > 1)
        line ();

      candidates = new int[vars + 1];
      if (!candidates)
        fatal ("out-of-memory allocating backbone candidate array");

      if (!big) {
        fixed = new int[vars + 1];
        if (!fixed)
          fatal ("out-of-memory allocating backbone result array");
      }

      if (!one_by_one) {
        constraint = new int[vars];
        if (!constraint)
          fatal ("out-of-memory allocating constraint stack");
      }

      if (cores) {
        core = new int[vars];
        if (!core)
          fatal ("out-of-memory allocating literal core stack");
      }

      // Initialize the candidate backbone literals with first model.

      for (int idx = 1; idx <= vars; idx++) {
        int lit = solver->val (idx) < 0 ? -idx : idx; // Legacy support.
        assert (lit == idx || lit == -idx);
        if (!big) {
          candidates[idx] = lit;
          fixed[idx] = 0;
        } else if (fixed[idx])
          candidates[idx] = 0;
        else
          candidates[idx] = lit;
        // If enabled by '--set-phase' set opposite value as default
        // decision phase.  This seems to have  negative effects with and
        // without using 'constrain' and thus is disabled by default.

        if (set_phase)
          solver->phase (-lit);
      }

      // Use first model to flip as many literals as possible which if
      // successful is cheaper than calling the SAT solver.

      try_to_flip_remaining (1);

      // Now go over all variables in turn and check whether they still
      // are candidates for being a backbone variables.  Each step of this
      // loop either drops at least one candidate or determines at least
      // one candidate to be a backbone (or skips already dropped
      // variables).

      int activation_variable = vars; // New variables if '--no-contrain'.
      int constraint_limit = INT_MAX; // Adapted dynamically using 'last'.
      int core_limit = 100;           // TODO make this configurable.
      int last = 10;                  // Last solver result.

      for (int idx = 1; idx <= vars; idx++) {

        // First skip variables that have been dropped as candidates
        // before.

        int lit = candidates[idx];
        if (!lit)
          continue;

        // With 'constrain' we might drop another literal but not 'idx'
        // and in that case simply restart checking 'idx' for being a
        // candidate (same applies if 'cores' are enabled).

      TRY_SAME_CANDIDATE_AGAIN:

        assert (lit == candidates[idx]);
        assert (lit);

        // If not disabled by '--no-fixed' filter root-level fixed
        // literals.

        if (!no_fixed && fix_candidate (idx))
          continue;

        if (cores) {

          assert (core_limit > 1);
          int assumed = 0;

          assert (assumed < vars);
          core[assumed++] = -lit;

          for (int other = idx + 1; other <= vars; other++) {
            int lit_other = candidates[other];
            if (!lit_other)
              continue;
            if (!no_fixed && fix_candidate (other))
              continue;
            assert (assumed < vars);
            core[assumed++] = -lit_other;

            if (assumed == core_limit)
              break;
          }

          bool progress = false;

          while (assumed) {

            dbg ("core based approach assumes %d literals", assumed);

            for (int i = 0; i != assumed; i++)
              solver->assume (core[i]);

            int tmp = solve ();
            if (tmp == 10) {

              dbg ("all %d negatively assumed backbone candidates "
                   "can be dropped",
                   assumed);

              for (int i = 0; i != assumed; i++)
                drop_candidate (abs (core[i]));

              statistics.failed += assumed;

              assert (INT_MAX - assumed >= idx);
              filter_candidates (idx);
              progress = true;
              assumed = -1;
              break;
            }

            assert (tmp == 20);

            int num_failed = 0;
            int failed_lit = 0;
            int remain = 0;

            for (int i = 0; i != assumed; i++) {
              int other = core[i];
              bool other_failed = solver->failed (other);
              if (other_failed) {
                failed_lit = other;
                num_failed++;
              }
              int other_idx = abs (other);
              assert (candidates[other_idx] == -other);
              if (!no_fixed && fix_candidate (other_idx)) {
                progress = true;
                continue;
              }
              if (!other_failed)
                core[remain++] = other;
            }

            dbg ("failed literal core of size %d", num_failed);
            assert (remain < assumed);
            assert (num_failed);

            if (num_failed == 1 && backbone_variable (abs (failed_lit))) {
              statistics.failed++;
              progress = true;
            }

            assumed = remain;
            dbg ("reducing core assumptions to complement of size %d",
                 remain);
          }

          if (progress) {

            dbg ("continuing with next core");

            if (candidates[idx])
              goto TRY_SAME_CANDIDATE_AGAIN;
            else
              continue;
          }

          dbg ("falling back to iterative approach");
        }

        // If not disabled through '--one-by-one' use the 'constrain'
	// optimization which assumes the disjunction of the negation of all
	// remaining possible backbone candidate literals.  By default this
	// uses the 'constrain' API call described in our FMCAD'21 paper
	// (unless '--no-constrain' is specified in which case we use
	// activation literals as in 'MiniBones')).

        // If the remaining backbone candidates are all actually backbones
	// then only one such call can be enough to prove it. Otherwise
	// without 'constraints' we need as many solver calls as there are
	// candidates.  Without constrain this puts heavy load on the
	// 'restore' algorithm which in some instances ended up taking 99%
	// of the running time.

	// It seems reasonable to limit the size of the constraint (the
	// number of negated candidate literals where one is assumed to be
	// flippable) by some sort of chunking.  In contrast to earlier work
	// in 'MiniBones' we adapt the limit during chunking as follows.  As
	// long constraint was unsatisfiable (and all the contained
	// candidates are thus fixed) we increase the limit on the
	// considered candidates in the constraint exponentially (by the
	// hard coded factor 10).  If the call returns a model we go back to
	// checking candidates one-by-one.  If the following call returns
	// unsatisfiable, we limit the size of the constraint to 10
	// candidates next time etc.

        if (!one_by_one && chunking) {
          if (last == 20)
            constraint_limit = (constraint_limit < INT_MAX / 10)
                                   ? 10 * constraint_limit
                                   : INT_MAX;
          else
            constraint_limit = 1;
        }

        if (!one_by_one && last == 20) {

          assert (constraint_limit > 1);
          int assumed = 0;
          assert (assumed < vars);
          constraint[assumed++] = -lit;

          for (int other = idx + 1; other <= vars; other++) {
            int lit_other = candidates[other];
            if (!lit_other)
              continue;
            if (!no_fixed && fix_candidate (other))
              continue;
            assert (assumed < vars);
            constraint[assumed++] = -lit_other;

            if (assumed == constraint_limit)
              break;
          }

          if (assumed == 1)
            goto ASSUME_NEGATION_OF_SINGLE_BACKBONE_CANDIDATE;

          dbg ("assuming negation of %d remaining backbone "
               "candidates starting with variable %d",
               assumed, idx);

          if (no_constrain) {
            activation_variable++;
            dbg ("new activation variable %s", activation_variable);
            solver->add (activation_variable);
            for (int i = 0; i != assumed; i++)
              solver->add (constraint[i]);
            solver->add (0);
            solver->assume (-activation_variable);
          } else {
            for (int i = 0; i != assumed; i++)
              solver->constrain (constraint[i]);
            solver->constrain (0);
          }

          last = solve ();
          if (last == 10) {
            dbg ("constraining negation of %d backbones candidates "
                 "starting with variable %d all-at-once produced model",
                 assumed, idx);
            int other = drop_first_candidate (idx);
            filter_candidates (other + 1);
            try_to_flip_remaining (idx);
          }

          if (no_constrain) {
            solver->add (activation_variable);
            solver->add (0);
          }

          if (last == 10) {

            lit = candidates[idx];
            if (lit)
              goto TRY_SAME_CANDIDATE_AGAIN;

            continue; // ... with next candidate.
          }

          assert (last == 20);
          msg ("%d remaining candidates starting at %d "
               "shown to be backbones in one call",
               assumed, lit);
          backbone_variables (assumed); // Plural!  So all assumed.
          continue;
        }

      ASSUME_NEGATION_OF_SINGLE_BACKBONE_CANDIDATE:

        dbg ("no other literal besides %d remains a backbone candidate",
             lit);

        dbg ("assuming negation %d of backbone candidate %d", -lit, lit);
        solver->assume (-lit);
        last = solve ();
        if (last == 10) {
          dbg ("found model satisfying single assumed "
               "negation %d of backbone candidate %d",
               -lit, lit);
          drop_candidate (idx);
          filter_candidates (idx + 1);
          assert (!candidates[idx]);
          try_to_flip_remaining (idx + 1);
        } else {
          assert (last == 20);
          dbg ("no model with %d thus found backbone literal %d", -lit,
               lit);
          backbone_variable (idx); // Singular! So only this one.
        }
      }

      // All backbones found! So terminate the backbone list with 'b 0'.

      if (!no_print) {
        fprintf (files.backbone.file, "b 0\n");
        fflush (files.backbone.file);
      }

      // We only print 's SATISFIABLE' here which is supposed to indicate
      // that the run completed.  Otherwise printing it before printing
      // 'b' lines confuses scripts (and 'zummarize').

      line ();
      printf ("s SATISFIABLE\n");
      fflush (stdout);

#ifndef NDEBUG

      if (res == 10) {

        // At the end all variables are either backbones or filtered.

        {
          size_t count = 0;
          for (int idx = 1; idx <= vars; idx++)
            if (fixed[idx])
              count++;

          assert (count == statistics.backbones);
        }

        {
          size_t count = 0;
          for (int idx = 1; idx <= vars; idx++)
            if (!fixed[idx])
              count++;

          assert (count == statistics.dropped);
        }

        assert (statistics.backbones + statistics.dropped == (size_t) vars);
      }

#endif

      delete[] candidates;
      delete[] fixed;

      if (!one_by_one)
        delete[] constraint;

      if (cores)
        delete[] core;

      if (checker) {
        if (statistics.checked < (size_t) vars)
          fatal ("checked %zu literals and not all %d variables",
                 statistics.checked, vars);
        else if (statistics.checked > (size_t) vars)
          fatal ("checked %zu literals thus more than all %d variables",
                 statistics.checked, vars);
        delete checker;
      }
    } else {
      assert (res == 20);
      printf ("s UNSATISFIABLE\n");
    }

    if (files.backbone.close)
      fclose (files.backbone.file);

    print_statistics ();
    dbg ("deleting solver");
    CaDiCaL::Signal::reset ();
  }

  delete solver;

  line ();
  msg ("exit %d", res);

  return res;
}