×

Inconsistency proofs for ASP: the ASP-DRUPE format. (English) Zbl 1434.68065

Summary: 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.

MSC:

68N17 Logic programming
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alviano, M., Dodaro, C., Leone, N., and Ricca, F.2015. Advances in WASP. In LPNMR 2015. LNCS, vol. 9345. Springer, 40-54. · Zbl 1467.68021
[2] Alviano, M., Dodaro, C., and Maratea, M.2018. Shared aggregate sets in answer set programming. TPLP 18, 3-4, 301-318. · Zbl 1451.68062
[3] Balduccini, M., Gelfond, M., and Nogueira, M.2006. Answer set based design of knowledge systems. Ann. Math. Artif. Intell. 47,1-2, 183-219. · Zbl 1105.68105
[4] Bomanson, J., Gebser, M., Janhunen, T., Kaufmann, B., and Schaub, T.2016. Answer set programming modulo acyclicity. Fundam. Inform. 147, 1, 63-91. · Zbl 1373.68170
[5] Brewka, G., Eiter, T., and Truszczyński, M.2011. Answer set programming at a glance. Communications of the ACM 54, 12, 92-103.
[6] Calimeri, F., Faber, W., Gebser, M., Ianni, G., Kaminski, R., Krennwallner, T., Leone, N., Ricca, F., and Schaub, T.2015. ASP-core-2 input language format.
[7] Clark, K. L.1977. Negation as failure. In Symposium on Logic and Data Bases 1977. Advances in Data Base Theory. Plemum Press, 293-322.
[8] Cruz-Filipe, L., Heule, M. J. H., Jr., W. A. H., Kaufmann, M., and Schneider-Kamp, P.2017. Efficient certified RAT verification. In CADE 2017. LNCS, vol. 10395. Springer, 220-236. · Zbl 1494.68284
[9] Eén, N. and Biere, A.2005. Effective preprocessing in SAT through variable and clause elimination. In SAT 2005. LNCS, vol. 3569. Springer, 61-75. · Zbl 1128.68463
[10] Faber, W.2005. Unfounded sets for disjunctive logic programs with arbitrary aggregates. In LPNMR 2005. LNCS, vol. 3662. Springer, 40-52. · Zbl 1152.68405
[11] Faber, W., Pfeifer, G., and Leone, N.2011. Semantics and complexity of recursive aggregates in answer set programming. Artif. Intell. 175, 1, 278-298. · Zbl 1216.68263
[12] Fages, F.1994. Consistency of clark’s completion and existence of stable models. Meth. of Logic in CS 1, 1, 51-60.
[13] Ferraris, P.2011. Logic programs with propositional connectives and aggregates. ACM Trans. Comput. Log. 12, 4, 25:1-25:40. · Zbl 1351.68053
[14] Gebser, M., Guziolowski, C., Ivanchev, M., Schaub, T., Siegel, A., Thiele, S., and Veber, P.2010. Repair and prediction (under inconsistency) in large biological networks with answer set programming. In KR 2010. The AAAI Press, 497-507.
[15] Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., and Wanko, P.2016. Theory solving made easy with clingo 5. In ICLP (Tech. C.). OASICS, vol. 52. Dagstuhl Pub., 2:1-2:15.
[16] Gebser, M., Kaminski, R., Kaufmann, B., and Schaub, T.2011. Multi-Criteria Optimization in Answer Set Programming. In ICLP 2011. LIPIcs, vol. 11. Dagstuhl Pub., 1-10. · Zbl 1245.68052
[17] Gebser, M., Kaminski, R., Kaufmann, B., and Schaub, T.2012. Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers. · Zbl 1251.68060
[18] Gebser, M., Kaufmann, B., Neumann, A., and Schaub, T.2008. Advanced preprocessing for answer set solving. In ECAI 2008. Frontiers in Artificial Intelligence and Applications, vol. 178. IOS Press, 15-19.
[19] Gebser, M., Obermeier, P., Ratsch-Heitmann, M., Runge, M., and Schaub, T.2018. Routing driverless transport vehicles in car assembly with answer set programming. CoRR abs/1804.10437. · Zbl 06988659
[20] Gebser, M., Schaub, T., Thiele, S., and Veber, P.2011. Detecting inconsistencies in large biological networks with answer set programming. TPLP 11, 2-3, 323-360. · Zbl 1220.68036
[21] Gelder, A. V.2008. Verifying RUP proofs of propositional unsatisfiability. In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2008, Fort Lauderdale, Florida, USA, January 2-4, 2008.
[22] Gelfond, M. and Zhang, Y.2014. Vicious circle principle and logic programs with aggregates. TPLP 14, 4-5, 587-601. · Zbl 1309.68032
[23] Goldberg, E. I. and Novikov, Y.2003. Verification of proofs of unsatisfiability for CNF formulas. In DATE. IEEE Computer Society, 10886-10891.
[24] Guziolowski, C., Videla, S., Eduati, F., Thiele, S., Cokelaer, T., Siegel, A., and Saez-Rodriguez, J.2013. Exhaustively characterizing feasible logic models of a signaling network using answer set programming. Bioinformatics 29, 18, 2320-2326. Erratum see Bioinformatics 30, 13, 1942.
[25] Haubelt, C., Neubauer, K., Schaub, T., and Wanko, P.2018. Design space exploration with answer set programming. KI - Künstliche Intelligenz 32, 2, 205-206.
[26] Heule, M., HuntJr., W. A., and Wetzler, N.2013. Verifying refutations with extended resolution. In CADE 2013. LNCS, vol. 7898. Springer, 345-359. · Zbl 1381.68270
[27] Heule, M., HuntJr., W. A., and Wetzler, N.2015. Expressing symmetry breaking in DRAT proofs. In CADE 2015. LNCS, vol. 9195. Springer, 591-606. · Zbl 1465.68285
[28] Heule, M., Seidl, M., and Biere, A.2014. A unified proof system for QBF preprocessing. In IJCAR. LNCS, vol. 8562. Springer, 91-106. · Zbl 1409.68257
[29] Janhunen, T.2006. Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics 16, 1-2, 35-86. · Zbl 1184.68160
[30] Kiesl, B., Rebola-Pardo, A., and Heule, M. J. H.2018. Extended resolution simulates DRAT. In IJCAR 2018. LNCS, vol. 10900. Springer, 516-531. · Zbl 1441.68278
[31] Lin, F. and Zhao, J.2003. On tight logic programs and yet another translation from normal logic programs to propositional logic. In IJCAI’03. Morgan Kaufmann, 853-858.
[32] Liu, L., Pontelli, E., Son, T. C., and Truszczynski, M.2010. Logic programs with abstract constraint atoms: The role of computations. Artif. Intell. 174, 3-4, 295-315. · Zbl 1207.68119
[33] Lonsing, F. and Egly, U.2018. QRAT+: generalizing QRAT by a more powerful QBF redundancy property. In IJCAR. LNCS, vol. 10900. Springer, 161-177. · Zbl 1511.68325
[34] Pearce, D.1999. Stable inference as intuitionistic validity. J. Log. Program. 38, 1, 79-91. · Zbl 0911.68136
[35] Pelov, N., Denecker, M., and Bruynooghe, M.2007. Well-founded and stable semantics of logic programs with aggregates. Theory and Practice of Logic Programming 7, 3, 301-353. · Zbl 1111.68070
[36] Philipp, T. and Rebola-Pardo, A.2016. DRAT proofs for XOR reasoning. In JELIA 2016. LNCS, vol. 10021. Springer, 415-429. · Zbl 1483.68357
[37] Ricca, F., Grasso, G., Alviano, M., Manna, M., Lio, V., Iiritano, S., and Leone, N.2012. Team-building with answer set programming in the Gioia-Tauro seaport. TPLP 12, 361-381. · Zbl 1250.90050
[38] Silva, J. P. M. and Sakallah, K. A.1999. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers 48, 5, 506-521. · Zbl 1392.68388
[39] Son, T. C. and Pontelli, E.2007. A constructive semantic characterization of aggregates in answer set programming. Theory and Practice of Logic Programming 7, 3, 355-375. · Zbl 1111.68072
[40] Syrjänen, T.2000. Lparse 1.0 User’s Manual.
[41] Truszczyński, M.2011. Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs. TPLP 11, 881-904. · Zbl 1242.68052
[42] Wetzler, N., Heule, M., and HuntJr., W. A.2014. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In SAT 2014. LNCS, vol. 8561. Springer, 422-429. · Zbl 1423.68475
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.