4 ms·

If anyone else is wondering how the hell to use this thing... the main API is here: https://github.com/arminbiere/kissat/blob/master/src/kissat.h In parti

If anyone else is wondering how the hell to use this thing... the main API is here: https://github.com/arminbiere/kissat/blob/master/src/kissat.h In particular all you need to add clauses is this single API entry point: void kissat_add (kissat * solver, int lit); The solver consists of the conjunction of disjunctions (I hope I have that correct — maybe the other way around? I can never remember). Variables are assumed to be any non-zero integer: kissat_add(s, [N != 0]); You create a clause by repeatedly calling kissat_add; the clause is terminated by a 0. For instance if {shirt=1, tie=2}, then "!shirt or tie" is: kissat_add(s, -1); kissat_add(s, 2); kissat_add(s, 0); Once the solver is run, if there's a solution, you get the solution using `kissat_val`: kissat_val(s, 1); kissat_val(s, 2); I hope.

throwawaygh 6y ago
It supports the DIMACS input format [1], which you can parse using the kissat_parse_dimacs function [2]. DIMACS is a pretty terrible format, but at least you don't have to build the clauses up yourself using kissat_add. [1] http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/SATLINK____DIMACS http://www.cs.utexas.edu/users/moore/acl2/manuals/current/ma... [2] https://github.com/arminbiere/kissat/blob/master/src/parse.h https://github.com/arminbiere/kissat/blob/master/src/parse.h
amelius 6y ago
How do you interrupt the computation, e.g. when it takes too long?
- mgraczyk 6y ago
  You could always fork the process and send SIGKILL to the child after a timeout.
  - jwilk 6y ago
    No need to fork; you could install timer using alarm(), setitimer(), or timer_create() and friends.
    - amelius 6y ago
      But how would you clean up the heap and restart the library?
      - jwilk 6y ago
        I think you can call kissat_terminate() from the signal handler.
jwilk 6y ago
SAT solvers use CNF (conjuction of disjunctions). DNF-SAT can be trivially solved in O(n), because each clause directly encodes a solution (except for clauses that are contradictory, of course). But there's no known way to "convert" arbitrary formulas to DNF in polynomial time, so such a solver is not useful.

throwawaygh 6y ago

It supports the DIMACS input format [1], which you can parse using the kissat_parse_dimacs function [2]. DIMACS is a pretty terrible format, but at least you don't have to build the clauses up yourself using kissat_add. [1] http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/SATLINK____DIMACS http://www.cs.utexas.edu/users/moore/acl2/manuals/current/ma... [2] https://github.com/arminbiere/kissat/blob/master/src/parse.h https://github.com/arminbiere/kissat/blob/master/src/parse.h

amelius 6y ago

How do you interrupt the computation, e.g. when it takes too long?

mgraczyk 6y ago
You could always fork the process and send SIGKILL to the child after a timeout.
- jwilk 6y ago
  No need to fork; you could install timer using alarm(), setitimer(), or timer_create() and friends.
  - amelius 6y ago
    But how would you clean up the heap and restart the library?
    - jwilk 6y ago
      I think you can call kissat_terminate() from the signal handler.

jwilk 6y ago

SAT solvers use CNF (conjuction of disjunctions). DNF-SAT can be trivially solved in O(n), because each clause directly encodes a solution (except for clauses that are contradictory, of course). But there's no known way to "convert" arbitrary formulas to DNF in polynomial time, so such a solver is not useful.