imported sc2022-bulky

LICENSE

@@ -1,4 +1,5 @@
 Copyright (c) 2019-2021 Armin Biere, Johannes Kepler University Linz, Austria
+Copyright (c) 2021-2022 Armin Biere, University of Freiburg, Germany
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

NEWS.md

@@ -0,0 +1,29 @@
+Version sc2022-bulky
+--------------------
+
+Compared to version 2.0.2 and thus the version submitted to the competition
+in 2021 we added the following features:
+
+  - added ACIDS branching variable heuristics (disabled by default)
+  - added CHB variable branching heuristic (but disabled by default)
+    inspired by the success of 'kissat_mab' in the SAT Competition 2021
+  - faster randomization of phases in the Kitten sub-solver
+  - using literal flipping for faster refinement during sweeping
+  - literal flipping in a partial model obtained by Kitten
+  - disabled priority queue for variable elimination (elimination attempts
+    of variables in the given variable order is now enforced)
+  - disabled by default reusing the trail during restarts
+  - disabled by default hyper ternary resolution
+  - obtain initial local search assignment through propagation
+    (similar to the "warming-up" idea of Donald Knuth and how Shaowei Cai
+     for "ReasonLS" solvers initializes the local search)
+  - actual watch replacement of true literals during unit propagation instead
+    of just updating the blocking literal (as suggested by Norbert Manthey)
+  - fixed clause length and variable occurrences during variable elimination
+    instead of increasing the limits dynamically (but very rarely actually)
+
+
+Version 2.0.2
+-------------
+
+- removed 'src/makefile' from git (set during configuration instead)

README.md

@@ -1,5 +1,5 @@
 [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
-[![Build Status](https://travis-ci.com/arminbiere/kissat.svg?branch=master)](https://travis-ci.com/arminbiere/kissat)
+[![Build Status](https://app.travis-ci.com/github/arminbiere/kissat.svg?branch=master)](https://app.travis-ci.com/github/arminbiere/kissat)
 
 The Kissat SAT Solver
 =====================

VERSION

@@ -1 +1 @@
-2.0.1
+sc2022-bulky

configure

@@ -685,3 +685,12 @@ sed \
   -e "s#@AR@#$AR#" \
   -e "s#@GOALS@#$goals#" \
   ../makefile.in > makefile
+
+if [ -f ../src/makefile ]
+then
+  msg "removing src/makefile"
+  rm -f ../src/makefile
+fi
+
+msg "linking src/makefile"
+ln -s $ROOT/makefile ../src

scripts/prepare-competition.sh

@@ -99,16 +99,13 @@ exec ./build.sh
 EOF
 chmod 755 $starexec_build
 
-for config in default sat unsat
-do 
-
 build=$dir/build/build.sh
 cat <<EOF > $build
 #!/bin/sh
 tar xf ../archive/kissat*
 mv kissat* kissat
 cd kissat
-./configure --competition --$config --test
+./configure --competition --test
 make all || exit 1
 build/tissat || exit 1
 exec install -s build/kissat ../../bin/
@@ -118,22 +115,23 @@ chmod 755 $build
 starexec_run_default=$dir/bin/starexec_run_default
 cat <<EOF >$starexec_run_default
 #!/bin/sh
-exec ./kissat --$config \$1 \$2/proof.out
+exec ./kissat \$1 \$2/proof.out
 EOF
 chmod 755 $starexec_run_default
 
-msg "generated '$config' build and run scripts"
+msg "generated build and run scripts"
+version=`cat VERSION`
 
 description=$dir/starexec_description.txt
 cat <<EOF>$description
-Keep it Simple bare metal SAT solver with $config configuration
+Keep it simple bare metal SAT Solver
 EOF
 msg "included the following description:"
 printf $BOLD
 cat $description
 printf $NORMAL
  
-zipfile=/tmp/$base-$config.zip
+zipfile=/tmp/$base.zip
 rm -f $zipfile
 
 cd $dir
@@ -145,5 +143,3 @@ BYTES="`ls --block-size=1 -s $zipfile 2>/dev/null |awk '{print $1}'`"
 msg "zip file has $BYTES bytes"
 
 echo $zipfile
-
-done

src/allocate.h

@@ -15,6 +15,11 @@ void kissat_dealloc (struct kissat *, void *ptr, size_t n, size_t size);
 void *kissat_realloc (struct kissat *, void *, size_t old, size_t bytes);
 void *kissat_nrealloc (struct kissat *, void *, size_t o, size_t n, size_t);
 
+#define NALLOC(P,N) \
+do { \
+  (P) = kissat_nalloc (solver, (N), sizeof *(P)); \
+} while (0)
+
 #define CALLOC(P,N) \
 do { \
   (P) = kissat_calloc (solver, (N), sizeof *(P)); \

src/analyze.c

@@ -177,6 +177,8 @@ analyze_reason_side_literal (kissat * solver, size_t limit, ward * arena,
 static void
 analyze_reason_side_literals (kissat * solver)
 {
+  if (!GET_OPTION (bump))
+    return;
   if (!GET_OPTION (bumpreasons))
     return;
   if (solver->probing)
@@ -245,21 +247,6 @@ analyze_reason_side_literals (kissat * solver)
        solver->delays.bumpreasons.count);
 }
 
-#if 0
-
-#define RANK_LITERAL_BY_INVERSE_LEVEL(LIT) \
-  (~assigned[IDX (LIT)].level)
-
-static void
-sort_deduced_clause (kissat * solver)
-{
-  unsigneds *clause = &solver->clause;
-  assigned *assigned = solver->assigned;
-  RADIX_STACK (unsigned, unsigned, *clause, RANK_LITERAL_BY_INVERSE_LEVEL);
-}
-
-#else
-
 #define RADIX_SORT_LEVELS_LIMIT 32
 
 #define RANK_LEVEL(A) (A)
@@ -365,8 +352,6 @@ sort_deduced_clause (kissat * solver)
 #endif
 }
 
-#endif
-
 static void
 reset_levels (kissat * solver)
 {
@@ -653,8 +638,8 @@ kissat_analyze (kissat * solver, clause * conflict)
 	}
       if (!EMPTY_STACK (solver->analyzed))
 	{
-	  if (!solver->probing)
-	    kissat_bump (solver);
+	  if (!solver->probing && GET_OPTION (bump))
+	    kissat_bump_analyzed (solver);
 	  kissat_reset_only_analyzed_literals (solver);
 	}
     }

src/ands.c

@@ -41,7 +41,7 @@ kissat_find_and_gate (kissat * solver, unsigned lit, unsigned negative)
 	  const value value = values[other];
 	  if (value > 0)
 	    {
-	      kissat_eliminate_clause (solver, c, INVALID_LIT);
+	      kissat_mark_clause_as_garbage (solver, c);
 	      base = 0;
 	      break;
 	    }

src/application.c

@@ -14,6 +14,8 @@
 #include <string.h>
 #include <unistd.h>
 
+#define SOLVER_NAME "Kissat SAT Solver"
+
 typedef struct application application;
 
 struct application
@@ -261,7 +263,7 @@ parsed_one_option_and_return_zero_exit_code (char *arg)
     }
   if (!strcmp (arg, "--banner"))
     {
-      kissat_banner (0, "KISSAT SAT Solver");
+      kissat_banner (0, SOLVER_NAME);
       return true;
     }
   if (!strcmp (arg, "--build"))
@@ -271,7 +273,8 @@ parsed_one_option_and_return_zero_exit_code (char *arg)
     }
   if (!strcmp (arg, "--copyright"))
     {
-      printf ("%s\n", kissat_copyright ());
+      for (const char **p = kissat_copyright (), *line; (line = *p); p++)
+	printf ("%s\n", line);
       return true;
     }
   if (!strcmp (arg, "--compiler"))
@@ -841,7 +844,7 @@ print_limits (application * application)
 
 static int
 run_application (kissat * solver,
-		 int argc, char **argv, bool * cancel_alarm_ptr)
+		 int argc, char **argv, bool *cancel_alarm_ptr)
 {
   *cancel_alarm_ptr = false;
   if (argc == 2)
@@ -858,7 +861,7 @@ run_application (kissat * solver,
   kissat_section (solver, "banner");
   if (!GET_OPTION (quiet))
     {
-      kissat_banner ("c ", "KISSAT SAT Solver");
+      kissat_banner ("c ", SOLVER_NAME);
       fflush (stdout);
     }
 #endif

src/backbone.c

@@ -396,7 +396,7 @@ compute_backbone (kissat * solver)
   unsigned inconsistent = INVALID_LIT;
 
   SET_EFFORT_LIMIT (ticks_limit, backbone, backbone_ticks,
-		    kissat_linear (1 + solver->active));
+		    1 + solver->active);
 
   size_t round_limit = GET_OPTION (backbonerounds);
   assert (solver->statistics.backbone_computations);

src/backtrack.c

@@ -99,7 +99,7 @@ kissat_backtrack_without_updating_phases (kissat * solver, unsigned new_level)
   unsigned *q = new_end;
   if (solver->stable)
     {
-      heap *scores = &solver->scores;
+      heap *scores = SCORES;
       for (const unsigned *p = q; p != old_end; p++)
 	{
 	  const unsigned lit = *p;
@@ -182,16 +182,12 @@ kissat_backtrack_after_conflict (kissat * solver, unsigned new_level)
   kissat_backtrack_without_updating_phases (solver, new_level);
 }
 
-// TODO check whether this can be merged with
-// 'kissat_restart_and_flush_trail'.
-
 void
 kissat_backtrack_propagate_and_flush_trail (kissat * solver)
 {
   if (solver->level)
     {
       assert (solver->watching);
-      assert (solver->level > 0);
       kissat_backtrack_in_consistent_state (solver, 0);
 #ifndef NDEBUG
       clause *conflict =

src/backward.c

@@ -29,7 +29,7 @@ backward_subsume_lits (kissat * solver, reference ignore,
 
   assert (min_lit != INVALID_LIT);
 
-  const unsigned occlim = solver->bounds.subsume.occurrences;
+  const unsigned occlim = GET_OPTION (subsumeocclim);
   if (min_occs > occlim)
     return true;
 
@@ -40,7 +40,7 @@ backward_subsume_lits (kissat * solver, reference ignore,
   const value *const values = solver->values;
   ward *const arena = BEGIN_STACK (solver->arena);
 
-  const unsigned clslim = solver->bounds.subsume.clause_size;
+  const unsigned clslim = GET_OPTION (subsumeclslim);
 
   const unsigned match =
     (size > 2 ? INVALID_LIT : (lits[0] ^ lits[1] ^ min_lit));
@@ -90,7 +90,6 @@ backward_subsume_lits (kissat * solver, reference ignore,
 	      INC (duplicated);
 	      kissat_disconnect_binary (solver, other, min_lit);
 	      kissat_delete_binary (solver, false, false, min_lit, other);
-	      kissat_update_after_removing_variable (solver, IDX (other));
 	      q--;
 	    }
 	  else
@@ -136,8 +135,6 @@ backward_subsume_lits (kissat * solver, reference ignore,
 		{
 		  LOGCLS (c, "satisfied by %s", LOGLIT (lit));
 		  kissat_mark_clause_as_garbage (solver, c);
-		  kissat_update_after_removing_clause (solver, c,
-						       INVALID_LIT);
 		  break;
 		}
 	      if (value < 0)
@@ -180,7 +177,6 @@ backward_subsume_lits (kissat * solver, reference ignore,
 	      INC (subsumed);
 	      INC (backward_subsumed);
 	      kissat_mark_clause_as_garbage (solver, c);
-	      kissat_update_after_removing_clause (solver, c, INVALID_LIT);
 	      q--;
 	      continue;
 	    }
@@ -206,7 +202,6 @@ backward_subsume_lits (kissat * solver, reference ignore,
 	  if (satisfied)
 	    {
 	      kissat_mark_clause_as_garbage (solver, c);
-	      kissat_update_after_removing_clause (solver, c, INVALID_LIT);
 	      q--;
 	      continue;
 	    }
@@ -272,7 +267,6 @@ backward_subsume_lits (kissat * solver, reference ignore,
 	      q--;
 	    }
 	  kissat_mark_removed_literal (solver, remove);
-	  kissat_update_after_removing_variable (solver, IDX (remove));
 	}
     }
 

src/bits.h

@@ -16,7 +16,7 @@ static inline size_t
 kissat_bits_size_in_words (size_t size)
 {
   assert (sizeof (bits) == 4);
-  return (size >> 5) + ! !(size & 31);
+  return (size >> 5) + !!(size & 31);
 }
 
 static inline bool
@@ -29,7 +29,7 @@ kissat_get_bit (const bits * bits, size_t size, size_t bit)
   const unsigned y = (bit & 31);
   const unsigned mask = (1u << y);
   const unsigned masked = word & mask;
-  const bool res = ! !masked;
+  const bool res = !!masked;
   (void) size;
   return res;
 }

src/branching.c

@@ -0,0 +1,56 @@
+#include "internal.h"
+#include "print.h"
+
+#ifndef QUIET
+
+static const char *
+branching_name (kissat * solver, unsigned branching)
+{
+#ifdef NOPTIONS
+  (void) solver;
+#endif
+  return branching ? "CHB" : GET_OPTION (acids) ? "ACIDS" : "VSIDS";
+}
+
+#endif
+
+void
+kissat_init_branching (kissat * solver)
+{
+  if (!GET_OPTION (bump))
+    return;
+
+  solver->branching = GET_OPTION (chb) == 2;
+  kissat_very_verbose (solver,
+		       "will start with %s branching heuristics",
+		       branching_name (solver, solver->branching));
+
+  if (GET_OPTION (chb))
+    {
+      const int emachb = GET_OPTION (emachb);
+      solver->alphachb = 1.0 / emachb;
+      kissat_very_verbose (solver, "CHB branching alpha %g (window %d)",
+			   solver->alphachb, emachb);
+    }
+}
+
+bool
+kissat_toggle_branching (kissat * solver)
+{
+  assert (solver->stable);
+  if (!GET_OPTION (bump))
+    return false;
+  if (GET_OPTION (chb) != 1)
+    return false;
+#ifndef QUIET
+  const unsigned current = solver->branching;
+  const unsigned next = solver->branching = !current;
+  kissat_extremely_verbose (solver,
+			    "switching from %s branching heuristic to %s",
+			    branching_name (solver, current),
+			    branching_name (solver, next));
+#else
+  (void) solver;
+#endif
+  return true;
+}