×

Constraint answer set solver {ezcsp} and why integration schemas matter. (English) Zbl 1379.68038

Summary: Researchers in answer set programming and constraint programming have spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming. Constraint answer set programming languages and systems proved to be successful at providing declarative, yet efficient solutions to problems involving hybrid reasoning tasks. One of the main contributions of this paper is the first comprehensive account of the constraint answer set language and solver {ezcsp}, a mainstream representative of this research area that has been used in various successful applications. We also develop an extension of the transition systems proposed by R. Nieuwenhuis et al. [J. ACM 53, No. 6, 937–977 (2006; Zbl 1326.68164)] to capture Boolean satisfiability solvers. We use this extension to describe the {ezcsp} algorithm and prove formal claims about it. The design and algorithmic details behind {ezcsp} clearly demonstrate that the development of the hybrid systems of this kind is challenging. Many questions arise when one faces various design choices in an attempt to maximize system’s benefits. One of the key decisions that a developer of a hybrid solver makes is settling on a particular integration schema within its implementation. Thus, another important contribution of this paper is a thorough case study based on {ezcsp}, focused on the various integration schemas that it provides.

MSC:

68N17 Logic programming
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T27 Logic in artificial intelligence
68T30 Knowledge representation

Citations:

Zbl 1326.68164
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] AngerC., GebserM., JanhunenT. and SchaubT.2006. What’s a head without a body? In Proc. of the European Conference on Artificial Intelligence (ECAI’06), 769-770.
[2] BalducciniM.2009. Representing constraint satisfaction problems in answer set programming. In Proc. of ICLP09 Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP09).
[3] BalducciniM.2011. Industrial-size scheduling with ASP+CP. In Proc. of 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR11), J. P.Delgrande and W.Faber, Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 6645. Springer Verlag, Berlin, 284-296. · Zbl 1327.90066
[4] BalducciniM. and LierlerY.2012. Practical and methodological aspects of the use of cutting-edge ASP tools. In Proc. of 14th International Symposium on Practical Aspects of Declarative Languages (PADL 2012), C.Russo and N.-F.Zhou, Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 7149. Springer Verlag, Berlin, 78-92.
[5] BartholomewM. and LeeJ.2014. System aspmt2smt: Computing ASPMT theories by SMT solvers. In Proc. of European Conference on Logics in Artificial Intelligence, JELIA, Springer, 529-542.
[6] BrewkaG., EiterT. and TruszczyńskiM.2011. Answer set programming at a glance. Communications of the ACM54(12), 92-103.
[7] CalimeriF., CozzaS. and IanniG.2007. External sources of knowledge and value invention in logic programming. Annals of Mathematics and Artificial Intelligence50, 3-4, 333-361.10.1007/s10472-007-9076-z · Zbl 1125.68026
[8] CalimeriF., CozzaS., IanniG. and LeoneN.2008. Computable functions in ASP: theory and implementation. In Proc. of International Conference on Logic Programming (ICLP), 407-424.
[9] CalimeriF., IanniG., RiccaF., AlvianoM., BriaA., CatalanoG., CozzaS., FaberW., FebbraroO., LeoneN., MannaM., MartelloA., PanettaC., PerriS., RealeK., SantoroM. C., SirianniM., TerracinaG. and VeltriP.2011. The third answer set programming competition: Preliminary report of the system competition track. In Proc. of the International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Springer-Verlag, Berlin, Heidelberg, 388-403.
[10] CarlssonM. and MildnerP.2012. SICStus Prolog-the first 25 years. Theory and Practice of Logic Programming12, 1-2 (Jan.), 35-66.10.1017/S1471068411000482 · Zbl 1244.68016
[11] CatB. D., BogaertsB. and DeneckerM.2014. MiniSAT(ID) for satisfiability checking and constraint solving. In ALP Newsletter Feautured Article. URL: https://www.cs.nmsu.edu/ALP/2014/09/minisatid-for-satisfiability-checking-and-constraint-solving/
[12] DavisM., LogemannG. and LovelandD.1962. A machine program for theorem proving. Communications of the ACM5(7), 394-397.10.1145/368273.368557 · Zbl 0217.54002
[13] De MouraL. and BjørnerN.2008. Z3: An efficient SMT solver. In Proc. of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 337-340.
[14] DeneckerM., VennekensJ., BondS., GebserM. and TruszczyńskiM.2009. The second answer set programming system competition. In Proc. of the International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), E.Erdem, F.Lin, and T.Schaub, Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 5753. Springer, Berlin Heidelberg.
[15] DovierA., FormisanoA. and PontelliE.2011. Perspectives on logic-based approaches for reasoning. In Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning: Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday. Lecture Notes in Artificial Intelligence (LNCS). Springer Verlag, Berlin, 259-279.
[16] DrescherC. and WalshT.2011. A translational approach to constraint answer set solving. Theory and Practice of Logic Programming (TPLP)10, 4-6, 465-480. · Zbl 1209.68511
[17] EénN. and BiereA.2005. Effective preprocessing in SAT through variable and clause elimination. In Proc. of the International Conference on Theory and Applications of Satisfiability Testing. Springer, Berlin Heidelberg, 61-75.
[18] EénN. and SörenssonN.2003. An extensible SAT-solver. In Proc. of the International Conference on Theory and Applications of Satisfiability Testing. Springer, Berlin Heidelberg, 502-518.
[19] EiterT., IanniG., SchindlauerR. and TompitsH.2005. A uniform integration of higher-order reasoning and external evaluations in answer set programming. In Proc. International Joint Conference on Artificial Intelligence (IJCAI). Professional Book Center, 90-96.
[20] ElkabaniI., PontelliE. and SonT. C.2004. Smodels with CLP and its applications: A simple and effective approach to aggregates in ASP. In Proc. of the International Conference on Logic Programming, B.Demoen and V.Lifschitz, Eds. Lecture Notes in Computer Science, vol. 3132. Springer, 73-89.
[21] FerrarisP. and LifschitzV.2005. Weight constraints as nested expressions. Theory and Practice of Logic Programming5, 45-74.10.1017/S1471068403001923S1471068403001923 · Zbl 1093.68017
[22] GebserM., KaufmannB., NeumannA. and SchaubT.2007. Conflict-driven answer set solving. In Proc. 20th International Joint Conference on Artificial Intelligence (IJCAI’07), MIT Press, 386-392.
[23] GebserM., LiuL., NamasivayamG., NeumannA., SchaubT. and TruszczyńskiM.2007. The first answer set programming system competition. In Proc. the International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), C.Baral, G.Brewka, and J.Schlipf, Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 4483. Springer, Berlin Heidelberg, 3-17.
[24] GebserM., OstrowskiM. and SchaubT.2009. Constraint answer set solving. In Proc. of 25th International Conference on Logic Programming (ICLP), P. M.Hill and D. S.Warren, Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 5649. Springer, Berlin Heidelberg, 235-249.
[25] GebserM., SchaubT. and ThieleS.2007. Gringo: A new grounder for answer set programming. In Logic Programming and Nonmonotonic Reasoning, C.Baral, G.Brewka, and J.Schlipf, Eds. Lecture Notes in Computer Science, vol. 4483. Springer, Berlin Heidelberg, 266-271.
[26] GelfondM. and LifschitzV.1998. Action languages^11. Electronic Transactions on Artificial Intelligence3, 195-210.
[27] GiunchigliaE., LeoneN. and MarateaM.2008. On the relation among answer set solvers. Annals of Mathematics and Artificial Intelligence53, 1-4, 169-204.10.1007/s10472-009-9113-1 · Zbl 1165.68333
[28] GiunchigliaE., LierlerY. and MarateaM.2006. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning36, 345-377. · Zbl 1107.68029
[29] GomesC. P., KautzH., SabharwalA. and SelmanB.2008. Satisfiability solvers. In Handbook of Knowledge Representation, F.van Harmelen, V.Lifschitz, and B.Porter, Eds. Elsevier, 89-134.
[30] JaffarJ. and MaherM. J.1994. Constraint logic programming: A survey. The Journal of Logic Programming 1920, Supplement 1, 503-581. Special Issue: Ten Years of Logic Programming.
[31] JanhunenT., LiuG. and NiemelI.2011. Tight integration of non-ground answer set programming and satisfiability modulo theories. In Working notes of the 1st Workshop on Grounding and Transformations for Theories with Variables.
[32] LeeJ.2005. A model-theoretic counterpart of loop formulas. In Proc. International Joint Conference on Artificial Intelligence (IJCAI). Professional Book Center, 503-508.
[33] LierlerY.2014. Relating constraint answer set programming languages and algorithms. Artificial Intelligence207C, 1-22. · Zbl 1334.68041
[34] LierlerY., SmithS., TruszczyńskiM. and WestlundA.2012. Weighted-sequence problem: ASP versus CASP and declarative versus problem oriented solving. In Proc. of 14th International Symposium on Practical Aspects of Declarative Languages (PADL), C. V.Russo and N.-F.Zhou, Eds. Lecture Notes in Computer Science, vol. 7149. Springer Verlag, Berlin.
[35] LierlerY. and TruszczyńskiM.2011. Transition systems for model generators - A unifying approach. Theory and Practice of Logic Programming, 27th Int’l. Conference on Logic Programming (ICLP’11) Special Issue11, 4-5, 629-646. · Zbl 1222.68063
[36] LifschitzV., TangL. R. and TurnerH.1999. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence25, 369-389.10.1023/A:1018978005636 · Zbl 0940.68075
[37] LiuG., JanhunenT. and NiemeläI.2012. Answer set programming via mixed integer programming. In Principles of Knowledge Representation and Reasoning: Proceedings of the 13th International Conference. AAAI Press, 32-42.
[38] MarekV. and TruszczyńskiM.1999. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm: a 25-Year Perspective. Springer Verlag, 375-398.10.1007/978-3-642-60085-2_17 · Zbl 0979.68524
[39] MarriottK., NethercoteN., RafehR., StuckeyP. J., GarciaDe La Banda, M. and WallaceM.2008. The design of the Zinc modelling language. Constraints13, 3 (September), 229-267.10.1007/s10601-008-9041-4 · Zbl 1146.68352
[40] MellarkodV. S., GelfondM. and ZhangY.2008. Integrating answer set programming and constraint logic programming. Annals of Mathematics and Artificial Intelligence53, 1-4, 251-287.10.1007/s10472-009-9116-y · Zbl 1165.68504
[41] NiemeläI.1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence25, 241-273.10.1023/A:1018930122475 · Zbl 0940.68018
[42] NiemeläI. and SimonsP.2000. Extending the Smodels system with cardinality and weight constraints. In Logic-Based Artificial Intelligence, J.Minker, Ed. Kluwer, 491-521.10.1007/978-1-4615-1567-8 · Zbl 0979.68015
[43] NieuwenhuisR., OliverasA. and TinelliC.2006. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM53(6), 937-977.10.1145/1217856.1217859 · Zbl 1326.68164
[44] RossiF., van BeekP. and WalshT.2008. Constraint programming. In Handbook of Knowledge Representation, F.van Harmelen, V.Lifschitz, and B.Porter, Eds. Elsevier, 181-212.
[45] SchulteC. and StuckeyP. J.2008. Efficient constraint propagation engines. Transactions on Programming Languages and Systems31(1), 2:1-2:43.
[46] SimonsP., NiemeläI. and SoininenT.2002. Extending and implementing the stable model semantics. Artificial Intelligence138, 181-234.10.1016/S0004-3702(02)00187-X · Zbl 0995.68021
[47] SusmanB. and LierlerY.2016. SMT-based constraint answer set solver EZSMT (system description). In International Conference on Logic Programming (ICLP).
[48] Van GelderA., RossK. and SchlipfJ.1991. The well-founded semantics for general logic programs. Journal of ACM38, 3, 620-650. · Zbl 0799.68045
[49] WittocxJ., MariënM. and DeneckerM.2008. The idp system: A model expansion system for an extension of classical logic. In Proceedings of Workshop on Logic and Search, Computation of Structures from Declarative Descriptions (LaSh). Electronic, 153-165. URL: https://lirias.kuleuven.be/bitstream/123456789/229814/1/lash08.pdf [Accessed on June 16, 2017].
[50] ZhangL., MadiganC. F., MoskewiczM. W. and MalikS.2001. Efficient conflict driven learning in a Boolean satisfiability solver. In Proc. of 2001 IEEE/ACM International Conference on Computer-Aided Design (ICCAD-01). 279-285.
[51] ZhouN.-F.2012. The language features and architecture of B-Prolog. Journal of Theory and Practice of Logic Programming (TPLP)12, 1-2 (January), 189-218.10.1017/S1471068411000445 · Zbl 1244.68024
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.