idsat

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 W_P 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.

INSTALLATION

1. Download lparse from here.
2. 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
   

3. Compile and install lparse:

   cd lparse-1.0.XX
   ./configure
   make
   make install
   

4. (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.
5. Install one of the following sat solvers:
   • relsat*
   • sato*
   • satz
   • siege
   • zchaff
   • berkmin
   • walksat

   * the solver can compute all solutions.

USAGE

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.

PUBLICATIONS

1. N. Pelov and E. Ternovska. Reducing Inductive Definitions to Propositional Satisfiability. ICLP 2005.
   (The paper describes only the weak:3 reduction.)

LINKS

Other 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.

Reductions to SAT under the stable semantics:

• ASSAT
• cmodels
• lp2sat

ACKNOWLEDGEMENT

This project is a joint work with Prof. Eugenia Ternovska and was done during a post-doc at the Computational Logic group at Simon Fraser University. Their support is greatly appreciated.