MinisatID is a complete, combinatorial search algorithm, mainly supporting the ground fragment of the language FO(·)-IDP. The solver is used, among others, as search backend of the IDP Knowledge Base system.
- Accepts input in the languages CNF, ECNF (native format), OPB (pseudo-boolean) QBF, FlatZinc and ground Lparse.
- Can transform the input theory into CNF or FlatZinc.
- Extensible, open-source research solver.
- High performance: 4th place of 16 in the 2nd ASP competition, eye-to-eye with clasp (winner) in the NP category in the 3rd ASP competition.
- Extends the SAT solver MiniSat using the DPLL(T) architecture.
- Efficient propagation for pseudo-boolean aggregate expressions (e.g. cardinality).
- Unfounded set detection algorithms to support inductive definitions (e.g. reachability).
- Branch-and-bounds optimization.
- Lazy clause generation for finite domain constraints (over integers).
- Integration with the constraint programming engine gecode.
- Dynamic symmetry breaking using minisat-SPFS as backend (to be integrated soon).
- Interface for incrementally adding any type of variable or constraint, minimally disturbing the current state (used in lazy grounding algorithms).
Developed by Broes De Cat and formerly by Maarten Mariën.
Extract, run cmake (cmake-gui) and make to compile (requires g++ >= 4.6, cmake and bison >= 2.5). Tested using gcc 4.6 on mac, linux and windows, if any problems arise, please let us know.
For usage information, use -h or read the provided input format file (requires pdflatex to compile).