PV4 MathSATproduces a satisfiability result for a formula

Application domain/field

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
SMT

Links

Last commit date

23 April 2021 (based on https://mathsat.fbk.eu/releasenotes.html)

Related papers

https://doi.org/10.1007/978-3-642-36742-7_7

Last publication date

2013

Related tools

Successor of MathSAT 4

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.