release 3.1.0 = SAT Competition 2023 submission merged

LICENSE

@@ -1,5 +1,5 @@
+Copyright (c) 2021-2023 Armin Biere, University of Freiburg, Germany
 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

@@ -1,3 +1,18 @@
+Version 3.1.0
+-------------
+
+  - replaced `__gcov_flush` by `__gcov_dump`
+  - moved to `clang-format` instead of `indent`
+  - removed warnings for MacOS (latest clang)
+  - added back irredundant clause vivification
+  - reason jumping during binary reason clause chains
+  - more focused sweeping (more effort and unscheduling)
+  - probing and elimination preprocessing initially
+  - relevancy and occurrence score based variable elimination
+  - faster parsing and proof writing
+  - no redundant virtual clauses anymore
+  - doubled allowed maximum variable index to more than 1 billion variables
+
 Version 3.0.0
 -------------
 

README.md

@@ -1,4 +1,5 @@
 [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
+[![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
 =====================
@@ -11,21 +12,4 @@ Coincidentally "kissat" also means "cats" in Finnish.
 
 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.
-<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>
-]
-
 See [NEWS.md](NEWS.md) for feature updates.

VERSION

@@ -1 +1 @@
-3.0.0
+3.1.0

configure

@@ -325,11 +325,11 @@ clean:
 	rm -rf "$BUILD"
 coverage:
 	\$(MAKE) -C "$BUILD" coverage
-indent:
-	\$(MAKE) -C "$BUILD" indent
+format:
+	\$(MAKE) -C "$BUILD" format
 test:
 	\$(MAKE) -C "$BUILD" test
-.PHONY: all clean coverage indent kissat test tissat
+.PHONY: all clean coverage format kissat test tissat
 EOF
 
 [ $statistics = no -a $metrics = yes ] && \

makefile.in

@@ -42,8 +42,8 @@ clean:
 coverage:
 	@gcov -o . -s ../src/*.[ch] 2>&1 | \
 	../scripts/filter-coverage-output.sh
-indent:
-	indent ../*/*.[ch]
+format:
+	clang-format -i ../*/*.[ch]
 
 kissat: main.o $(APPOBJ) libkissat.a makefile
 	$(LD) -o $@ main.o $(APPOBJ) $(LIBS) -lm

scripts/build-and-test-all-configurations.sh

@@ -10,13 +10,17 @@ usage: $binary [ <option> ]
 
 where '<option>' is one of the following
 
-  -h  print this command line option summary
-  -n  only print and fake building and testing
-  -1  single configuration option mode (default)
-  -2  double configuration options mode
-  -3  triple configuration options mode
-  -f  force '--coverage' with 'clang'
-  -j  build and test in parallel
+  -h             print this command line option summary
+  -1             single configuration option mode (default)
+  -2             double configuration options mode
+  -3             triple configuration options mode
+  -j             build and test in parallel
+
+  --fake         only print and fake building and testing
+  --force        force '--coverage' with 'clang'
+
+  --no-coverage  disable coverage
+  --no-pedantic  disable pedantic option
 EOF
 exit 0
 }
@@ -51,7 +55,6 @@ rm -f $tmp*
 # Default mode is to test single configurations ('-1').
 
 mode=1
-fake=no
 
 if [ -t 1 ]
 then
@@ -71,18 +74,23 @@ die () {
   exit 1
 }
 
+fake=no
 force=no
 coverage=yes
+pedantic=yes
 
 while [ $# -gt 0 ]
 do
   case "$1" in
     -h) usage;;
-    -n) fake=yes;;
     -1) mode=1;;
     -2) mode=2;;
     -3) mode=3;;
-    -n) force=yes;;
+    -f) force=yes;;
+    --fake) fake=yes;;
+    --force) force=yes;;
+    --no-coverage) coverage=no;;
+    --no-pedantic) pedantic=no;;
     -j|-j*) parallel="$1";;
     *) die "invalid option '$1' (try '-h')";;
   esac
@@ -219,13 +227,14 @@ echo "---- [ single configurations ]" \
 "----------------------------------------------"
 echo
 
-for pedantic in yes no
+for p in yes no
 do
+  [ $pedantic = no -a $p = yes ] && continue
   for first in $all
   do
     [ $first = --no-metrics ] && continue
     options="$first"
-    [ $pedantic = yes ] && options="-p $options"
+    [ $p = yes ] && options="-p $options"
     run $options
   done
 done
@@ -279,20 +288,21 @@ echo "---- [ double configurations ]" \
 "----------------------------------------------"
 echo
 
-for pedantic in yes no
+for p in yes no
 do
+  [ $pedantic = no -a $p = yes ] && continue
   for first in $all
   do
     [ x$first = x--default ] && continue;
     [ x$first = x--no-metrics ] && continue;
     metrics=no
     [ x$first = x-g -o x$first = x-l ] && metrics=yes
-    for second in `echo -- $all|fmt -0|sed "1,/$first/d"`
+    for second in `echo -- $all|fmt -1|sed "1,/$first/d"`
     do
       if redundant $first $second; then continue; fi
       [ x$second = x--no-metrics -a $metrics = no ] && continue
       options="$first $second"
-      [ $pedantic = yes ] && options="-p $options"
+      [ $p = yes ] && options="-p $options"
       run $options
     done
   done
@@ -312,26 +322,27 @@ echo "---- [ triple configurations ]" \
 "----------------------------------------------"
 echo
 
-for pedantic in yes no
+for p in yes no
 do
+  [ $pedantic = no -a $p = yes ] && continue
   for first in $all
   do
     [ x$first = x--default ] && continue;
     [ x$first = x-g -o x$first = x-l ] && metrics=yes
-    for second in `echo -- $all|fmt -0|sed "1,/$first/d"`
+    for second in `echo -- $all|fmt -1|sed "1,/$first/d"`
     do
       if redundant $first $second; then continue; fi
       metrics=no
       [ x$first = x-g -o x$first = x-l ] && metrics=yes
       [ x$second = x--no-metrics -a $metrics = no ] && continue
       [ x$second = x-g -o x$second = x-l ] && metrics=yes
-      for third in `echo -- $all|fmt -0|sed "1,/$second/d"`
+      for third in `echo -- $all|fmt -1|sed "1,/$second/d"`
       do
 	if redundant $first $third; then continue; fi
 	if redundant $second $third; then continue; fi
         [ x$third = x--no-metrics -a $metrics = no ] && continue
 	options="$first $second $third"
-	[ $pedantic = yes ] && options="-p $options"
+	[ $p = yes ] && options="-p $options"
 	run $options
       done
     done

src/allocate.c

@@ -12,46 +12,39 @@
 #include <inttypes.h>
 #endif
 
-static void
-inc_bytes (kissat * solver, size_t bytes)
-{
+static void inc_bytes (kissat *solver, size_t bytes) {
 #ifdef METRICS
   if (!solver)
     return;
   ADD (allocated_current, bytes);
   LOG5 ("allocated_current = %s",
-	FORMAT_BYTES (solver->statistics.allocated_current));
+        FORMAT_BYTES (solver->statistics.allocated_current));
   if (solver->statistics.allocated_current >=
-      solver->statistics.allocated_max)
-    {
-      solver->statistics.allocated_max = solver->statistics.allocated_current;
-      LOG5 ("allocated_max = %s",
-	    FORMAT_BYTES (solver->statistics.allocated_max));
-    }
+      solver->statistics.allocated_max) {
+    solver->statistics.allocated_max = solver->statistics.allocated_current;
+    LOG5 ("allocated_max = %s",
+          FORMAT_BYTES (solver->statistics.allocated_max));
+  }
 #else
   (void) solver;
   (void) bytes;
 #endif
 }
 
-static void
-dec_bytes (kissat * solver, size_t bytes)
-{
+static void dec_bytes (kissat *solver, size_t bytes) {
 #ifdef METRICS
   if (!solver)
     return;
   SUB (allocated_current, bytes);
   LOG5 ("allocated_current = %s",
-	FORMAT_BYTES (solver->statistics.allocated_current));
+        FORMAT_BYTES (solver->statistics.allocated_current));
 #else
   (void) solver;
   (void) bytes;
 #endif
 }
 
-void *
-kissat_malloc (kissat * solver, size_t bytes)
-{
+void *kissat_malloc (kissat *solver, size_t bytes) {
   void *res;
   if (!bytes)
     return 0;
@@ -63,22 +56,16 @@ kissat_malloc (kissat * solver, size_t bytes)
   return res;
 }
 
-void
-kissat_free (kissat * solver, void *ptr, size_t bytes)
-{
-  if (ptr)
-    {
-      LOG4 ("free (%p[%zu])", ptr, bytes);
-      dec_bytes (solver, bytes);
-      free (ptr);
-    }
-  else
+void kissat_free (kissat *solver, void *ptr, size_t bytes) {
+  if (ptr) {
+    LOG4 ("free (%p[%zu])", ptr, bytes);
+    dec_bytes (solver, bytes);
+    free (ptr);
+  } else
     assert (!bytes);
 }
 
-void *
-kissat_nalloc (kissat * solver, size_t n, size_t size)
-{
+void *kissat_nalloc (kissat *solver, size_t n, size_t size) {
   void *res;
   if (!n || !size)
     return 0;
@@ -89,15 +76,13 @@ kissat_nalloc (kissat * solver, size_t n, size_t size)
   LOG4 ("nalloc (%zu, %zu) = %p", n, size, res);
   if (!res)
     kissat_fatal ("out-of-memory allocating "
-		  "%zu = %zu x %zu bytes", bytes, n, size);
+                  "%zu = %zu x %zu bytes",
+                  bytes, n, size);
   inc_bytes (solver, bytes);
   return res;
 }
 
-
-void *
-kissat_calloc (kissat * solver, size_t n, size_t size)
-{
+void *kissat_calloc (kissat *solver, size_t n, size_t size) {
   void *res;
   if (!n || !size)
     return 0;
@@ -108,14 +93,13 @@ kissat_calloc (kissat * solver, size_t n, size_t size)
   const size_t bytes = n * size;
   if (!res)
     kissat_fatal ("out-of-memory allocating "
-		  "%zu = %zu x %zu bytes", bytes, n, size);
+                  "%zu = %zu x %zu bytes",
+                  bytes, n, size);
   inc_bytes (solver, bytes);
   return res;
 }
 
-void
-kissat_dealloc (kissat * solver, void *ptr, size_t n, size_t size)
-{
+void kissat_dealloc (kissat *solver, void *ptr, size_t n, size_t size) {
   if (!n || !size)
     return;
   if (MAX_SIZE_T / size < n)
@@ -124,38 +108,34 @@ kissat_dealloc (kissat * solver, void *ptr, size_t n, size_t size)
   kissat_free (solver, ptr, bytes);
 }
 
-void *
-kissat_realloc (kissat * solver, void *p, size_t old_bytes, size_t new_bytes)
-{
+void *kissat_realloc (kissat *solver, void *p, size_t old_bytes,
+                      size_t new_bytes) {
   if (old_bytes == new_bytes)
     return p;
-  if (!new_bytes)
-    {
-      kissat_free (solver, p, old_bytes);
-      return 0;
-    }
+  if (!new_bytes) {
+    kissat_free (solver, p, old_bytes);
+    return 0;
+  }
   dec_bytes (solver, old_bytes);
   void *res = realloc (p, new_bytes);
   LOG4 ("realloc (%p[%zu], %zu) = %p", p, old_bytes, new_bytes, res);
   if (new_bytes && !res)
     kissat_fatal ("out-of-memory reallocating from %zu to %zu bytes",
-		  old_bytes, new_bytes);
+                  old_bytes, new_bytes);
   inc_bytes (solver, new_bytes);
   return res;
 }
 
-void *
-kissat_nrealloc (kissat * solver, void *p, size_t o, size_t n, size_t size)
-{
-  if (!size)
-    {
-      assert (!p);
-      assert (!o);
-      return 0;
-    }
+void *kissat_nrealloc (kissat *solver, void *p, size_t o, size_t n,
+                       size_t size) {
+  if (!size) {
+    assert (!p);
+    assert (!o);
+    return 0;
+  }
   const size_t max = MAX_SIZE_T / size;
   if (max < o || max < n)
-    kissat_fatal ("invalid 'kissat_nrealloc (..., %zu, %zu, %zu)' call",
-		  o, n, size);
+    kissat_fatal ("invalid 'kissat_nrealloc (..., %zu, %zu, %zu)' call", o,
+                  n, size);
   return kissat_realloc (solver, p, o * size, n * size);
 }