Fixed (i)val, recompute glue (to promote clauses) and condition (glob…

…ally blocked).

BUILD.md

@@ -16,7 +16,10 @@ The header file of the library is in
 
 The build process requires GNU make.  Using the generated `makefile` with
 GNU make compiles separate object files, which can be cached (for instance
-with `ccache`).  The `makefile` uses parallel compilation by default (`-j`).
+with `ccache`).  In order to force parallel build you can use the '-j'
+option either for 'configure' or with 'make'.  If the environment variable
+'MAKEFLAGS' is set, e.g., 'MAKEFLAGS=-j ./configure', the same effect
+is achieved and the generated makefile will use those flags.
 
 You might want to check out options of `./configure -h`, such as
 

VERSION

@@ -1 +1 @@
-1.1.0
+1.2.0

configure

@@ -396,7 +396,7 @@ sed \
 -e "2c\\
 # This 'makefile' is generated from '../makefile.in'." \
 -e "s,@CXX@,$CXX," \
--e "s,@CXXFLAGS@,$CXXFLAGS," \
+-e "s#@CXXFLAGS@#$CXXFLAGS#" \
 -e "s,@MAKEFLAGS@,$MAKEFLAGS," \
 ../makefile.in > makefile
 
@@ -409,27 +409,27 @@ makefile="`dirname "$build"`/makefile"
 cat <<EOF > "$makefile"
 CADICALBUILD=$build
 all:
-	make -C "\$(CADICALBUILD)"
+	\$(MAKE) -C "\$(CADICALBUILD)"
 clean:
 	@if [ -d "\$(CADICALBUILD)" ]; \\
 	then \\
 	  if [ -f "\$(CADICALBUILD)"/makefile ]; \\
 	  then \\
 	     touch "\$(CADICALBUILD)"/build.hpp; \\
 	     touch "\$(CADICALBUILD)"/dependencies; \\
-	     make -C "\$(CADICALBUILD)" clean; \\
+	     \$(MAKE) -C "\$(CADICALBUILD)" clean; \\
 	  fi; \\
 	  rm -rf "\$(CADICALBUILD)"; \\
 	fi
 	rm -f "$makefile"
 test:
-	make -j1 -C "\$(CADICALBUILD)" test
+	\$(MAKE) -j1 -C "\$(CADICALBUILD)" test
 cadical:
-	make -j1 -C "\$(CADICALBUILD)" cadical
+	\$(MAKE) -j1 -C "\$(CADICALBUILD)" cadical
 mobical:
-	make -j1 -C "\$(CADICALBUILD)" mobical
+	\$(MAKE) -j1 -C "\$(CADICALBUILD)" mobical
 update:
-	make -j1 -C "\$(CADICALBUILD)" update
+	\$(MAKE) -j1 -C "\$(CADICALBUILD)" update
 .PHONY: all cadical clean mobical test update
 EOF
 

makefile.in

@@ -22,7 +22,7 @@ APP=cadical.cpp mobical.cpp
 ALL=$(sort $(wildcard ../src/*.[ch]pp))
 SRC=$(filter %.cpp,$(subst ../src/,,$(ALL)))
 LIB=$(filter-out $(APP),$(SRC))
-OBJ=$(patsubst %.cpp,%.o,$(LIB))
+OBJ=$(LIB:.cpp=.o)
 DIR=../$(shell pwd|sed -e 's,.*/,,')
 COMPILE=$(CXX) $(CXXFLAGS) -I$(DIR)
 
@@ -81,7 +81,7 @@ clean:
 	rm -f *.gcda *.gcno *.gcov gmon.out
 
 test: all
-	CADICALBUILD="$(DIR)" make -j1 -C ../test
+	CADICALBUILD="$(DIR)" $(MAKE) -j1 -C ../test
 
 #--------------------------------------------------------------------------#
 

src/analyze.cpp

@@ -55,8 +55,8 @@ void Internal::bump_queue (int lit) {
 // and simply put a hard limit here.  It is less elegant but easy to port.
 
 static inline bool evsids_limit_hit (double score) {
-  assert (sizeof (score) == 8);	// assume IEEE 754 64-bit double
-  return score > 1e150;		// MAX_DOUBLE is around 1.8e308
+  assert (sizeof (score) == 8); // assume IEEE 754 64-bit double
+  return score > 1e150;         // MAX_DOUBLE is around 1.8e308
 }
 
 /*------------------------------------------------------------------------*/
@@ -178,14 +178,35 @@ void Internal::bump_variables () {
 
 /*------------------------------------------------------------------------*/
 
-// Clauses resolved since the last reduction are marked as 'used'.
+// We use the glue time stamp table 'gtab' for fast glue computation.
+
+int Internal::recompute_glue (Clause * c) {
+  int res = 0;
+  const int64_t stamp = ++stats.recomputed;
+  for (const auto & lit : *c) {
+    int level = var (lit).level;
+    assert (gtab[level] <= stamp);
+    if (gtab[level] == stamp) continue;
+    gtab[level] = stamp;
+    res++;
+  }
+  return res;
+}
+
+// Clauses resolved since the last reduction are marked as 'used', their
+// glue is recomputed and they promoted if the glue shrinks.  Note that
+// promotion from 'tier3' to 'tier2' will set 'used' to '2'.
 
 inline void Internal::bump_clause (Clause * c) {
   LOG (c, "bumping");
-  if (c->hyper) c->used = 1;
-  else if (c->glue <= opts.reducekeepglue) c->used = 1;
-  else if (c->glue <= opts.reducetier2glue) c->used = 2;
-  else c->used = 1;
+  unsigned used = c->used;
+  c->used = 1;
+  if (c->keep) return;
+  if (c->hyper) return;
+  if (!c->redundant) return;
+  int new_glue = recompute_glue (c);
+  if (new_glue < c->glue) promote_clause (c, new_glue);
+  else if (used && c->glue <= opts.reducetier2glue) c->used = 2;
 }
 
 /*------------------------------------------------------------------------*/
@@ -347,7 +368,7 @@ Clause * Internal::new_driving_clause (const int glue, int & jump) {
     // We have to get the last assigned literals into the watch position.
     // Sorting all literals with respect to reverse assignment order is
     // overkill but seems to get slightly faster run-time.  For 'minimize'
-    // we sort the literals to heuristically along the trail order (so in
+    // we sort the literals too heuristically along the trail order (so in
     // the opposite order) with the hope to hit the recursion limit less
     // frequently.  Thus sorting effort is doubled here.
     //
@@ -357,7 +378,8 @@ Clause * Internal::new_driving_clause (const int glue, int & jump) {
 
     jump = var (clause[1]).level;
     res = new_learned_redundant_clause (glue);
-    bump_clause (res);
+    if (glue <= opts.reducetier2glue) res->used = 2;
+    else res->used = 1;
   }
 
   LOG ("jump level %d", jump);
@@ -654,7 +676,7 @@ void Internal::analyze () {
 
   int i = trail.size ();        // Start at end-of-trail.
   int open = 0;                 // Seen but not processed on this level.
-  int uip = 0;                  // The first uip literal.
+  int uip = 0;                  // The first UIP literal.
 
   for (;;) {
     analyze_reason (uip, reason, open);
@@ -672,24 +694,21 @@ void Internal::analyze () {
   LOG ("first UIP %d", uip);
   clause.push_back (-uip);
 
-  // Update glue statistics.
+  // Update glue and learned (1st UIP literals) statistics.
   //
-  const int glue = (int) levels.size ();
-  LOG (clause, "1st UIP size %zd and glue %d clause",
-    clause.size (), glue);
+  int size = (int) clause.size ();
+  const int glue = (int) levels.size () - 1;
+  LOG (clause, "1st UIP size %d and glue %d clause", size, glue);
   UPDATE_AVERAGE (averages.current.glue.fast, glue);
   UPDATE_AVERAGE (averages.current.glue.slow, glue);
+  stats.learned.literals += size;
+  stats.learned.clauses++;
+  assert (glue < size);
 
   // Update decision heuristics.
   //
   if (opts.bump) bump_variables ();
 
-  // Update learned = 1st UIP literals counter.
-  //
-  int size = (int) clause.size ();
-  stats.learned.literals += size;
-  stats.learned.clauses++;
-
   // Minimize the 1st UIP clause as pioneered by Niklas Soerensson in
   // MiniSAT and described in our joint SAT'09 paper.
   //

src/assume.cpp

@@ -60,7 +60,7 @@ void Internal::failing () {
     // Find an assumption falsified at smallest decision level.
     //
     for (auto & lit : assumptions) {
-      const int tmp = val (lit);
+      const signed char tmp = val (lit);
       if (tmp >= 0) continue;
       if (!first || var (first).level > var (lit).level)
         first = lit;

src/backtrack.cpp

@@ -20,7 +20,7 @@ inline void Internal::unassign (int lit) {
   if (!scores.contains (idx)) scores.push_back (idx);
 
   // For VMTF we need to update the 'queue.unassigned' pointer in case this
-  // variables sits after the variable to which 'queue.unassigned' currently
+  // variable sits after the variable to which 'queue.unassigned' currently
   // points.  See our SAT'15 paper for more details on this aspect.
   //
   if (queue.bumped < btab[idx]) update_queue_unassigned (idx);
@@ -30,7 +30,7 @@ inline void Internal::unassign (int lit) {
 
 // Update the current target maximum assignment and also the very best
 // assignment.  Whether a trail produces a conflict is determined during
-// propagation, thus that all functions in the 'search' loop after
+// propagation.  Thus that all functions in the 'search' loop after
 // propagation can assume that 'no_conflict_until' is valid.  If a conflict
 // is found then the trail before the last decision is used (see the end of
 // 'propagate').  During backtracking we can then save this largest

src/backward.cpp

@@ -44,7 +44,7 @@ void Internal::elim_backward_clause (Eliminator & eliminator, Clause *c) {
   int best = 0;
   bool satisfied = false;
   for (const auto & lit : *c) {
-    const int tmp = val (lit);
+    const signed char tmp = val (lit);
     if (tmp > 0) { satisfied = true; break; }
     if (tmp < 0) continue;
     size_t l = occs (lit).size ();
@@ -70,7 +70,7 @@ void Internal::elim_backward_clause (Eliminator & eliminator, Clause *c) {
       int negated = 0;
       unsigned found = 0;
       for (const auto & lit : *d) {
-        int tmp = val (lit);
+        signed char tmp = val (lit);
         if (tmp > 0) { satisfied = true; break; }
         if (tmp < 0) continue;
         tmp = marked (lit);
@@ -95,7 +95,7 @@ void Internal::elim_backward_clause (Eliminator & eliminator, Clause *c) {
         } else {
           int unit = 0;
           for (const auto & lit : * d) {
-            const int tmp = val (lit);
+            const signed char tmp = val (lit);
             if (tmp < 0) continue;
             if (tmp > 0) { satisfied = true; break; }
             if (lit == negated) continue;

src/cadical.cpp

@@ -94,7 +94,7 @@ void App::print_usage (bool all) {
 "\n"
 "or one of the less common options\n"
 "\n"
-"  -O<level>      increase limits by '10^<level>' (default level '0')\n"
+"  -O<level>      increase limits by '{2,10}^<level>' (default '0')\n"
 "  -P<rounds>     enable preprocessing initially (default '0' rounds)\n"
 "  -L<rounds>     run local search initialially (default '0' rounds)\n"
 "\n"
@@ -332,8 +332,8 @@ int App::main (int argc, char ** argv) {
              !strcmp (argv[i], "--strict=true")) strict = 2;
     else if (argv[i][0] == '-' && argv[i][1] == 'O') {
       if (!parse_int_str (argv[i] + 2, optimize) ||
-          optimize < 0 || optimize > 3)
-        APPERR ("invalid optimization option '%s' (expected '-O[0..3]')",
+          optimize < 0 || optimize > 31)
+        APPERR ("invalid optimization option '%s' (expected '-O[0..31]')",
           argv[i]);
     } else if (argv[i][0] == '-' && argv[i][1] == 'P') {
       if (!parse_int_str (argv[i] + 2, preprocessing) || preprocessing < 0)
@@ -489,7 +489,11 @@ int App::main (int argc, char ** argv) {
   solver->section ("solving");
   res = solver->solve ();
 
-  if (proof_specified) solver->close_proof_trace ();
+  if (proof_specified) {
+    solver->section ("closing proof");
+    solver->flush_proof_trace ();
+    solver->close_proof_trace ();
+  }
 
   if (output_path) {
     solver->section ("writing output");

src/cadical.hpp

@@ -505,6 +505,13 @@ class Solver {
   bool trace_proof (FILE * file, const char * name); // Write DRAT proof.
   bool trace_proof (const char * path);              // Open & write proof.
 
+  // Flush proof trace file.
+  //
+  //   require (VALID)
+  //   ensure (VALID)
+  //
+  void flush_proof_trace ();
+
   // Close proof trace early.
   //
   //   require (VALID)
@@ -736,10 +743,12 @@ class ClauseIterator {
 /*------------------------------------------------------------------------*/
 
 // Allows to traverse all clauses on the extension stack together with their
-// witness cubes.  If the solver is inconsistent nothing is traversed.
+// witness cubes.  If the solver is inconsistent, i.e., an empty clause is
+// found and the formula is unsatisfiable, then nothing is traversed.
 //
 // The clauses traversed in 'traverse_clauses' together with the clauses on
 // the extension stack are logically equivalent to the original clauses.
+// See our SAT'19 paper for more details.
 //
 // The witness literals can be used to extend and fix an assignment on the
 // remaining clauses to satisfy the clauses on the extension stack too.

src/checker.cpp

@@ -261,7 +261,7 @@ bool Checker::tautological () {
     int lit = *i;
     if (lit == prev) continue;          // duplicated literal
     if (lit == -prev) return true;      // tautological clause
-    const int tmp = val (lit);
+    const signed char tmp = val (lit);
     if (tmp > 0) return true;           // satisfied literal and clause
     *j++ = prev = lit;
   }
@@ -335,7 +335,7 @@ inline void Checker::assign (int lit) {
 }
 
 inline void Checker::assume (int lit) {
-  int tmp = val (lit);
+  signed char tmp = val (lit);
   if (tmp > 0) return;
   assert (!tmp);
   stats.assumptions++;
@@ -378,7 +378,7 @@ bool Checker::propagate () {
       CheckerWatch & w = *j++ = *i;
       const int blit = w.blit;
       assert (blit != -lit);
-      const int blit_val = val (blit);
+      const signed char blit_val = val (blit);
       if (blit_val > 0) continue;
       const unsigned size = w.size;
       if (size == 2) {                          // not precise since
@@ -392,11 +392,12 @@ bool Checker::propagate () {
         int * lits = c->literals;
         int other = lits[0]^lits[1]^(-lit);
         assert (other != -lit);
-        int other_val = val (other);
+        signed char other_val = val (other);
         if (other_val > 0) { j[-1].blit = other; continue; }
         lits[0] = other, lits[1] = -lit;
         unsigned k;
-        int replacement = 0, replacement_val = -1;
+        int replacement = 0;
+        signed char replacement_val = -1;
         for (k = 2; k < size; k++)
           if ((replacement_val = val (replacement = lits[k])) >= 0)
             break;
@@ -434,7 +435,7 @@ void Checker::add_clause (const char * type) {
 
   int unit = 0;
   for (const auto & lit : simplified) {
-    const int tmp = val (lit);
+    const signed char tmp = val (lit);
     if (tmp < 0) continue;
     assert (!tmp);
     if (unit) { unit = INT_MIN; break; }