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 BasseNormandie, France) since December, 2006.
Abduction is the process of finding explanations for observed manifestations. Formally, we are given:
 a set of propositional variables V,
 a (propositional) knowledge base KB, in CNF, over V,
 a query q, which is a literal over a variable in V,
 a set of hypotheses H, which is a set of literals over variables in V.
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 DPLLlike 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 :

every line beginning with
c
is considered a comment,  variables are represented by integers, among which 0 is not allowed; making so that such variables form a range {1,...,n} may positively affect resolution, since a variable, e.g., 34, implicitly says that variables 1,...,33 may occur in the formula,
 a positive literal is represented by of its variables, and a negative literal by the corresponding integer, negated; e.g., literal "not x12" is represented by 12,

the KB is introduced on a line of the form
p cnf xxx yyy
, wherexxx
is the number of variables in the KB (in fact, the greatest index of one) andyyy
is its number of clauses, 
the query is given on a line of the form
q xx
, wherexx
is the query (negative or positive literal), 
the set of hypotheses is given on a line of the form
h xx yy .. zz 0
, wherexx
,yy
, ...,zz
are the hypotheses (literals), and0
marks the end of the enumeration, 
each clause in the KB is given by a line of the form
xx yy .. zz 0
, wherexx
,yy
, ...,zz
are the literals in the clause, and0
marks the end of the enumeration,  the clauses in the KB are listed, preferrably each on a separate line.
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 singleletter 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 singleletters 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 :
 the QUIP project in Vienna,
 the zres solver by Laurent Simon in Paris and Alvaro del Val in Barcelona.