PySMT
Edit and run PySMT scripts in the browser — Boolean logic, linear arithmetic, quantifiers, UF, and bit-vectors with a live z3 backend.
Explore →Horn Clause Solver
Linear-time satisfiability for Horn CNF formulas — unit propagation until fixpoint.
Explore →Tseytin Transformation
Convert a propositional formula to an equisatisfiable CNF — one sub-formula at a time.
Explore →DPLL
Davis–Putnam–Logemann–Loveland algorithm — backtracking SAT solving with unit propagation and pure literal elimination.
Explore →Basic CDCL
Conflict-Driven Clause Learning without non-chronological backjumping — build your intuition for conflict analysis.
Explore →CDCL
Full Conflict-Driven Clause Learning with UIP-based conflict analysis and non-chronological backjumping.
Explore →Term Flattening
EUF pre-processing — transform a cube into an equisatisfiable flat cube, one rewrite rule at a time.
Explore →Congruence Closure
EUF theory solver — decide satisfiability of a flat cube using equivalence classes and the CC algorithm.
Explore →Union-Find
Interactive Union-Find data structure with path compression and union by rank — building block for CC.
Explore →DPLL(T)
DPLL modulo theories — combine a SAT solver (DPLL / Basic CDCL / CDCL) with a theory solver (Union-Find or CC).
Explore →Integer Difference Logic (IDL)
Decide QF_IDL satisfiability by building a constraint graph and detecting negative cycles via Bellman-Ford.
Explore →Ackermanization
Reduce QF_UF to QF_EQ — replace function applications with fresh constants and add congruence axioms.
Explore →Bit Blasting (BV-Flattening)
Reduce bit-vector constraints to propositional logic — equality, bitwise ops, addition, subtraction, and multiplication.
Explore →Prenex Normal Form (PNF)
Convert a first-order formula to PNF in four steps: eliminate →/↔, push ¬ inward, rename variables, pull quantifiers out.
Explore →