AbHS

A propositional abduction solver based on the implicit hitting set paradigm

About

AbHS is implements a hybrid SAT-IP approach, as outlined in [1], to the propositional propositional abduction problem based on the implicit hitting set paradigm [1,2]. AbHS is developed by the Constraint Optimization and Reasoning Group at the Department of Computer Science, University of Helsinki. The system is implemented by Paul Saikko.

Propositional Abduction

In short, an instance of the propositional abduction problem consists of a set M of manifestations (or observations) which we are to explain by a subset of a set H of hypotheses. Such a subset of hypotheses, together with a background theory T, is a solution to the given abduction problem if (i) it entails the manifestations and (ii) is consistent. Here we are interested in minimum-cost explanations under a given cost function over the subsets of H, defined as the sum of the weights of the hypotheses in the subset. For more details, see [1].

Input Format

AbHS accepts input very similar to the WCNF file format used for e.g. weighted partial maximum satisfiability. A list of literals which correspond to manifestations is listed on an additional 'm' line. The set of hypothesis and the theory are expressed in CNF as soft and hard clauses, respectively.

For instance, example 7 from [1] is encoded as follows

p wcnf 4 5 4   
m 4 0
4 -1 -2 4 0
4 -1 -3 4 0
1 1 0
1 2 0
2 3 0

Downloads

AbHS is available in open source under the MIT license at GitHub. AbHS requires the IBM CPLEX solver, for which an academic license is available at no cost.

Benchmarks. The set of benchmarks described and used in [1] are available here (ASP) and here (AbHS).

Disjunctive ASP encoding of propositional abduction in the input format of clingo, as used in [1] to compare against AbHS, is available here.

To compute minimum-cost explanations, add ASP facts encoding an instance of propositional abduction as follows:

variable(X).       ... variable in instance
hclause(H).        ... clause H in theory
sclause(S,W).      ... clause in hypotheses with cost W 
manifestation(M).  ... manifestation clause M  
pos(C,X).          ... positive literal X in clause C
neg(C,Y).          ... negative literal Y in clause C

For instance, the example from above is encoded as follows

variable(1). variable(2). variable(3). variable(4).
hclause(h1). pos(h1,4). neg(h1,1). neg(h1,2).
hclause(h2). pos(h2,4). neg(h2,1). neg(h2,3).
sclause(s1,1). pos(s1,1).
sclause(s2,1). pos(s2,2).
sclause(s3,2). pos(s3,3).
manifestation(m). pos(m,4).

References

[1] Paul Saikko, Johannes P. Wallner, and Matti Järvisalo: Implicit Hitting Set Algorithms for Reasoning Beyond NP. KR 2016.

[2] Erick Moreno-Centeno and Richard M. Karp: The implicit hitting set approach to solve combinatorial optimization problems with an application to multi-genome alignment. Operations Research 61(2) 2013, 453-468.