Wrapper for iterative (incremental) SAT solving using cryptominisat.
Original idea and base code is taken from EFSM-tools.
Simply execute make
.
Pull from Docker Hub:
docker pull lipen/incremental-cryptominisat
or build it yourself:
docker build -t incremental-cryptominisat .
docker run --rm -i lipen/incremental-cryptominisat < icnf
## SAT
## v -1 -2 -3
## SAT
## v 1 -2 3
## UNSAT
iCNF format is very similar to the standard DIMACS format:
- Iterative (incremental) SAT problem is represented by blocks -- each block is a set of clauses and the
solve
statement. - Each clause is represented with a single line containing a sequence of positive/negative variables, ending with 0 (zero).
- The
solve
statement indicates when the solver have to actually solve the SAT problem and print the result: satisfying assignment, or "UNSAT". - The standard DIMACS header (
p cnf <num-of-cons> <num-of-vars>
) is not required, but may be useful to specify the total number of variables in advance. - The
halt
statement forces the solver to halt. The solver automatically exits on EOF, so it is not required to have thehalt
statement at the end.
1 -3 0
2 3 -1 0
solve
1 0
-2 0
solve
-3
solve
halt