A propositional abduction solver based on the implicit hitting set paradigm
AbHS is implements a hybrid SAT-IP approach, as outlined in , 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.
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 .
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  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
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.
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).
 Paul Saikko, Johannes P. Wallner, and Matti Järvisalo: Implicit Hitting Set Algorithms for Reasoning Beyond NP. KR 2016.
 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.