Download | Documentation | Citation
MinisatID is a SAT(ID,Agg) solver, a model generator for propositional FO(·)IDP. It is the search component of the knowledge base system IDP. MinisatID is an extension of the SAT solver 
MiniSat.
Features
- Minisat backend.
- Combination of constraint propagation engine and DPLL(T) search framework.
- Currently supporting aggregate expressions (sum, cardinality, min, max, product), inductive definitions and branch-and-bound optimization.
- Supports input in CNF (SAT), ECNF (native), ground-LParse (ASP), QBF (QBF-lib) and OPB (pseudo-boolean).
- 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.
Usage
Extract, configure and make to compile (requires g++ >= 4.2 and autotools). Tested using gcc 4.4 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).
Developed by Maarten Mariën and Broes De Cat.