SAT is a NP-complete problem also called "satisfiability problem". It is most often presented in the form of a set of boolean clauses, each of those being a disjunction of literals. A literal is either a proposition or its negation. The problem goal is to find whether it exists a valuation for those boolean literals such that all clauses are true, and, in this case, to give such a valuation. In other words, can we give each proposition a truth value such that all clauses have at least one true literal?
A simple example is:
a or (not b) b or c (not a) or (not c) (not c)
which is satisfiable by the valuation
a=1, b=1, c=0
There exists a simple, straighfoward standard format used to facilitate reading of a problem by a solver.
It is composed of:
p <n> <n>. The two numbers define the number of variables (propositions) and the number of clauses, respectively.
-9represents the literal
x9is the ninth proposition. A positive number just represents a proposition. Each clause (a list of literals) is ended by a 0, which cannot be a proposition since there would be no way to tell
c a very personal comment on this problem c talking about clauses and literals p 3 2 1 2 3 0 2 -3 0
It represents the logical problem
x1 or x2 or x3 x2 or (not x3)
A list of a few problem (quite) simple on which to test a SAT-solver, in Dimacs format.
The result is a SAT solver in rust, batsat with the ability to provide callbacks. I think these should be enough to be the basis for a CDCL(T) SMT solver.
I have been working on a (relatively) efficient SAT-solver written in Java. It implements the DPLL algorithm, with the following features:
Some lacking features are: