MOLOSS, a MOdal LOgic Satisfiability Solver

MOLOSS is a satisfiability solver for modal logics. It is an implementation (and more) of C. Aceres, P. Fontaine and S. Merz paper "Modal Satisfiability via SMT solving" in which the authors use a translation of propositional modal logic to first-order logic.

Copyright

MOLOSS is licensed under the GNU General Public License v3. See the COPYING file for more details.

Installation

For the moment, you can only install MOLOSS manually. To install MOLOSS, you need:

• an OCaml compiler (version >= 4.0.3)
• the Menhir parser generator
• the OCaml library mSat
• the OCaml library ocaml-minisat to interact with the MiniSat solver

All these tools can be easily installed using the OPAM OCaml Package Manager:

opam install menhir msat minisat
eval $(opam config env)

You can then build the system with

make

The previous command will build a native and byte code executable. You may also use more specific targets:

• profile for native code executable with profiling
• debug for byte code executable with debug
• static for static native code executable with no dynamic libraries (even libc)

Notice also that:

• (for the moment) MOLOSS uses UNIX system calls, so you must be on a UNIX/Linux system to use it
• MOLOSS uses Z3, a SMT solver. You must have a Z3 installed if you want to use it as an oracle or directly (see further).

Documentation

You can find the documentation online.

Usage

The moloss executable takes as an argument a file containing the formula to be checked in InToHyLo format (see examples in the data directory or 4.1). MOLOSS then output SAT or UNSAT. By default, MiniSat is used as an oracle.

MOLOSS implements some frame axioms that can be called as an option of the execautable:

• -S or -M: reflexiv relation
• -B: symmetric relation
• -4: transitive relation
• -5: euclidian relation
• -CD: functionnal relation

Options:

• --all: all SAT oracles are used (MiniSat, Z3, mSAT)
• --z3, --mSAT: only the corresponding oracle is used
• --time: print the total execution time (including parsing)
• --get-model: print the Kripke model if the formula is satisfiable in the Flat Kripke Model (FKM) format.
• --get-assert: print the assertions made by the solver and the final model if the formule is satisfiable.
• --direct: use Z3 as a first-order solver on the translation of modal formulas into first-order formulas (no instanciation procedures)
• --get-log: print the log of interaction with the z3 SMT solver (only for direct mode)
• --soft: use assert-soft constraints, even if not needed by the considered modal logic
• --soft-ignore: do not use assert-soft constraints, even if needed (beware, infinite loop possible in this case!)

Not yet avaible options:

• --get-proof: print a proof unsatisfiability if the formula is unsatisfiable (Z3 only)

Acknowledgments

MOLOSS has been partly developed during an internship at ISAE-SUPAERO and ONERA.