merged internal sc2024 version

.clang-format

@@ -0,0 +1,4 @@
+AlignEscapedNewlines: DontAlign
+ColumnLimit: 76
+SpaceBeforeParens: Always
+SpaceAfterCStyleCast: true

LICENSE

@@ -1,4 +1,4 @@
-Copyright (c) 2021-2023 Armin Biere, University of Freiburg, Germany
+Copyright (c) 2021-2024 Armin Biere, University of Freiburg, Germany
 Copyright (c) 2019-2021 Armin Biere, Johannes Kepler University Linz, Austria
 
 Permission is hereby granted, free of charge, to any person obtaining a copy

NEWS.md

@@ -1,3 +1,25 @@
+Version sc2024
+--------------
+
+  - fast variable elimination during preprocessing (in `fastel.c`)
+  - lucky phases as in `CaDiCaL` but before and after preprocessing
+    and with unit extraction and SLURM semantics
+  - reason jumping only for formulas with large binary clauses fraction
+  - U-shaped delta scaling of probing and elimination interval 
+  - option `-o <output>` to write simplified formula to a file
+  - dynamically increased reduced-clauses fraction (60% - 90%)
+  - bounded variable addition (in `factor.c`)
+  - clausal congruence closure algorithm (in `congruence.c`)
+  - generic preprocessing phase (using a subset-set of simplifiers)
+  - more vivification (tier0=irredundant,tier1,tier2,tier3)
+  - added `--no-conflicts` as synonym to `--conflicts=0`
+  - optimized and simplified vivification
+
+Version 3.1.1
+-------------
+
+  - configuration option `--safe` disables writing through `popen`
+
 Version 3.1.0
 -------------
 

VERSION

@@ -1 +1 @@
-3.1.1-rc.1
+sc2024

configure

@@ -25,6 +25,7 @@ pic=no
 profile=no
 proofs=yes
 quiet=no
+safe=no
 sat=no
 shared=no
 static=no
@@ -77,13 +78,18 @@ fi
 cat << EOF
 Options used to instrument the code for coverage and performance profiling.
 
-  --coverage       include line coverage code (to be used with 'gcov')
-  --profile        include profiling code (to be used with 'gprof')
+  --coverage        include line coverage code (to be used with 'gcov')
+  --profile         include profiling code (to be used with 'gprof')
 
 For coverage testing it might be useful to enforce different compiler
 optimization levels, i.e., lower than the default '-O3' (without '-g').
   
-  -O[0|1|2|3]      set the optimization level of the compiler explicitly
+  -O[0|1|2|3]       set the optimization level of the compiler explicitly
+
+Writing through 'popen' can be considered harmful in certain library usage.
+
+  --safe            disable the use of writing through 'popen'
+                    (and thus disables writing zipped files too)
 
 We have compile time options which save memory and speed up the solver by
 limiting the size of formulas that can be handled, fix the default
@@ -216,6 +222,8 @@ do
     -O2) optimize=2;;
     -O3) optimize=3;;
 
+    --safe) safe=yes;;
+
     --compact) compact=yes;;
     --no-options) options=no;;
     --quiet) quiet=yes;;
@@ -321,6 +329,7 @@ tissat:
 	\$(MAKE) -C "$BUILD" tissat
 clean:
 	rm -f "$ROOT"/makefile
+	rm -f "$ROOT"/src/makefile
 	-\$(MAKE) -C "$BUILD" clean
 	rm -rf "$BUILD"
 coverage:
@@ -595,6 +604,7 @@ fi
 [ $options = no ] && CFLAGS="$CFLAGS -DNOPTIONS"
 [ $proofs = no ] && CFLAGS="$CFLAGS -DNPROOFS"
 [ $quiet = yes ] && CFLAGS="$CFLAGS -DQUIET"
+[ $safe = yes ] && CFLAGS="$CFLAGS -DSAFE"
 [ $sat = yes ] && CFLAGS="$CFLAGS -DSAT"
 [ $statistics = yes -a $metrics = no ] && CFLAGS="$CFLAGS -DSTATISTICS"
 [ $unsat = yes ] && CFLAGS="$CFLAGS -DUNSAT"

src/analyze.c

@@ -5,9 +5,11 @@
 #include "inline.h"
 #include "learn.h"
 #include "minimize.h"
+#include "print.h"
 #include "rank.h"
 #include "shrink.h"
 #include "sort.h"
+#include "tiers.h"
 
 #include <inttypes.h>
 
@@ -171,12 +173,8 @@ static void analyze_reason_side_literals (kissat *solver) {
     return;
   if (solver->probing)
     return;
-  if (solver->delays.bumpreasons.count) {
-    solver->delays.bumpreasons.count--;
-    LOG ("bump reasons still delayed (%u more times)",
-         solver->delays.bumpreasons.count);
+  if (DELAYING (bumpreasons))
     return;
-  }
   const double decision_rate = AVERAGE (decision_rate);
   const int decision_rate_limit = GET_OPTION (bumpreasonsrate);
   if (decision_rate >= decision_rate_limit) {
@@ -208,21 +206,9 @@ static void analyze_reason_side_literals (kissat *solver) {
       assert (a->analyzed);
       a->analyzed = false;
     }
-    if (solver->delays.bumpreasons.current < UINT_MAX) {
-      solver->delays.bumpreasons.current++;
-      LOG ("solver delay bump reasons interval increased to %u",
-           solver->delays.bumpreasons.current);
-    }
-  } else if (solver->delays.bumpreasons.current) {
-    solver->delays.bumpreasons.current /= 2;
-    LOG ("bump reasons delay interval decreased to %u",
-         solver->delays.bumpreasons.current);
+    BUMP_DELAY (bumpreasons);
   } else
-    LOG ("keeping zero bump reasons delays");
-
-  solver->delays.bumpreasons.count = solver->delays.bumpreasons.current;
-  LOG ("next bump reasons delayed %u times",
-       solver->delays.bumpreasons.count);
+    REDUCE_DELAY (bumpreasons);
 }
 
 #define RADIX_SORT_LEVELS_LIMIT 32
@@ -524,7 +510,18 @@ static void analyze_failed_literal (kissat *solver, clause *conflict) {
   for (all_stack (unsigned, lit, *units))
     kissat_learned_unit (solver, lit);
   CLEAR_STACK (*units);
-  solver->iterating = true;
+  if (!solver->probing) {
+    solver->iterating = true;
+    INC (iterations);
+  }
+}
+
+static void update_tier_limits (kissat *solver) {
+  INC (retiered);
+  kissat_compute_and_set_tier_limits (solver);
+  if (solver->limits.glue.interval < (1u << 16))
+    solver->limits.glue.interval *= 2;
+  solver->limits.glue.conflicts = CONFLICTS + solver->limits.glue.interval;
 }
 
 int kissat_analyze (kissat *solver, clause *conflict) {
@@ -555,7 +552,10 @@ int kissat_analyze (kissat *solver, clause *conflict) {
     } else if ((conflict =
                     kissat_deduce_first_uip_clause (solver, conflict))) {
       reset_analysis_but_not_analyzed_literals (solver);
-      res = 0;
+      INC (conflicts);
+      if (CONFLICTS > solver->limits.glue.conflicts)
+        update_tier_limits (solver);
+      res = 0; // And continue with new conflict analysis.
     } else {
       if (GET_OPTION (minimize)) {
         sort_deduced_clause (solver);

src/application.c

@@ -5,6 +5,7 @@
 #include "error.h"
 #include "internal.h"
 #include "keatures.h"
+#include "krite.h"
 #include "parse.h"
 #include "print.h"
 #include "proof.h"
@@ -22,6 +23,7 @@ typedef struct application application;
 struct application {
   kissat *solver;
   const char *input_path;
+  const char *output_path;
 #ifndef NPROOFS
   const char *proof_path;
   file proof_file;
@@ -43,7 +45,6 @@ static void init_app (application *application, kissat *solver) {
   memset (application, 0, sizeof *application);
   application->solver = solver;
   application->witness = true;
-  application->time = 0;
   application->conflicts = -1;
   application->decisions = -1;
   application->strict = NORMAL_PARSING;
@@ -378,6 +379,9 @@ static bool parse_options (application *application, int argc,
 #if !defined(NPROOFS) || !defined(KISSAT_HAS_COMPRESSION)
   const char *force_option = 0;
 #endif
+  const char *conflicts_option = 0;
+  const char *decisions_option = 0;
+  const char *time_option = 0;
   const char *valstr;
   for (int i = 1; i < argc; i++) {
     const char *arg = argv[i];
@@ -457,30 +461,30 @@ static bool parse_options (application *application, int argc,
     else if ((valstr = kissat_parse_option_name (arg, "time"))) {
       int val;
       if (kissat_parse_option_value (valstr, &val) && val > 0) {
-        if (application->time > 0)
-          ERROR ("multiple '--time=%d' and '%s'", application->time, arg);
+        if (time_option)
+          ERROR ("multiple '%s' and '%s'", time_option, arg);
         application->time = val;
         alarm (val);
       } else
         ERROR ("invalid argument in '%s' (try '-h')", arg);
     } else if ((valstr = kissat_parse_option_name (arg, "conflicts"))) {
       int val;
       if (kissat_parse_option_value (valstr, &val) && val >= 0) {
-        if (application->conflicts >= 0)
-          ERROR ("multiple '--conflicts=%d' and '%s'",
-                 application->conflicts, arg);
+        if (conflicts_option)
+          ERROR ("multiple '%s' and '%s'", conflicts_option, arg);
         kissat_set_conflict_limit (solver, val);
         application->conflicts = val;
+        conflicts_option = arg;
       } else
         ERROR ("invalid argument in '%s' (try '-h')", arg);
     } else if ((valstr = kissat_parse_option_name (arg, "decisions"))) {
       int val;
       if (kissat_parse_option_value (valstr, &val) && val >= 0) {
-        if (application->decisions >= 0)
-          ERROR ("multiple '--decisions=%d' and '%s'",
-                 application->decisions, arg);
+        if (decisions_option)
+          ERROR ("multiple '%s' and '%s'", decisions_option, arg);
         kissat_set_decision_limit (solver, val);
         application->decisions = val;
+        decisions_option = arg;
       } else
         ERROR ("invalid argument in '%s' (try '-h')", arg);
     } else if (!strcmp (arg, "--partial"))
@@ -518,6 +522,24 @@ static bool parse_options (application *application, int argc,
       ERROR ("invalid long option '%s' "
              "(configured with '--no-options')",
              arg);
+#endif
+    else if (!strcmp (arg, "-o")) {
+
+      if (++i == argc)
+        ERROR ("argument to '-o' missing (try '-h')");
+      arg = argv[i];
+      if (application->output_path)
+        ERROR ("multiple output options '-o %s' and '-o %s' (try '-h')",
+               application->output_path, arg);
+      application->output_path = arg;
+    }
+#ifdef NOPTIONS
+    else if (arg[0] == '-' && !arg[2] &&
+             (arg[1] == 'l' || arg[1] == 'q' || arg[1] == 's' ||
+              arg[1] == 'v'))
+      ERROR ("invalid short option '%s' "
+             "(configured with '--no-options')",
+             arg);
 #endif
 #ifdef QUIET
     else if (arg[0] == '-' && !arg[2] &&
@@ -529,14 +551,6 @@ static bool parse_options (application *application, int argc,
       ERROR ("invalid short option '%s' "
              "(configured without '-l' or '-g')",
              arg);
-#endif
-#ifdef NOPTIONS
-    else if (arg[0] == '-' && !arg[2] &&
-             (arg[1] == 'l' || arg[1] == 'q' || arg[1] == 's' ||
-              arg[1] == 'v'))
-      ERROR ("invalid short option '%s' "
-             "(configured with '--no-options')",
-             arg);
 #endif
     else if (arg[0] == '-' && arg[1])
       ERROR ("invalid short option '%s' (try '-h')", arg);
@@ -794,22 +808,31 @@ static int run_application (kissat *solver, int argc, char **argv,
 #ifndef NPROOFS
   close_proof (&application);
 #endif
-  if (res) {
-    kissat_section (solver, "result");
-    if (res == 20) {
-      printf ("s UNSATISFIABLE\n");
-      fflush (stdout);
-    } else if (res == 10) {
+  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 (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);
+    kissat_write_dimacs (solver, file);
+    fclose (file);
   }
 #ifndef QUIET
   kissat_print_statistics (solver);

src/assign.c

@@ -35,7 +35,7 @@ void kissat_assign_binary (kissat *solver, unsigned lit, unsigned other) {
   const unsigned other_idx = IDX (other);
   struct assigned *a = assigned + other_idx;
   unsigned level = a->level;
-  if (level && a->binary) {
+  if (GET_OPTION (jumpreasons) && level && a->binary) {
     LOGBINARY (lit, other, "jumping %s reason", LOGLIT (lit));
     INC (jumped_reasons);
     other = a->reason;

src/assign.h

@@ -7,6 +7,7 @@
 #define UNIT_REASON (DECISION_REASON - 1)
 
 #define INVALID_LEVEL UINT_MAX
+#define INVALID_TRAIL UINT_MAX
 
 typedef struct assigned assigned;
 struct clause;
@@ -28,7 +29,7 @@ struct assigned {
   (assert (VALID_INTERNAL_LITERAL (LIT)), solver->assigned + IDX (LIT))
 
 #define LEVEL(LIT) (ASSIGNED (LIT)->level)
-
+#define TRAIL(LIT) (ASSIGNED (LIT)->trail)
 #define REASON(LIT) (ASSIGNED (LIT)->reason)
 
 #ifndef FAST_ASSIGN

src/backbone.c

@@ -342,7 +342,6 @@ static unsigned compute_backbone (kissat *solver) {
   unsigned inconsistent = INVALID_LIT;
 
   SET_EFFORT_LIMIT (ticks_limit, backbone, backbone_ticks);
-
   size_t round_limit = GET_OPTION (backbonerounds);
   assert (solver->statistics.backbone_computations);
   round_limit *= solver->statistics.backbone_computations;

src/backbone.h

@@ -1,6 +1,8 @@
 #ifndef _backbone_h_INCLUDED
 #define _backbone_h_INCLUDED
 
+#include <stdbool.h>
+
 struct kissat;
 void kissat_binary_clauses_backbone (struct kissat *);
 

src/build.c

@@ -12,7 +12,7 @@ const char *kissat_id (void) { return ID; }
 const char *kissat_compiler (void) { return COMPILER; }
 
 static const char *copyright_lines[] = {
-    "Copyright (c) 2021-2023 Armin Biere University of Freiburg",
+    "Copyright (c) 2021-2024 Armin Biere University of Freiburg",
     "Copyright (c) 2019-2021 Armin Biere Johannes Kepler University Linz",
     0};