idsat is a tool which implements a reduction of the ID-logic language to propositional satisfiability. Additionally, the tool can call a SAT solver on the translation and so it can be used as a model generator for ID-logic.
The system implements the following translations:
- full[:(1|2)] (one-to-one)
- Based on the alternating fixpoint procedure. The system computes an upper bound on the number of alternations. Then for each alternation there is a copy in the translation of the original program which models the fixpoint computation.
- semi[:(1|2)] (one-to-one)
- Also based on the alternating fixpoint computation but there is a single copy of the program for deriving positive literals and as many copies of the program for deriving negative literals as there are alternations.
- weak[:(1|2|3|4)] (one-to-many)
- This is the smallest translation and is based on modeling the levels of the well-founded operator WP based on weak level-mappings.
The optional number :N specifies a variation of the translation. Run idsat --help for more details.
Download the latest version: idsat-0.9.5.
- Download lparse from here.
- Unpack and patch lparse:
tar xfz lparse-1.0.XX.tar.gz cd lparse-1.0.XX patch -p1 < ../path/to/idsat/lparse-1.0.15.patch
- Compile and install lparse:
cd lparse-1.0.XX ./configure make make install
- (Optional) The idsat solver is written in perl. If your perl
executable is not in /usr/bin/perl,
edit the first line of idsat to point to the correct path of perl.
- Install one of the following sat solvers:
* the solver can compute all solutions.
lparse idl_theory.lp | ./idsat [-t trans]
This translates an ID-logic theory to a propositional theory (in DIMACS cnf format) where trans is an optional translation to use.
lparse idl_theory.lp | ./idsat [-t trans] -s sat-solver
This computes a model of an ID-logic theory by calling a SAT solver sat-solver and trans is as above.
- N. Pelov and E. Ternovska.
Reducing Inductive Definitions to Propositional Satisfiability.
(The paper describes only the
LINKSOther implementations of ID-logic:
- Asystem - an abductive system implementing a subset of ID-logic.
- IDP - a native implementation of a model generator for ID-logic.