Command line tool for SAT solving, SMT solving in various theories, and other algorithms related to satisfiability checking.
The techniques used here are introduced in the RWTH University lecture 'Satisfiability checking' by Prof. Dr. Erika Ábrahám.
Under Releases you can find the latest version of the project.
Download the jar file and run it with the following command:
java -jar satchecking-v1.0.1.jar
Now you should see the command prompt indicated by a > symbol.
An SMT solver is implemented for non-linear real arithmetic (QF_NRA), linear real arithmetic (QF_LRA), linear integer arithmetic (QF_LIA), equality logic (QF_EQ), equality logic with uninterpreted functions (QF_EQUF) and bit vector arithmetic (QF_BV).
> smt QF_NRA (y<=x^3) & (y<=-x^2+1) & (max(x+y))
SAT:
x=(x^3+x^2-1, 3/4, 7/8) ≈ 0.7548776662466928; y=(-1x^3+2x^2-3x+1, -4, 4) ≈ 0.4301597090019467;
Time: 297ms> smt QF_NRA (x^2+y^2<1) & (min(y))
UNSAT
Time: 12ms> smt QF_NRA (x^2 + y^2 = 1) & (x^2 + y^3 = 1/2)
SAT:
x=(x^6-2x^4+2x^2-3/4, 3/4, 15/16) ≈ 0.8249554777467228; y=(x^9+1/2x^6+3/4x^3+1/8, -7/4, 7/4) ≈ -0.5651977173836394;
Time: 456ms> smt QF_NRA (x*y > 0) & (y*z > 0) & (x*z > 0) & (x + y + z = 0)
UNSAT
Time: 7ms> smt QF_LRA (x<=-3 | x>=3) & (y=5) & (x+y>=12) & (min(x))
SAT:
x=7; y=5;
Time: 0ms> smt QF_LRA (x<=0 | x>=5) & (x+y=5/2) & (y=1)
UNSAT
Time: 1ms> smt QF_LIA (y+0.8x<=4) & (y-0.25x>=0) & (max(x))
SAT:
x=3; y=1;
Time: 1ms> smt QF_LIA (y-x<=0) & (y+x<=1) & (y>=0.1)
UNSAT
Time: 1ms> smt QF_EQ (a=b) & (c=d) & (a!=d)
SAT:
a=0.0; b=0.0; c=1.0; d=1.0;
Time: 0ms> smt QF_EQ (a=b) & (b=c) & (c=d) & (a!=d)
UNSAT
Time: 0ms> smt QF_EQUF (x1 = x2) & (x2 = x3) & (x4 = x5) & (f(x1) != f(x5))
SAT:
f(x1)=0.0; f(x5)=3.0; x1=2.0; x2=2.0; x3=2.0; x4=1.0; x5=1.0;
Time: 0ms> smt QF_EQUF (f(f(y)) != x) & (x = f(y)) & (y = u) & (x = y)
UNSAT
Time: 0ms> smt QF_BV (x >= 0) & (y > 0) & (y[6]) & (x >> y = 0) & (x + y < x * y)
SAT:
x=0b01010101 (85); y=0b01000000 (64);
Time: 3ms> smt QF_BV (a * b = c) & (b * a = c) & (x < y) & (y < x)
UNSAT
Time: 11msBesides the custom smt <theory> <formula> syntax above, the solver can read
SMT-LIB 2.6 scripts (a subset) with the smtlib command. This is how the
solver is validated against the official SMT-LIB benchmark library.
> smtlib (set-logic QF_NRA)(declare-const x Real)(declare-const y Real)(assert (= (+ (* x x) (* y y)) 1))(assert (= (+ (* x x) (* y y y)) (/ 1 2)))(check-sat)
satA file path can be given instead of an inline script:
> smtlib path/to/problem.smt2
When the script contains (set-info :status sat|unsat), the result is reported as MATCHES or
MISMATCHES the declared status.
Supported logics: QF_UF, QF_EQ, QF_LRA, QF_LIA, QF_NRA, and a sound fragment of QF_BV.
Supported features include full boolean structure (and, or, not, =>, ite, xor), let
bindings, define-fun macros, Bool-sorted variables, strict and non-strict (in)equalities, and
push/pop. Constructs that the underlying theories cannot yet solve soundly (e.g. bit-vector
extract/concat/unsigned comparisons, nonlinear division) are rejected with a clear error rather
than mis-solved.
Standard DIMACS CNF files can
be solved directly with the dimacs command:
> dimacs path/to/problem.cnf
Comment lines (c ...) are skipped, the p cnf <variables> <clauses> header is parsed, and the
formula is solved with the DPLL+CDCL solver.
A SAT solver is implemented that can employ DPLL+CDCL, DPLL as well as simple enumeration to solve propositional logic problems.
Input can be given in conjunctive normal form in the following way.
> sat (a) & (~a | b) & (~b | ~c)
SAT:
a=1, b=1, c=0;
1 model/s found in 0 ms> sat (a) & (~a | b) & (~b)
UNSATThe Tseitin transformation is implemented for propositional logic.
It can be used to transform a formula into an equi-satisfiable formula in conjunctive normal form.
The logical operators '~', '&', '|', '->', '<->' as well as parentheses are supported.
> tseitin ~(a & (a -> b) -> b)
Tseitin's transformation:
(~h3 | ~a | b) & (a | h3) & (~b | h3) & (~h2 | a) & (~h2 | h3) & (~a | ~h3 | h2) & (~h1 | ~h2 | b) & (h2 | h1) & (~b | h1) & (~h0 | ~h1) & (h1 | h0) & (h0)The program can check sets of weak linear constraints for satisfiability employing
the Simplex algorithm.
If the set of constraints is satisfiable, the program will print a satisfying assignment.
Otherwise, an explanation for unsatisfiability is given in the form of an infeasible subset.
Decimals, as well as fractions are supported which will be handled by exact rational arithmetic.
This setting can be changed to use floating point arithmetic in the config.properties file.
> simplex a+3b+5c=30 a>=5 a<=10 b>=2 c>=1
SAT!
Solution: a=10; b=5; c=1; Time: 0ms> simplex x+y=3 y=1 x<=1
UNSAT!
Explanation: x<=1; y=1; x+y=3; Time: 0msAn optional objective function can be given to maximize or minimize the value of a linear expression.
> simplex min(-2x-3y-4z) 3x+2y+z<=10 2x+5y+3z<=15 x>=0 y>=0 z>=0
SAT! (optimal)
Solution: x=0; y=0; z=5; Optimum: -20
Time: 0ms> simplex max(x) x>=-1 x>=-1/2
UNSAT! (feasible, but unbounded)
Solution: x=-1/2;
Time: 0msClone the git repository:
git clone https://github.com/paultristanwagner/satisfiability-checking.git
Navigate into the created directory:
cd satisfiability-checking
Let Maven build the project:
mvn package
Run the project:
java -jar target/satchecking-1.0-SNAPSHOT.jar
Now you should see the command prompt indicated by a > symbol.