arminbiere/kissat

kissat's Issues

Shared library with example usage?

In order to allow Kissat to be used by other languages (Java, .NET, Python, Go, etc.) it would be nice to have it built as a shared library. In addition to that, a simple example on how to use the library would also be great.

When both shared and static lib is requested each module should be built twice - with and without -fpic

Currently all modules are built once with -fpic.

The easiest way to achieve this is to use cmake to build the project.

Description of autarky flags swapped

The descriptions of the autarky and autarkydelay flags look like they should be swapped:

kissat/src/options.h

Lines 9 to 10 in baef460

	OPTION( autarky, 1, 0, 1, "delay autarky reasoning") \
	OPTION( autarkydelay, 1, 0, 1, "enable autarky reasoning") \

Run multiple file .cnf.txt then export to a file?

Is there any way to run multiple files .cnf.txt (in build folder) and export the result to a file instead of running each file in turn and then reading the results in the console?
Thanks!

Pipe/Fork/Exec/Waitpid instead of Popen

Also should move to pipe/fork/exec/waitpid instead of calling popen for writing compressed proofs as in CaDiCaL:
https://github.com/arminbiere/cadical/releases/tag/rel-1.7.3

Size checking in check_repeated_proof_lines (src/proof.c)

Hi,

During installation on macOS, I faced the following error:

Scheduled 133 jobs through 'tissat_schedule_prove'.

Running 693 jobs in parallel using up to 4 processes.
tissat: unexpected signal: Caught signal '6' (SIGABRT) in application 'kissat -q ../test/cnf/add128.cnf add128.proof66'
make[1]: *** [test] Error 1

Here's the detail.

$ ./build/kissat -q test/cnf/add128.cnf proof.drat
../src/proof.c:269: check_repeated_proof_lines: Coverage goal `proof->units[punit]' reached.
zsh: abort      ./build/kissat -q test/cnf/add128.cnf proof.drat

So I fixed the bug by modifying the checking code.

diff --git a/src/proof.c b/src/proof.c
index dfd6a0f..94e3014 100644
--- a/src/proof.c
+++ b/src/proof.c
@@ -262,7 +262,7 @@ check_repeated_proof_lines (proof * proof)
       const int eunit = PEEK_STACK (proof->line, 0);
       const unsigned punit = external_to_proof_literal (eunit);
       assert (punit != INVALID_LIT);
-      if (!proof->size_units || proof->size_units < punit)
+      if (!proof->size_units || proof->size_units <= punit)
        resize_proof_units (proof, punit);
       else
        {

Am I right?

IPASIR compatibility

What are your plans for supporting IPASIR interface? It seems to me that there is no way for the following API currently:

1. void ipasir_assume (void * solver, int lit)
2. int ipasir_failed (void * solver, int lit)
3. void ipasir_set_learn (void * solver, void * state, int max_length, void (*learn)(void * state, int * clause))

Add '--thanks=<string-hashed-to-seed>' option

#49 (comment)

exactly one clauses

is it possible -in theory- to handle exactly-one-clauses (non-cnf) more efficiently
by SAT-solvers like kissat ?

they are tedious and lengthy to convert to cnf and are used by
exact-cover problem conversions.

These are clauses where exactly one from a list of variables is true and
all others in the list are false.

SC 2022 versions - when to use them?

I wonder - should I now switch to sc2022-light (current master branch)? I just want a powerful solver :-) From the README I figure that you have a different goal: simplify the solver. I did some experiments (switching solvers) which are inconclusive so far.

My application is https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox . I will cite kissat in my system description, to be submitted for Workshop on Termination.

internal time limit feature

The following discussion became an enhancement rquest in adding an internal time limit feature.

hi,

I wonder how to set the time limit through the Kissat API? kissat_set_option doesn't seem to work. Looks like we can set it through --time in CLI, is that the only option?

https://www.mankier.com/1/kissat
https://github.com/arminbiere/kissat/blob/master/src/kissat.h

The API works better for us as the CLI'd introduce significant overhead in disk I/O.

thanks, Jian

Originally posted by @zengjian-hu-rai in #42

inaccurate format string

With the attached patch applied:

diff --git src/print.h src/print.h
index 2c39e2e..9092dab 100644
--- src/print.h
+++ src/print.h
@@ -10,15 +10,15 @@ struct kissat;
 int kissat_verbosity (struct kissat *);

 void kissat_signal (struct kissat *, const char *type, int sig);
-void kissat_message (struct kissat *, const char *fmt, ...);
+void kissat_message (struct kissat *, const char *fmt, ...) __attribute__((format(printf, 2, 3)));
 void kissat_section (struct kissat *, const char *name);
-void kissat_verbose (struct kissat *, const char *fmt, ...);
-void kissat_very_verbose (struct kissat *, const char *fmt, ...);
-void kissat_extremely_verbose (struct kissat *, const char *fmt, ...);
-void kissat_warning (struct kissat *, const char *fmt, ...);
+void kissat_verbose (struct kissat *, const char *fmt, ...) __attribute__((format(printf, 2, 3)));
+void kissat_very_verbose (struct kissat *, const char *fmt, ...) __attribute__((format(printf, 2, 3)));
+void kissat_extremely_verbose (struct kissat *, const char *fmt, ...) __attribute__((format(printf, 2, 3)));
+void kissat_warning (struct kissat *, const char *fmt, ...) __attribute__((format(printf, 2, 3)));

 void kissat_phase (struct kissat *, const char *name, uint64_t,
-                  const char *fmt, ...);
+                  const char *fmt, ...) __attribute__((format(printf, 4, 5)));
 #else

 #define kissat_message(...) do { } while (0)

GCC 7.5.0 says the following:

...
gcc -W -Wall -O3 -DNEMBEDDED -DNDEBUG -DNMETRICS -DNSTATISTICS -c ../src/limits.c
../src/limits.c: In function ‘kissat_scale_delta’:
../src/limits.c:92:5: warning: too many arguments for format [-Wformat-extra-args]
     "scaled %s delta %" PRIu64
     ^~~~~~~~~~~~~~~~~~~

I think the format string here is missing a "%". I.e. something like the following change:

diff --git src/limits.c src/limits.c
index fafc63e..23c1e69 100644
--- src/limits.c
+++ src/limits.c
@@ -92,7 +92,7 @@ kissat_scale_delta (kissat * solver, const char *pretty, uint64_t delta)
     "scaled %s delta %" PRIu64
     " = %g * %" PRIu64
     " = %g^2 * %" PRIu64
-    " = log10^2(" PRIu64 ") * %" PRIu64,
+    " = log10^2(%" PRIu64 ") * %" PRIu64,
     pretty, scaled, ff, delta, f, delta, C, delta);
 // *INDENT-ON*
   (void) pretty;

What options might influence kissat's behaviour the most?

(I apologize if this is not the right venue for discussion. Still I hope to get some input - and I will report back my findings as well.)

I noticed (perchance) in some application that setting "xors" to 0 and "walkinitially" to 1 makes kissat faster.

Rodrigue Konan Tchinda, Clémentin Tayou Djamegni: Pakis (Satcomp 21 proceedings, p 26/27) https://helda.helsinki.fi/handle/10138/333647 configure these options: tier1, chrono, stable, walkinitially, target, phase.

What other candidates are there for options that might have noticeable influence? What kissat version is best for experimentation with these?

I don't want to go modify kissat's source - just call it (command line or API, example - https://github.com/jwaldmann/ersatz-kissatapi/blob/main/test/twenty-four.hs#L109)

More incrementality features?

Hi Armin,

Are there chances that kissat will have a basic "assumptions" interface and be able to report unsatisfiable cores?

Best,
Alexey

test fails if too broad privileges (e.g. in root)

file '/etc/shadow' determined to be readable unexpectedly
file '/etc/passwd' determined to be writable unexpectedly

limit check print bug

In

kissat/src/application.c

Line 745 in 8fca2aa

application->conflicts < 0 && application->conflicts < 0)

there is application->conflicts checked twice. My guess is that one of them should instead read application->decisions

Description of --walkmineff is incorrect

Looks like a copy/past error:

  --walkmineff=0...          minimum vivify efficiency [1e7]

I think it should say "minimum local search efficiency".

output simplified formula

It would be great if kissat could emit the simplified formula after setting some limit, such as --conflicts, similar to CaDiCAL's -o option.

Remove redundant variables

I have a question about the variables in Kissat described following.

p cnf 4 2
1 2 0
5 6 0

Expected output:

Satisfiable
1 2 5 6 0

In .cnf file, I have 4 variables X1, X2, X5, X6 and 2 clauses X1 v X2 and X5 v X6 as above. For some reason, I don't need to use X3, X4, I just use 4 variables X1, X2, X5, X6 and I expect that the output should return only the value of those variables. However, when I used Kissat to solve this problem, it showed the following log:

parse error: maximum variable index exceeded (try '--relaxed' parsing)

Then I edited the number of variables in the header to 6 (p cnf 6 2), and I found that Kissat returned the value of both X3, X4 (it means that it returned full variables from X1 to the biggest variable - X6).

Hence, my questions are:

• Is it compulsory to use continuous variables in Kissat?
• If not, how to get result of only declared variables in .cnf file?
• I tried --relaxed, but it only returned the value of X1, X2, X3, X4 (4 variables as in the header) without the value of X5, X6.

kissat is using CPU time (not wall time) for stats?

I am running several kissat solver instances concurrently, via IPASIR, from one (Haskell) main program. When I switch on verbose logging, the seconds column of kissat output increases (much) faster than real time.

Could it be that kissat uses CPU time for this? Should it be wall time?

Is this number used elsewhere besides logging? Perhaps for time-out?

Example: a long-running such process, containing 10 kissat instances, main programm killed, prints

...
c ? 85843.06 630 87 100 1172 93920 2 27281595 222077 48% 37 24901 1204 15%
c } 85841.94 596 86 102 1202 97658 2 28347427 235795 49% 37 24841 1197 15%
c ? 85841.94 596 86 102 1202 97658 2 28347427 235795 49% 37 24841 1197 15%
c ] 85842.67 560 82 107 1287 106876 1 31360910 252378 51% 34 24725 1178 14%
c ? 85842.67 560 86 107 1287 106876 2 31360910 252378 48% 38 24725 1178 14%


real    144m21.859s
user    1427m6.330s
sys     3m38.234s

note that 1427 min (user time) is 85620 seconds (roughly what's in the log)

`kissat_set_terminate` is not Implemented

Declaration is there but implementation is not.

Proofs?

How to generate proofs?
I tried (latest) kissat -f fname.cnf, but no file created...

beginner's questions

what can i do if it says "Did not find 'drat-trim' executable." when testing? and how can i check the proof?

Windows x64 port

Officially-provided windows binaries would be nice. In the meantime, I hacked together a port to Windows (and VC++), and released x64 binaries here:
https://github.com/deiruch/kissat/releases/

The port uses the same PAL as my CaDiCaL port. I replaced the VLAs by alloca, because VLAs are unfortunately still not supported by VC++. Additionally, I had to change some struct members from bool to unsigned to work around the annoying struct packing behavior of VC++.

treewidth

is there a concept similar to "treewidth" for SAT-problems ?
That gave improvements in "parameterized programming"

We can just make the graph whose vertices are the variables
and there is an edge, iff 2 vertices appear in the same clause.

Then reorder the vertices with a treewidth program
and feed the reordered instance into kissat
(skipping kissat's initial reordering)

count_clause is called twice for all clauses

This line here:

kissat/src/vivify.c

Line 195 in baef460

count_clause (c, counts);

is called twice, due to prioritize going around twice. Probably a very small performance regression :)

documentation

I am very interested in using your SAT solver Kissat, for an interdisciplinary project with biologists.
Unfortunately I could not find a documentation on how to integrate it in a project (in this case a C++ project), or even to use it as external program. I could only clone the github repository and use make ("make test" works fine), but then I'm kind of stuck.

I am aware that it is probably my lack of experience which makes this a problem, but do you have a documentation or a quick pointer on how to get started ?

I also wanted to ask whether there is some incremental solving implemented in it, as it would be very useful for the model enumeration that I'm planning to do.

Thank you very much for your work and for your help !

kissat_signature not implemented

The kissat_signature function, as defined here

kissat/src/kissat.h

Line 8 in baef460

const char *kissat_signature (void);

is implemented nowhere.

Descriptions of options --autarky and --autarkeydelay are swapped

It appears that the descriptions of the autarky- and autarkeydelay-options are swapped. From the command-line help:

...
  --autarky=<bool>           delay autarky reasoning [true]
  --autarkydelay=<bool>      enable autarky reasoning [true]
...

Tag releases

It would be nice if you could tag release versions.

TISSAT is reporting an error

Hi,
while compiling kissat (Download from 28.08.2022, 14:20) under Windows under cygwin the following test did not run successfully:

User@DESKTOP-5UC7OJ9 ~/kissat-master
$ ./configure && make test
configure: default configuration (see '-h')
configure: new build directory 'build'
configure: assuming GCC version 11.3.0 uses C99 by default
configure: compiler 'gcc  -W -Wall -O3 -DNDEBUG'
configure: linker 'gcc' (no additional options)
configure: using default 'ar' (no cross compilation)
configure: no 'tissat' binary generated (without '--test')
configure: no 'libkissat.so' shared library generated (without '-shared')
configure: no 'kitten' binary generated (without '--kitten')
configure: linking src/makefile
make -C "/home/User/kissat-master/build" test
make[1]: Entering directory '/home/User/kissat-master/build'
gcc -W -Wall -O3 -DNDEBUG -c ../src/allocate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/analyze.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/ands.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/arena.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/assign.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/averages.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/backbone.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/backtrack.c
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -DNDEBUG -I../build -c ../src/build.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/bump.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/check.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/clause.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/collect.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/colors.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/compact.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/config.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/decide.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/deduce.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/definition.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/dense.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/dump.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/eliminate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/equivalences.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/error.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/extend.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/file.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/flags.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/format.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/forward.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/gates.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/heap.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/ifthenelse.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/import.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/internal.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/kimits.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/kitten.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/learn.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/logging.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/minimize.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/mode.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/options.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/phases.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/print.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/probe.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/profile.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/promote.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/proof.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propbeyond.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propdense.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/proprobe.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propsearch.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/queue.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/reduce.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/reluctant.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/rephase.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/report.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resize.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resolve.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resources.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/restart.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/search.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/shrink.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/smooth.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/sort.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/stack.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/statistics.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/strengthen.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/substitute.c
../src/substitute.c: In function ‘kissat_substitute’:
../src/substitute.c:575:30: warning: array subscript 3 is above array bounds of ‘unsigned int[3]’ [-Warray-bounds]
  575 |                       c->lits[old_size - 1] = INVALID_LIT;
      |                       ~~~~~~~^~~~~~~~~~~~~~
In file included from ../src/internal.h:9,
                 from ../src/inlinevector.h:4,
                 from ../src/inline.h:4,
                 from ../src/substitute.c:3:
../src/clause.h:34:12: note: while referencing ‘lits’
   34 |   unsigned lits[3];
      |            ^~~~
gcc -W -Wall -O3 -DNDEBUG -c ../src/sweep.c
../src/sweep.c: In function ‘substitute_connected_clauses.isra’:
../src/sweep.c:1082:28: warning: array subscript 3 is above array bounds of ‘unsigned int[3]’ [-Warray-bounds]
 1082 |                     c->lits[old_size - 1] = INVALID_LIT;
      |                     ~~~~~~~^~~~~~~~~~~~~~
In file included from ../src/internal.h:9,
                 from ../src/inlinevector.h:4,
                 from ../src/inline.h:4,
                 from ../src/sweep.c:2:
../src/clause.h:34:12: note: while referencing ‘lits’
   34 |   unsigned lits[3];
      |            ^~~~
gcc -W -Wall -O3 -DNDEBUG -c ../src/terminate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/trail.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/utilities.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/vector.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/vivify.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/walk.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/warmup.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/watch.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/weaken.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o averages.o backbone.o backtrack.o build.o bump.o check.o clause.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dump.o eliminate.o equivalences.o error.o extend.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kimits.o kitten.o learn.o logging.o minimize.o mode.o options.o phases.o print.o probe.o profile.o promote.o proof.o propbeyond.o propdense.o proprobe.o propsearch.o queue.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o trail.o utilities.o vector.o vivify.o walk.o warmup.o watch.o weaken.o
gcc -W -Wall -O3 -DNDEBUG -c ../src/main.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/application.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/handle.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/parse.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/witness.c
gcc -o kissat main.o application.o handle.o parse.o witness.o libkissat.a -lm
gcc -W -Wall -O3 -DNDEBUG -I../build -c ../test/test.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testadd.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testallocate.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testapplication.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testarena.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testarray.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testbump.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testceil.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testcollect.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testconfig.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testcoverage.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testdivert.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testdump.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testendianness.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testerror.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testfile.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testformat.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testheap.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testinit.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testkitten.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testmain.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testmessages.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testoptions.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testparse.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testprove.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testqueue.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testrandom.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testrank.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testreferences.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testreluctant.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testscheduler.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testsizes.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testsolve.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testsort.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/teststack.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testterminate.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testusage.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testutilities.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testvector.c
gcc -o tissat test.o application.o handle.o parse.o witness.o testadd.o testallocate.o testapplication.o testarena.o testarray.o testbump.o testceil.o testcollect.o testconfig.o testcoverage.o testdivert.o testdump.o testendianness.o testerror.o testfile.o testformat.o testheap.o testinit.o testkitten.o testmain.o testmessages.o testoptions.o testparse.o testprove.o testqueue.o testrandom.o testrank.o testreferences.o testreluctant.o testscheduler.o testsizes.o testsolve.o testsort.o teststack.o testterminate.o testusage.o testutilities.o testvector.o libkissat.a -lm
./tissat
TISSAT Tester for KISSAT

Copyright (c) 2021-2022 Armin Biere University of Freiburg
Copyright (c) 2019-2021 Armin Biere Johannes Kepler University Linz

Version 3.0.0 unknown
gcc (GCC) 11.3.0 -W -Wall -O3 -DNDEBUG
Sun, Aug 28, 2022 2:18:54 PM CYGWIN_NT-10.0-22000 DESKTOP-5UC7OJ9 3.3.5-341.x86_64 x86_64

Use '-h' to print usage (i.e., how to use patterns).
Changed to '/home/User/kissat-master/build' directory.
Parallel execution using at most 32 processes (by default).
Job execution progress reporting disabled (enable with '-p').

Found '../test' directory (running test cases that need '../test' too).
Did not find 'drabt' executable.
Did not find 'drat-trim' executable.

Install either 'drat-trim' or 'drabt' to check proofs too!

Found 'bzip2' executable for testing compression.
Found 'gzip' executable for testing compression.
Found 'lzma' executable for testing compression.
Found 'xz' executable for testing compression.
Did not find '7z' executable for testing compression.

Scheduled 4 jobs through 'tissat_schedule_error'.
Scheduled 1 jobs through 'tissat_schedule_utilities'.
Scheduled 1 jobs through 'tissat_schedule_endianness'.
Scheduled 3 jobs through 'tissat_schedule_ceil'.
Scheduled 1 jobs through 'tissat_schedule_format'.
Scheduled 2 jobs through 'tissat_schedule_references'.
Scheduled 1 jobs through 'tissat_schedule_reluctant'.
Scheduled 2 jobs through 'tissat_schedule_random'.
Scheduled 1 jobs through 'tissat_schedule_queue'.
Scheduled 3 jobs through 'tissat_schedule_allocate'.
Scheduled 1 jobs through 'tissat_schedule_array'.
Scheduled 2 jobs through 'tissat_schedule_stack'.
Scheduled 4 jobs through 'tissat_schedule_arena'.
Scheduled 3 jobs through 'tissat_schedule_heap'.
Scheduled 2 jobs through 'tissat_schedule_vector'.
Scheduled 2 jobs through 'tissat_schedule_rank'.
Scheduled 2 jobs through 'tissat_schedule_sort'.
Scheduled 1 jobs through 'tissat_schedule_bump'.
Scheduled 4 jobs through 'tissat_schedule_options'.
Scheduled 2 jobs through 'tissat_schedule_config'.
Scheduled 5 jobs through 'tissat_schedule_init'.
Scheduled 1 jobs through 'tissat_schedule_add'.
Scheduled 6 jobs through 'tissat_schedule_file'.
Scheduled 2 jobs through 'tissat_schedule_parse'.
Scheduled 44 jobs through 'tissat_schedule_usage'.
Scheduled 6 jobs through 'tissat_schedule_main'.
Scheduled 1 jobs through 'tissat_schedule_collect'.
Scheduled 2 jobs through 'tissat_schedule_kitten'.
Scheduled 414 jobs through 'tissat_schedule_solve'.
Scheduled 45 jobs through 'tissat_schedule_coverage'.
Scheduled 0 jobs through 'tissat_schedule_terminate'.

Running 568 jobs in parallel using up to 32 processes.
tissat: fatal error: 'kissat --walkinitially --conflicts=3000 --probeinit=0 --eliminateinit=0 ../test/cnf/hard.cnf --profile=4' returns '1' and not '0'
tissat: fatal error: 'kissat ../test/cnf/hard.cnf --walkinitially -v -v -v --colors --conflicts=1e4' returns '1' and not '0'
Stack trace:
Frame        Function    Args
000FFFFBE90  00180062277 (000FFFFC098, 00000000002, 00000000002, 000FFFFDE50)
00000000000  001800642F5 (000FFFFC840, 00000000000, 00000000180, 00000000000)
000FFFFC5A0  00180133018 (00180143837, 0018026A7A0, 00000000004, 00000000002)
00000000041  0018012E64B (00180156060, 00000000000, 00000000000, 00000000000)
00000000001  0018012EA55 (000FFFFC998, 0010045F050, 00800068A60, 0080006F590)
00000000001  00180215498 (00180230EE8, 0010045F074, 000FFFFC9B0, 0010045F037)
00000000001  00100410799 (00800068A60, 00000000001, 00000000000, 0010045F030)
00000000001  00100404B30 (00800068A60, 00000000002, 00000000000, 00000000D90)
0010046760D  0010041A8EC (000FFFFCABC, 00000000020, 00000000000, 000FFFFD680)
0010046760D  0010041B15F (00000000000, 0010045CC89, 000FFFFCC80, 00000000000)
001004F53C4  0010045A4EF (00180049B11, 00180048A70, 00000000002, 00180325FC0)
000FFFFCD30  00180049B7D (00000000000, 00000000000, 00000000000, 00000000000)
000FFFFFFF0  00180047746 (00000000000, 00000000000, 00000000000, 00000000000)
000FFFFFFF0  001800477F4 (00000000000, 00000000000, 00000000000, 00000000000)
End of stack trace
                  tissat: unexpected signal: Caught signal '6' (SIGABRT) in application 'kissat ../test/cnf/hard.cnf --walkinitially -v -v -v --colors --conflicts=1e4'
tissat: fatal error: 'kissat --decisions=10 ../test/cnf/hard.cnf --no-reduce' returns '1' and not '0'
Stack trace:
Frame        Function    Args
000FFFFBE90  00180062277 (000FFFFC098, 00000000002, 00000000002, 000FFFFDE50)
00000000000  001800642F5 (000FFFFC840, 00000000000, 0000000017C, 00000000000)
000FFFFC5A0  00180133018 (00180143837, 0018026A7A0, 00000000002, 00000000002)
00000000041  0018012E64B (00180156060, 00000000000, 00000000000, 00000000000)
00000000001  0018012EA55 (000FFFFC998, 0010045F050, 00800068AB0, 0080006F510)
00000000001  00180215498 (00180230EE8, 0010045F074, 000FFFFC9B0, 0010045F037)
00000000001  00100410799 (00800068AB0, 00000000001, 00000000000, 0010045F030)
00000000001  00100404B30 (00800068AB0, 00000000002, 00000000000, 00000000D91)
0010046760D  0010041A8EC (000FFFFCABC, 00000000020, 00000000000, 000FFFFD680)
0010046760D  0010041B15F (00000000000, 0010045CC89, 000FFFFCC80, 00000000000)
001004F53C4  0010045A4EF (00180049B11, 00180048A70, 00000000002, 00180325FC0)
000FFFFCD30  00180049B7D (00000000000, 00000000000, 00000000000, 00000000000)
000FFFFFFF0  00180047746 (00000000000, 00000000000, 00000000000, 00000000000)
000FFFFFFF0  001800477F4 (00000000000, 00000000000, 00000000000, 00000000000)
End of stack trace
                  make[1]: *** [makefile:31: test] Error 1
make[1]: Leaving directory '/home/User/kissat-master/build'
make: *** [makefile:16: test] Error 2

How do I make kissat use more CPU resources/time?

I want to make/let kissat use more resources to try and find solutions quicker. Is there a way to do this?

Is it possible to dump the pre-processed cnf?

Hi Armin,

Thanks for making this great tool! I'm writing to ask whether it's possible to use kissat (or CaDiCaL) to dump the preprocessed query (in cnf) after the solver has performed preprocessing on the cnf?

Best wishes,
Andrew

Is it possible to get the learned clauses after solving?

Hi,

Is it possible for Kissat to get the learned clauses after solving a SAT instance? In particular, is there a way to output the augmented CNF formula with the learned clauses when the CNF formula is satisfiable?

Thank you!

is kissat non-deterministic?

The following may sound a bit strange, but ...

I think kissat (3.1.1) found a model for a CNF (roughly 200k vars, 1m clauses), using --sat --quiet 1, after perhaps 15 min, but I am unable to reproduce it, in several tries, giving more than 1 hour each. So - was I hallucinating? Or was kissat just lucky?

The --help text includes

  --sat      target satisfiable instances ('--target=2 --restartint=50')
  --target=0..2              target phases (1=stable,2=focused) [1]
  --randec=<bool>            random decisions [true]
  --randecstable=<bool>      random decisions in stable mode [false]
  --randecfocused=<bool>     random decisions in focused mode [true]

meaing that it was random?

Assuming yes: what's the best strategy to find a model (again)? Just run repeatedly, with timeout? Or run once, without timeout? (of course I will try both.)

Availability of Documentation/Commented Source Code

Hello,

Is there any sort of documentation available to understand the source code? Or is there a version of source code with comments?

Thank you.

C++ interface

Hi,
as discussed via email, here is the issue regarding the C++ interface for kissat.
Nicolai

Remove build.h include

This is a minor issue but build.c includes a missing header file "build.h". I think this include can be removed.

#include "build.h"
#include "colors.h"
#include "kissat.h"
#include "print.h"

#include <stdio.h>

const char *kissat_signature (void) { return "kissat-" VERSION; }

Make binaries available for common platforms

In addition to source code, provide pre-compiled binaries for common platform (windows, macOS, linux) to allow students or researchers to simply download them to give a try to kissat.

If compiling kissat is easy for any computer scientist, when giving a tutorial about SAT, one would prefer to allow the audience to simply download a binary.

I am happy to contribute macOS binaries (M2 and Intel binaries).

Haskell API

Hi, if anyone is interested, I am working on a Haskell binding to Kissat here https://github.com/jwaldmann/ersatz-kissatapi

Test failures on Fedora

Since cvc4 1.8 adds support for kissat, I am looking into creating a Fedora package of kissat. The tests fail on 3 of our supported architectures.

On the two 32-bit architectures (arm and i686), the 2 GB allocation on line 20 of testallocate.c fails:

  p = kissat_calloc (solver, 1 << 29, 4);

The code doesn't check that p is nonnull, so the test segfaults when p is dereferenced on line 23. Simply changing all of the 29s to 28s leads to a successful run. Are you willing to make that change? (If not, I can simply patch those files during the Fedora build.)

On the big endian architecture (s390x), testendianess.c fails, as it is written to do. Is the issue that you don't have access to big endian hardware and therefore are unable to test? If so, and if I can figure out the code changes necessary to make the other tests pass, are you willing to look at a patch?

I have an unrelated question, which I can open a separate issue for if need be: are you willing to look at a patch that adds the ability to build a shared library?

not too bad

compilation on cygwin64 worked smooth - the test-thing aborted with a message 'fatal error file /etc/passwd determined to be writable unexpectedly' - why the heck does it want to write my passwd file ? never mind.
execution ( on cygwin64 ) is fine. Some early results compared to cadical october 2019:
seconds, incl reading

kissat     cadcal
   86         216
  370         390
   60          89
   58         131
  207         820

gar nicht mal so schlecht - weiter so!

default setting for --restartint

in your CPAIOR Master class SAT video, around minute 40, you say a few words about restart intervalls. I was surprised about the small intervall and looked at the Kissat parameters, how to increase it. i played with various values for --restartint and the larger, the better. i run kissat with --sat --restartint=10000 . Runtimes decrease between 25% and 75%, which is quite good.
The output says, that the default value 1 was replaced by 10000.
i propose to use a (much) larger default value when --sat is given. the Luby-sequence is just too slow to grow to large values.
Maybe it can be made adaptive to problem-size, that is number of variables or clauses ?

for those, who haven't seen the video:
https://youtu.be/t3bJcU1aQJI