PV4 ⊧ MonoSATproduces a satisfiability result for a formula

SMT solver for monotonic theories over Booleans and bitvectors

Application domain/field

• SMT solving
• SAT Modulo Theory
• Satisfiability modulo theories (SMT)
• Monotonic theories

Type of tool

SMT solver

Expected input

SAT problem

Format:

One of several options:

• It can be used via the Python 3 library
• It can be used via the Java library
• It can be used via the commandline, then it requires a .gnf file (this is an extension of the DIMACS format with e.g. bitvector support)

Expected output

SAT or UNSAT

Internals

The idea is to build an SMT solver for monotonic theories, for which they can create efficient SMT solvers. They claim that many common problems can be solved with this, including reachability, shortest paths, minimum spanning trees, etc.