updated internal development

arminbiere · Sep 12, 2024 · 21f1459 · 21f1459
1 parent 36acc9e
commit 21f1459
Show file tree

Hide file tree

Showing 8 changed files with 144 additions and 62 deletions.
diff --git a/NEWS.md b/NEWS.md
@@ -1,3 +1,15 @@
+Version 4.0.1
+-------------
+
+  - updated README to point to the 2024 system description
+  - removed redundant line in congruence closure
+  - fixed proof chain generation for matching ITE
+  - fixed getting size of watches for `--compact`
+  - more precise completion in congruence
+  - writing DIMACS to `<stdout>` with `-o -`
+  - fixed reporting in congruence
+  - fixed DIMACS writing
+
 Version 4.0.0
 -------------
 

diff --git a/README.md b/README.md
@@ -13,19 +13,35 @@ Run `./configure && make test` to configure, build and test in `build`.
 
 Binaries are provided with each major [release](https://github.com/arminbiere/kissat/releases/).
 
-You can get more information about Kissat in the last solver description for the SAT Competition 2022:
-
-<a href="https://cca.informatik.uni-freiburg.de/biere/index.html#publications">Armin Biere</a> and <a
-href="https://cca.informatik.uni-freiburg.de/fleury/index.html#publications">Mathias Fleury</a>.
-<a href="https://cca.informatik.uni-freiburg.de/papers/BiereFleury-SAT-Competition-2022-solvers.pdf">Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022</a>.
-In <i>Proc.&nbsp;of SAT Competition 2022 - Solver and Benchmark Descriptions</i>,
-Tomas Balyo, Marijn Heule, Markus Iser, Matti J&auml;rvisalo, Martin Suda (editors),
-vol.&nbsp;B-2022-1 of Department of Computer Science Report Series B,
-pages 10-11,
-University of Helsinki, 2022.
+You can get more information about Kissat in the last solver description for the SAT Competition 2024:
+
+<p>
+<a href="https://cca.informatik.uni-freiburg.de/biere/index.html#publications">Armin Biere</a>,
+<a href="/biere/index.html">Tobias Faller</a>,
+Katalin Fazekas,
+<a href="https://cca.informatik.uni-freiburg.de/fleury/index.html">Mathias Fleury</a>,
+Nils Froleyks
+and
+<a href="https://cca.informatik.uni-freiburg.de/pollittf.html">Florian Pollitt</a>
 <br>
-[ <a href="https://cca.informatik.uni-freiburg.de/papers/BiereFleury-SAT-Competition-2022-solvers.pdf">paper</a>
-| <a href="https://cca.informatik.uni-freiburg.de/papers/BiereFleury-SAT-Competition-2022-solvers.bib">bibtex</a>
+<a href="https://cca.informatik.uni-freiburg.de/papers/BiereFallerFazekasFleuryFroleyksPollitt-SAT-Competition-2024-solvers.pdf">CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024</a>
+<br>
+<i>Proc.&nbsp;SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions</i>
+<br>
+Marijn Heule, Markus Iser, Matti J&auml;rvisalo, Martin Suda (editors)
+<br>
+Department of Computer Science Report Series B
+<br>
+vol.&nbsp;B-2024-1,
+pages 8-10,
+University of Helsinki 2024
+<br>
+[ <a href="https://cca.informatik.uni-freiburg.de/papers/BiereFallerFazekasFleuryFroleyksPollitt-SAT-Competition-2024-solvers.pdf">paper</a>
+| <a href="https://cca.informatik.uni-freiburg.de/papers/BiereFallerFazekasFleuryFroleyksPollitt-SAT-Competition-2024-solvers.bib">bibtex</a>
+| <a href="https://github.com/arminbiere/cadical">cadical</a>
+| <a href="https://github.com/arminbiere/kissat">kissat</a>
+| <a href="https://github.com/arminbiere/gimsatul">gimsatul</a>
 ]
+</p>
 
 See [NEWS.md](NEWS.md) for feature updates.
diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-4.0.0
+4.0.1
diff --git a/src/application.c b/src/application.c
@@ -809,30 +809,54 @@ static int run_application (kissat *solver, int argc, char **argv,
   close_proof (&application);
 #endif
   kissat_section (solver, "result");
-  if (res == 20) {
-    printf ("s UNSATISFIABLE\n");
-    fflush (stdout);
-  } else if (res == 10) {
-#ifndef NDEBUG
-    if (GET_OPTION (check))
-      kissat_check_satisfying_assignment (solver);
-#endif
-    printf ("s SATISFIABLE\n");
-    fflush (stdout);
-    if (application.witness)
-      kissat_print_witness (solver, application.max_var,
-                            application.partial);
+  if (application.output_path && !strcmp (application.output_path, "-")) {
+    const char *status;
+    if (res == 20)
+      status = "UNSATISFIABLE";
+    else if (res == 10)
+      status = "SATISFIABLE";
+    else
+      status = "UNKNOWN";
+    kissat_message (solver,
+                    "not printing 's %s' status line "
+                    "when writing DIMACS to '<stdout>'",
+                    status);
   } else {
-    printf ("s UNKNOWN\n");
-    fflush (stdout);
+    if (res == 20) {
+      printf ("s UNSATISFIABLE\n");
+      fflush (stdout);
+    } else if (res == 10) {
+#ifndef NDEBUG
+      if (GET_OPTION (check))
+        kissat_check_satisfying_assignment (solver);
+#endif
+      printf ("s SATISFIABLE\n");
+      fflush (stdout);
+      if (application.witness)
+        kissat_print_witness (solver, application.max_var,
+                              application.partial);
+    } else {
+      printf ("s UNKNOWN\n");
+      fflush (stdout);
+    }
   }
   if (application.output_path) {
     // TODO want to use 'struct file' from 'file.h'?
-    FILE *file = fopen (application.output_path, "w");
-    if (!file)
-      ERROR ("could not write DIMACS file '%s'", application.output_path);
+    const char *path = application.output_path;
+    bool close_file;
+    FILE *file;
+    if (!strcmp (path, "-")) {
+      close_file = false;
+      file = stdout;
+    } else {
+      close_file = true;
+      file = fopen (path, "w");
+      if (!file)
+        ERROR ("could not write DIMACS file '%s'", path);
+    }
     kissat_write_dimacs (solver, file);
-    fclose (file);
+    if (close_file)
+      fclose (file);
   }
 #ifndef QUIET
   kissat_print_statistics (solver);

diff --git a/src/congruence.c b/src/congruence.c
@@ -834,8 +834,6 @@ static void add_binary_clause (closure *closure, unsigned a, unsigned b) {
     unit = b;
   else if (!a_value && b_value < 0)
     unit = a;
-  else if (a == b)
-    unit = a;
   if (unit != INVALID_LIT) {
     (void) !learn_congruence_unit (closure, unit);
     return;
@@ -1259,7 +1257,7 @@ static void add_ite_matching_proof_chain (closure *closure, gate *g,
   PUSH_STACK (*unsimplified, cond);
   SIMPLIFY_AND_ADD_TO_PROOF_CHAIN ();
   unsimplified->end--;
-  PUSH_STACK (*unsimplified, cond);
+  PUSH_STACK (*unsimplified, not_cond);
   SIMPLIFY_AND_ADD_TO_PROOF_CHAIN ();
   unsimplified->end--;
   SIMPLIFY_AND_ADD_TO_PROOF_CHAIN ();

diff --git a/src/factor.c b/src/factor.c
@@ -270,7 +270,7 @@ static double distinct_paths (factoring *factoring, unsigned src_lit,
     const unsigned signed_src_lit = src_lit ^ sign;
     watches *const watches = &WATCHES (signed_src_lit);
     uint64_t ticks =
-        1 + kissat_cache_lines (SIZE_STACK (*watches), sizeof (watch));
+        1 + kissat_cache_lines (SIZE_WATCHES (*watches), sizeof (watch));
     for (all_binary_large_watches (watch, *watches)) {
       if (watch.type.binary) {
         const unsigned other = watch.binary.lit;
@@ -559,7 +559,7 @@ static void factorize_next (factoring *factoring, unsigned next,
         assert (min_lit != INVALID_LIT);
         watches *min_watches = all_watches + min_lit;
         unsigned c_size = c->size;
-        ticks += 1 + kissat_cache_lines (SIZE_STACK (*min_watches),
+        ticks += 1 + kissat_cache_lines (SIZE_WATCHES (*min_watches),
                                          sizeof (watch));
         for (all_binary_large_watches (min_watch, *min_watches)) {
           if (min_watch.type.binary)
@@ -893,7 +893,7 @@ adjust_scores_and_phases_of_fresh_varaibles (factoring *factoring) {
   }
 }
 
-static void run_factorization (kissat *solver, uint64_t limit) {
+static bool run_factorization (kissat *solver, uint64_t limit) {
   factoring factoring;
   init_factoring (solver, &factoring, limit);
   schedule_factorization (&factoring);
@@ -903,7 +903,7 @@ static void run_factorization (kissat *solver, uint64_t limit) {
 #endif
   uint64_t *ticks = &solver->statistics.factor_ticks;
   kissat_extremely_verbose (
-      solver, "factorization limit of %" PRIu64 " ticks", limit);
+      solver, "factorization limit of %" PRIu64 " ticks", limit - *ticks);
   while (!done && !kissat_empty_heap (&factoring.schedule)) {
     const unsigned first =
         kissat_pop_max_heap (solver, &factoring.schedule);
@@ -946,9 +946,11 @@ static void run_factorization (kissat *solver, uint64_t limit) {
     }
     release_quotients (&factoring);
   }
+  bool completed = kissat_empty_heap (&factoring.schedule);
   adjust_scores_and_phases_of_fresh_varaibles (&factoring);
   release_factoring (&factoring);
   REPORT (!factored, 'f');
+  return completed;
 }
 
 static void connect_clauses_to_factor (kissat *solver) {
@@ -1069,8 +1071,14 @@ void kissat_factor (kissat *solver) {
   if (!GET_OPTION (factor))
     return;
   statistics *s = &solver->statistics;
-  if (solver->limits.factor.marked >= s->literals_factor)
+  if (solver->limits.factor.marked >= s->literals_factor) {
+    kissat_extremely_verbose (
+        solver,
+        "factorization skipped as no literals have been marked to be added "
+        "(%" PRIu64 " < %" PRIu64,
+        solver->limits.factor.marked, s->literals_factor);
     return;
+  }
   START (factor);
   INC (factorizations);
   kissat_phase (solver, "factorization", GET (factorizations),
@@ -1089,33 +1097,40 @@ void kissat_factor (kissat *solver) {
   }
 #ifndef QUIET
   struct {
-    int64_t variables, clauses, ticks;
+    int64_t variables, binary, clauses, ticks;
   } before, after, delta;
   before.variables = s->variables_extension + s->variables_original;
-  before.clauses = BINARY_CLAUSES;
+  before.binary = BINARY_CLAUSES;
+  before.clauses = IRREDUNDANT_CLAUSES;
   before.ticks = s->factor_ticks;
 #endif
   kissat_enter_dense_mode (solver, 0);
   connect_clauses_to_factor (solver);
-  run_factorization (solver, limit);
+  bool completed = run_factorization (solver, limit);
   kissat_resume_sparse_mode (solver, false, 0);
 #ifndef QUIET
   after.variables = s->variables_extension + s->variables_original;
-  after.clauses = BINARY_CLAUSES;
+  after.binary = BINARY_CLAUSES;
+  after.clauses = IRREDUNDANT_CLAUSES;
   after.ticks = s->factor_ticks;
   delta.variables = after.variables - before.variables;
+  delta.binary = before.binary - after.binary;
   delta.clauses = before.clauses - after.clauses;
-  delta.ticks = before.ticks - after.ticks;
+  delta.ticks = after.ticks - before.ticks;
   kissat_very_verbose (solver, "used %f million factorization ticks",
                        delta.ticks * 1e-6);
   kissat_phase (solver, "factorization", GET (factorizations),
                 "introduced %" PRId64 " extension variables %.0f%%",
                 delta.variables,
                 kissat_percent (delta.variables, before.variables));
   kissat_phase (solver, "factorization", GET (factorizations),
-                "removed %" PRId64 " binary clauses %.0f%%", delta.clauses,
+                "removed %" PRId64 " binary clauses %.0f%%", delta.binary,
+                kissat_percent (delta.binary, before.binary));
+  kissat_phase (solver, "factorization", GET (factorizations),
+                "removed %" PRId64 " large clauses %.0f%%", delta.clauses,
                 kissat_percent (delta.clauses, before.clauses));
 #endif
-  solver->limits.factor.marked = s->literals_factor;
+  if (completed)
+    solver->limits.factor.marked = s->literals_factor;
   STOP (factor);
 }
diff --git a/src/krite.c b/src/krite.c
@@ -6,18 +6,34 @@
 #include <inttypes.h>
 
 void kissat_write_dimacs (kissat *solver, FILE *file) {
-  fprintf (file, "p cnf %u %" PRIu64 "\n", VARS, BINIRR_CLAUSES);
+  size_t imported = SIZE_STACK (solver->import);
+  if (imported)
+    imported--;
+  fprintf (file, "p cnf %zu %" PRIu64 "\n", imported, BINIRR_CLAUSES);
   assert (solver->watching);
-  for (all_literals (ilit))
-    for (all_binary_large_watches (watch, WATCHES (ilit)))
-      if (watch.type.binary) {
-        const unsigned iother = watch.binary.lit;
-        if (iother < ilit)
-          continue;
-        const int elit = kissat_export_literal (solver, ilit);
-        const int eother = kissat_export_literal (solver, iother);
-        fprintf (file, "%d %d 0\n", elit, eother);
-      }
+  if (solver->watching) {
+    for (all_literals (ilit))
+      for (all_binary_blocking_watches (watch, WATCHES (ilit)))
+        if (watch.type.binary) {
+          const unsigned iother = watch.binary.lit;
+          if (iother < ilit)
+            continue;
+          const int elit = kissat_export_literal (solver, ilit);
+          const int eother = kissat_export_literal (solver, iother);
+          fprintf (file, "%d %d 0\n", elit, eother);
+        }
+  } else {
+    for (all_literals (ilit))
+      for (all_binary_large_watches (watch, WATCHES (ilit)))
+        if (watch.type.binary) {
+          const unsigned iother = watch.binary.lit;
+          if (iother < ilit)
+            continue;
+          const int elit = kissat_export_literal (solver, ilit);
+          const int eother = kissat_export_literal (solver, iother);
+          fprintf (file, "%d %d 0\n", elit, eother);
+        }
+  }
   for (all_clauses (c))
     if (!c->garbage && !c->redundant) {
       for (all_literals_in_clause (ilit, c)) {

diff --git a/test/testsolve.c b/test/testsolve.c
@@ -11,11 +11,12 @@ static void schedule_solve_job_with_option (int expected, const char *opt,
     tissat_warning ("Skipping unreadable '%s'", path);
     return;
   }
-  char cmd[256];
-  assert (strlen (path) + strlen (opt) + 32 < sizeof cmd);
-  sprintf (cmd, "%s%s", opt, path);
-  assert (strlen (cmd) < sizeof cmd);
+  size_t len = strlen (opt) + strlen (path) + 1;
+  char * cmd = malloc (len);
+  strcpy (cmd, opt);
+  strcat (cmd, path);
   tissat_schedule_application (expected, cmd);
+  free (cmd);
   scheduled++;
 }