imported sc2022-light

NEWS.md

@@ -1,3 +1,43 @@
+Version sc2022-light
+--------------------
+
+We started with version sc2022-bulky and then removed code which only gave a
+minor improvement on the last three SAT Competition 2019-2021.  The goal was
+to shrink the code base in order to concentrate on the really useful
+algorithms and heuristics and thus prepare for extending the solver.
+
+This is the list of removed features:
+
+  - autarky reasoning
+  - eager forward and backward subsumption during variable elimination
+    (relying on global forward subsumption instead)
+  - caching and reusing of minimum assignments during local search
+  - failed literal probing
+  - hyper binary resolution
+  - hyper ternary resolution
+  - transitive reduction of the binary implication graph
+  - eager subsumption of recently learned clauses during clause learning
+  - xor gate extraction during variable elimination
+  - alternative radix heap implementation for advanced shrinking
+  - priority queue for variable elimination (elimination attempts of
+    variables in the given variable order is now enforced)
+  - delaying of inprocessing functions based on formula size (initially
+    'really' and if not successful 'delay')
+  - reusing the trail during restarts
+  - vivification of irredundant clauses
+  - forced to keep untried elimination, backbone and vivification candidates
+    for next inprocessing round (removed options to disable keeping them)
+  - initial focused mode phase limited by conflicts only (not ticks anymore)
+
+Removing hyper binary resolution provided us with one more bit for encoding
+literals as virtual binary clauses kept only in watch lists do not have to
+be distinguish between being derived through hyper binary resolution or
+learned through conflict analysis.  The former were often generated in huge
+amounts during failed-literal probing and had to be deleted during clause
+data-base reduction eagerly to avoid cloaking up the memory.  As a
+consequence the solver now supports half a billion ('2^29-1') instead of a
+quarter billion ('2^28-1') variables in versions with hyper resolution.
+
 Version sc2022-hyper
 --------------------
 

VERSION

@@ -1 +1 @@
-sc2022-hyper
+sc2022-light

src/ands.c

@@ -73,7 +73,7 @@ kissat_find_and_gate (kissat * solver, unsigned lit, unsigned negative)
       assert (marks[not_other]);
       marks[not_other] = 0;
     }
-  watch tmp = kissat_binary_watch (0, false, false);
+  watch tmp = kissat_binary_watch (0, false);
   watches *watches = &WATCHES (lit);
   for (all_binary_large_watches (watch, *watches))
     {

src/assign.h

@@ -8,26 +8,21 @@
 
 #define INVALID_LEVEL UINT_MAX
 
-#define MAX_LEVEL ((1u<<28)-1)
-#define MAX_TRAIL ((1u<<30)-1)
-
 typedef struct assigned assigned;
 struct clause;
 
 struct assigned
 {
-  unsigned level:28;
+  unsigned level;
+  unsigned trail;
 
   bool analyzed:1;
+  bool binary:1;
   bool poisoned:1;
+  bool redundant:1;
   bool removable:1;
   bool shrinkable:1;
 
-  unsigned trail:30;
-
-  bool binary:1;
-  bool redundant:1;
-
   unsigned reason;
 };
 

src/backbone.c

@@ -619,8 +619,7 @@ compute_backbone (kissat * solver)
 		  "inconsistent binary clauses");
   else
     {
-      if (GET_OPTION (backbonekeep))
-	keep_backbone_candidates (solver, &candidates);
+      keep_backbone_candidates (solver, &candidates);
 #if defined(METRICS) && (!defined(QUIET) || !defined(NDEBUG))
       assert (implied_before <= solver->statistics.backbone_implied);
 #endif

src/clause.c

@@ -73,7 +73,7 @@ new_binary_clause (kissat * solver,
   assert (first != second);
   assert (first != NOT (second));
   assert (!original || !redundant);
-  kissat_watch_binary (solver, redundant, false, first, second);
+  kissat_watch_binary (solver, redundant, first, second);
   if (!redundant)
     {
       kissat_mark_added_literal (solver, first);
@@ -204,17 +204,14 @@ kissat_delete_clause (kissat * solver, clause * c)
 }
 
 void
-kissat_delete_binary (kissat * solver,
-		      bool redundant, bool hyper, unsigned a, unsigned b)
+kissat_delete_binary (kissat * solver, bool redundant, unsigned a, unsigned b)
 {
   LOGBINARY (a, b, "delete");
   if (!redundant)
     {
       kissat_mark_removed_literal (solver, a);
       kissat_mark_removed_literal (solver, b);
     }
-  else if (hyper)
-    DEC (hyper_binaries);
   REMOVE_CHECKER_BINARY (a, b);
   DELETE_BINARY_FROM_PROOF (a, b);
   dec_clause (solver, redundant);

src/clause.h

@@ -85,8 +85,8 @@ void kissat_sort_literals (struct kissat *, unsigned size, unsigned *lits);
 void kissat_connect_clause (struct kissat *, clause *);
 
 clause *kissat_delete_clause (struct kissat *, clause *);
-void kissat_delete_binary (struct kissat *,
-			   bool redundant, bool hyper, unsigned, unsigned);
+void kissat_delete_binary (struct kissat *, bool redundant, unsigned,
+			   unsigned);
 
 void kissat_mark_clause_as_garbage (struct kissat *, clause *);
 

src/collect.c

@@ -14,7 +14,7 @@
 #include <string.h>
 
 static void
-flush_watched_clauses_by_literal (kissat * solver, litpairs * hyper,
+flush_watched_clauses_by_literal (kissat * solver,
 				  unsigned lit, bool compact, reference start)
 {
   assert (start != INVALID_REF);
@@ -45,39 +45,25 @@ flush_watched_clauses_by_literal (kissat * solver, litpairs * hyper,
 	  if (lit_fixed > 0 || other_fixed > 0 || mother == INVALID_LIT)
 	    {
 	      if (lit < other)
-		kissat_delete_binary (solver,
-				      head.binary.redundant,
-				      head.binary.hyper, lit, other);
+		kissat_delete_binary (solver, head.binary.redundant, lit,
+				      other);
 	    }
 	  else
 	    {
 	      assert (!lit_fixed);
 	      assert (!other_fixed);
 
-	      if (head.binary.hyper)
-		{
-		  assert (head.binary.redundant);
-		  assert (mlit != INVALID_LIT);
-		  assert (mother != INVALID_LIT);
-		  if (lit < other)
-		    {
-		      const litpair litpair = kissat_litpair (lit, other);
-		      PUSH_STACK (*hyper, litpair);
-		      LOGBINARY (lit, other, "saved SRC hyper");
-		    }
-		}
-	      else
-		{
-		  head.binary.lit = mother;
-		  *q++ = head;
+	      {
+		head.binary.lit = mother;
+		*q++ = head;
 #ifdef LOGGING
-		  if (lit < other)
-		    {
-		      LOGBINARY (lit, other, "SRC");
-		      LOGBINARY (mlit, mother, "DST");
-		    }
+		if (lit < other)
+		  {
+		    LOGBINARY (lit, other, "SRC");
+		    LOGBINARY (mlit, mother, "DST");
+		  }
 #endif
-		}
+	      }
 	    }
 	}
       else
@@ -127,68 +113,18 @@ flush_watched_clauses_by_literal (kissat * solver, litpairs * hyper,
     assert (mlit == lit);
 }
 
-static void
-flush_hyper_binary_watches (kissat * solver, litpairs * hyper, bool compact)
-{
-  assert (!solver->probing);
-  const litpair *const end = END_STACK (*hyper);
-  const value *const values = solver->values;
-  size_t flushed = 0;
-  for (const litpair * p = BEGIN_STACK (*hyper); p != end; p++)
-    {
-      const unsigned lit = p->lits[0];
-      const unsigned other = p->lits[1];
-      assert (lit < other);
-
-      const value lit_value = values[lit];
-      const value other_value = values[other];
-
-      assert (!lit_value || LEVEL (lit));
-      assert (!other_value || LEVEL (other));
-
-      if (((lit_value < 0 && other_value > 0) ||
-	   ((lit_value > 0 && other_value < 0))))
-	{
-	  LOGBINARY (lit, other, "keeping potential reason hyper SRC");
-	  const unsigned mlit = kissat_map_literal (solver, lit, compact);
-	  const unsigned mother = kissat_map_literal (solver, other, compact);
-	  LOGBINARY (mlit, mother, "keeping potential reason hyper DST");
-	  kissat_watch_other (solver, true, true, mlit, mother);
-	  kissat_watch_other (solver, true, true, mother, mlit);
-	}
-      else
-	{
-	  LOGBINARY (lit, other, "flushing hyper SRC");
-	  kissat_delete_binary (solver, true, true, lit, other);
-	  flushed++;
-	}
-    }
-  if (flushed)
-    kissat_phase (solver, "collect",
-		  GET (garbage_collections),
-		  "flushed %zu unused hyper binary clauses %.0f%%",
-		  flushed, kissat_percent (flushed, SIZE_STACK (*hyper)));
-  (void) flushed;
-}
-
 static void
 flush_all_watched_clauses (kissat * solver, bool compact, reference start)
 {
   assert (solver->watching);
   LOG ("starting to flush watches at clause[%" REFERENCE_FORMAT "]", start);
-  litpairs hyper;
-  INIT_STACK (hyper);
   for (all_variables (idx))
     {
       const unsigned lit = LIT (idx);
-      flush_watched_clauses_by_literal (solver, &hyper, lit, compact, start);
+      flush_watched_clauses_by_literal (solver, lit, compact, start);
       const unsigned not_lit = NOT (lit);
-      flush_watched_clauses_by_literal (solver, &hyper,
-					not_lit, compact, start);
+      flush_watched_clauses_by_literal (solver, not_lit, compact, start);
     }
-  LOG ("saved %zu hyper binary watches", SIZE_STACK (hyper));
-  flush_hyper_binary_watches (solver, &hyper, compact);
-  RELEASE_STACK (hyper);
 }
 
 static void
@@ -511,7 +447,7 @@ sparse_sweep_garbage_clauses (kissat * solver, bool compact, reference start)
 
 	  const bool redundant = dst->redundant;
 	  LOGBINARY (mfirst, msecond, "DST");
-	  kissat_watch_binary (solver, redundant, false, mfirst, msecond);
+	  kissat_watch_binary (solver, redundant, mfirst, msecond);
 
 	  if (dst->reason)
 	    {

src/dense.c

@@ -70,8 +70,7 @@ flush_large_watches (kissat * solver,
 		  if (lit < other)
 		    {
 		      const bool red = watch.binary.redundant;
-		      const bool hyper = watch.binary.hyper;
-		      kissat_delete_binary (solver, red, hyper, lit, other);
+		      kissat_delete_binary (solver, red, lit, other);
 		      collected++;
 		    }
 		}
@@ -143,8 +142,7 @@ resume_watching_binaries_after_elimination (kissat * solver,
       else
 	{
 	  const bool redundant = watch.binary.redundant;
-	  const bool hyper = watch.binary.hyper;
-	  kissat_delete_binary (solver, redundant, hyper, first, second);
+	  kissat_delete_binary (solver, redundant, first, second);
 #ifdef LOGGING
 	  flushed_eliminated++;
 #endif
@@ -198,11 +196,11 @@ resume_watching_irredundant_binaries (kissat * solver, litpairs * binaries)
       assert (!ELIMINATED (IDX (second)));
 
       watches *first_watches = all_watches + first;
-      watch first_watch = kissat_binary_watch (second, false, false);
+      watch first_watch = kissat_binary_watch (second, false);
       PUSH_WATCHES (*first_watches, first_watch);
 
       watches *second_watches = all_watches + second;
-      watch second_watch = kissat_binary_watch (first, false, false);
+      watch second_watch = kissat_binary_watch (first, false);
       PUSH_WATCHES (*second_watches, second_watch);
 
 #ifdef LOGGING