PV4 ⊧ MathSATproduces a satisfiability result for a formula

Application domain/field

• SMT solving
• Satisfiability Module Theories (SMT) solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB v2, SMT-LIB v1.2 or DIMACS.

Expected output

SAT or UNSAT indicating whether the formula is satisfiable or not. When the formula is satisfiable, it can also produce a satisfying interpretation on domain variables. When the formula is unsatisfiable, it can produce a proof.

Comments

Current version: MathSAT 5