Inconsistency Proofs for ASP: The ASP-DRUPE Format
This addresses the challenge of verifying inconsistency claims in ASP solvers, which is incremental as it adapts an existing proof format from Boolean satisfiability to ASP.
The paper tackles the problem of verifying inconsistency in Answer Set Programming (ASP) by developing the ASP-DRUPE proof format, based on Reverse Unit Propagation, and implements it in the wasp solver for normal logic programs.
Answer Set Programming (ASP) solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether a logic program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for (normal) programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive logic programs, including weight and choice rules. ASP-DRUPE is based on the Reverse Unit Propagation (RUP) format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers. Later, we provide an implementation of ASP-DRUPE into the wasp solver for normal logic programs. This work is under consideration for acceptance in TPLP.