ASP-QRAT: A Conditionally Optimal Dual Proof System for ASP

Answer Set Programming (ASP) is a declarative programming approach

that captures many problems in knowledge representation and reasoning.

To certify an ASP solver's decision, whether the program is

consistent or inconsistent, we need a certificate or proof that can

be independently verified.

This paper proposes the dual proof system ASP-QRAT that certifies both

consistent and inconsistent ASPs. ASP-QRAT is based on a translation

of ASP to QBF (Quantified Boolean Formus) and the QBF proof system

QRAT as a checking format.

We show that ASP-QRAT p-simulates ASP-DRUPE, an existing refutation

system for inconsistent disjunctive ASPs. We show that ASP-QRAT is

conditionally optimal for consistent and inconsistent ASPs, i.e.,

any super-polynomial lower bound on the shortest proof size of

ASP-QRAT implies a major breakthrough in theoretical computer science.

The case for consistent ASPs is remarkable

because no analog exists in the QBF case.