Home

DPLL(T) Interactive Lab

SAT-solver + theory solver cooperation for SMT solving

T = UF
Formula Input Theory: UF
UF atoms: a=b, f(a)!=b, g(a,b)=c  |  Boolean: & | ! -> <->
Algorithm Flow
φ tr(φ) CNF sat SAT Solver ▾ click to choose unsat tr⁻¹(φₘ) sat T ▾ click to choose unsat sat F ∧ ¬φₘ unsat
—
Load a formula to begin.
Formula Trace
φ —
tr(φ) —
Propositional —
CNF —
UF Literals —
SAT Solver
Theory Solver (T)