## AbHS## A propositional abduction solver based on the implicit hitting set paradigm## AboutAbHS 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 ## Input FormatAbHS 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
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. |