Bruno Zanuttini

The ZL Abduction Solver

What is ZLAS?

ZLAS is a solver for propositional abduction problems, developed by Florian Letombe (at this time at the CRIL, Université d'Artois, France) and Bruno Zanuttini (GREYC, Université de Caen Basse-Normandie, France) since December, 2006.

Abduction is the process of finding explanations for observed manifestations. Formally, we are given:

Then an explanation is a subset E of H such that the conjunction of KB and E is consistent (satisfiable) and entails q.

The aim of ZLAS is to solve the decision problem associated to abduction : given an instance, is there at least one explanation? Its algorithm consists in a DPLL-like exploration of the search space constituted by all combinations of hypotheses, enhanced by various conditions for pruning subtrees of the search space off together with various heuristics for deciding the next hypothesis on which to branch.

Among others, an advantage of ZLAS is to take benefit of very efficient SAT solvers. We currently use minisat, by Niklas Eénand Niklas Sörensson.

Download and quick guide

ZLAS comes as a single executable file, compiled for Linux and downloadable here : download ZLAS. No installation is needed, simply save the file to your disk.

ZLAS reads from standard input or from a text file abduction problems written in ADIMACS format. The main features of this format (inspired from the DIMACS format for CNF formulas) are the following :

The following is an example of this format.

      c Example ADIMACS file.
      p cnf 4 5
      q 3
      h 1 -1 2 0
      1 2 3 0
      -1 -4 0
      -2 -3 -4 0
      1 3 4 0
      2 3 -4 0

ZLAS either writes "No explanation" to standard output and returns 20, or writes "Explanation exists" and returns 10. Some additional logging information is written to the error stream.

The behaviour of ZLAS can be tuned by choosing a heuristics for hypotheses. This is specified by a -hx option, where x is a single-letter identifier for the heuristics. By default, no heuristic is used, i.e., hypotheses are considered in the order in which they are given in the instance definition.

The behaviour of ZLAS can also be tuned by choosing pruning conditions for the search tree. This is specified by a -pxy...z option, where x, y, ..., z are single-letters identifiers for "pruners". By default, none is used, but you should always use at least -peqn, since they come with almost no computing overhead but may prune large subtrees off. According to our last experiments, -peqnu is the best choice.

To get help, run zlas h e l p m e (mandatory spaces).

Source code and documentation

ZLAS is written in C++. Its implementation is fully documented here : consult ZLAS implementation documentation. Its source code is available here (single tgz file) : download ZLAS source code.

An article (in French) was published in the conference JFPC 2007 ("Troisièmes Journées Francophones de Programmation par Contraintes"). See Bruno Zanuttini's publications.

Related work

Other projects aim(ed) at producing efficient abduction solvers :

Bruno Zanuttini XHTML 1.0 Strict valid CSS valid