Concept
Smt solver
Books
Journey Statuslearning Tags
A Decision procedure that determines satisfiability of formulas in first-order logic with theories (like arithmetic, arrays, bit-vectors), extending SAT solver to richer domains.
A decision procedure that determines satisfiability of formulas in first-order logic with theories (like arithmetic, arrays, bit-vectors), extending SAT to richer domains.