beginner's questions

[ticotica4]

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

[arminbiere]

Just install 'drat-trim' and put it (or a link) into your PATH.

[ticotica4]

thank you very much, does it means that i need to put 'drat-trim' into 'build' folder? i don't know the meaning of 'PATH'. Thank you again for answering my stupid questions.

[sschnug]

Start from https://en.wikipedia.org/wiki/PATH_(variable)
It's just about a system-global definition of where to look for some executable if it wasn't found in current scope.

As indicated by "current scope", for specific workflows it's not needed. Try it (e.g. putting every binary in build folder and executing from exactly this folder). If it doesn't work, make use of the path env-variable.

[ticotica4]

i tried to put 'drat-trim' into 'build' folder but it still says it can't find it.

[yberman]

Did you move the executable or the whole directory?

To modify the path

build_folder_path=`pwd`/build
echo $buid_folder_path

If it looks right:

PATH=$PATH:$build_folderpath

[KholodkovAlexey]

Is it possible to use kissat to get more than one model of cnf?
Or may be exists kissat forks that support multiple models search?

[a1880]

Kissat has a parameter --seed which defaults to 0 and initializes the random number generator. Choose another value and chances are that you get a different solution.

To definitely prevent the same solution to be found again, add an extra clause to your CNF which consists of inverted literals of the previous solution. Therefore, the next solution must be different in at least one variable.

[apgoucher]

add an extra clause to your CNF which consists of inverted literals of the previous solution.

Yes. If you're doing this, it's better to use an incremental SAT solver such as CaDiCaL (by the same author as kissat, Armin Biere) where you can add additional clauses and 'resume solving' instead of having to run it afresh with a slightly modified CNF. This way, you don't discard all of the progress (learned clauses) from the first run, so it will be able to find the next solution (or return UNSAT) much more quickly.

[a1880]

Other SAT solvers with built-in feature of multiple models/solutions include cryptominisat and clasp.

[KholodkovAlexey]

it's better to use an incremental SAT solver

Why incremental feature not implemented in kissat? It is not compatible with kissats's algorithm/heuristic?

[apgoucher]

I think that it's a planned feature -- there's an open issue about it -- but the author hasn't had time yet to implement it (there are more complicated invariants to consider when proving correctness of an incremental SAT solver). There's a fork of the repo by Jannis Harder which does add incremental solving to kissat, but it doesn't seem to be reliable (I've had it segfault before), so for now I just use CaDiCaL when I need an incremental solver.