Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-24T19:41:53.712Z Has data issue: false hasContentIssue false
  • English
  • Français

Constraint answer set solver EZCSP and why integration schemas matter

Published online by Cambridge University Press:  29 June 2017

MARCELLO BALDUCCINI  and
YULIYA LIERLER
MARCELLO BALDUCCINI
Affiliation:
Department of Decision & System Sciences, Saint Joseph's University, Philadelphia, PA, USA (e-mail: [email protected])
YULIYA LIERLER
Affiliation:
Computer Science Department, University of Nebraska at Omaha, Omaha, NE, USA (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

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 Nieuwenhuis et al. in 2006 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.

Keywords

Constraint Answer Set ProgrammingKnowledge RepresentationNonmonotonic Reasoning
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 17 , Issue 4 , July 2017 , pp. 462 - 515
Copyright
Copyright © Cambridge University Press 2017 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Anger, C., Gebser, M., Janhunen, T. and Schaub, T. 2006. What's a head without a body? In Proc. of the European Conference on Artificial Intelligence (ECAI'06), 769–770.Google Scholar
Balduccini, M. 2009. Representing constraint satisfaction problems in answer set programming. In Proc. of ICLP09 Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP09).Google Scholar
Balduccini, M. 2011. Industrial-size scheduling with ASP+CP. In Proc. of 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR11), Delgrande, J. P. and Faber, W., Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 6645. Springer Verlag, Berlin, 284–296.Google Scholar
Balduccini, M. and Lierler, Y. 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), Russo, C. and Zhou, N.-F., Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 7149. Springer Verlag, Berlin, 78–92.Google Scholar
Bartholomew, M. and Lee, J. 2014. System aspmt2smt: Computing ASPMT theories by SMT solvers. In Proc. of European Conference on Logics in Artificial Intelligence, JELIA, Springer, 529–542.Google Scholar
Brewka, G., Eiter, T. and Truszczyński, M. 2011. Answer set programming at a glance. Communications of the ACM 54 (12), 92–103.CrossRefGoogle Scholar
Calimeri, F., Cozza, S. and Ianni, G. 2007. External sources of knowledge and value invention in logic programming. Annals of Mathematics and Artificial Intelligence 50, 3–4, 333–361.Google Scholar
Calimeri, F., Cozza, S., Ianni, G. and Leone, N. 2008. Computable functions in ASP: theory and implementation. In Proc. of International Conference on Logic Programming (ICLP), 407–424.Google Scholar
Calimeri, F., Ianni, G., Ricca, F., Alviano, M., Bria, A., Catalano, G., Cozza, S., Faber, W., Febbraro, O., Leone, N., Manna, M., Martello, A., Panetta, C., Perri, S., Reale, K., Santoro, M. C., Sirianni, M., Terracina, G. and Veltri, P. 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.Google Scholar
Carlsson, M. and Mildner, P. 2012. SICStus Prolog-the first 25 years. Theory and Practice of Logic Programming 12, 1–2 (Jan.), 35–66.Google Scholar
Cat, B. D., Bogaerts, B. and Denecker, M. 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/ Google Scholar
Davis, M., Logemann, G. and Loveland, D. 1962. A machine program for theorem proving. Communications of the ACM 5 (7), 394–397.Google Scholar
De Moura, L. and Bjørner, N. 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.Google Scholar
Denecker, M., Vennekens, J., Bond, S., Gebser, M. and Truszczyński, M. 2009. The second answer set programming system competition. In Proc. of the International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Erdem, E., Lin, F., and Schaub, T., Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 5753. Springer, Berlin Heidelberg.CrossRefGoogle Scholar
Dovier, A., Formisano, A. and Pontelli, E. 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.Google Scholar
Drescher, C. and Walsh, T. 2011. A translational approach to constraint answer set solving. Theory and Practice of Logic Programming (TPLP) 10, 4–6, 465–480.CrossRefGoogle Scholar
Eén, N. and Biere, A. 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.Google Scholar
Eén, N. and Sörensson, N. 2003. An extensible SAT-solver. In Proc. of the International Conference on Theory and Applications of Satisfiability Testing. Springer, Berlin Heidelberg, 502–518.Google Scholar
Eiter, T., Ianni, G., Schindlauer, R. and Tompits, H. 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.Google Scholar
Elkabani, I., Pontelli, E. and Son, T. 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, Demoen, B. and Lifschitz, V., Eds. Lecture Notes in Computer Science, vol. 3132. Springer, 73–89.Google Scholar
Ferraris, P. and Lifschitz, V. 2005. Weight constraints as nested expressions. Theory and Practice of Logic Programming 5, 45–74.CrossRefGoogle Scholar
Gebser, M., Kaufmann, B., Neumann, A. and Schaub, T. 2007. Conflict-driven answer set solving. In Proc. 20th International Joint Conference on Artificial Intelligence (IJCAI'07), MIT Press, 386–392.Google Scholar
Gebser, M., Liu, L., Namasivayam, G., Neumann, A., Schaub, T. and Truszczyński, M. 2007. The first answer set programming system competition. In Proc. the International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Baral, C., Brewka, G., and Schlipf, J., Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 4483. Springer, Berlin Heidelberg, 3–17.Google Scholar
Gebser, M., Ostrowski, M. and Schaub, T. 2009. Constraint answer set solving. In Proc. of 25th International Conference on Logic Programming (ICLP), Hill, P. M. and Warren, D. S., Eds. Lecture Notes in Artificial Intelligence (LNCS), vol. 5649. Springer, Berlin Heidelberg, 235–249.Google Scholar
Gebser, M., Schaub, T. and Thiele, S. 2007. Gringo: A new grounder for answer set programming. In Logic Programming and Nonmonotonic Reasoning, Baral, C., Brewka, G., and Schlipf, J., Eds. Lecture Notes in Computer Science, vol. 4483. Springer, Berlin Heidelberg, 266–271.Google Scholar
Gelfond, M. and Lifschitz, V. 1998. Action languages 11 . Electronic Transactions on Artificial Intelligence 3, 195–210.Google Scholar
Giunchiglia, E., Leone, N. and Maratea, M. 2008. On the relation among answer set solvers. Annals of Mathematics and Artificial Intelligence 53, 1–4, 169–204.CrossRefGoogle Scholar
Giunchiglia, E., Lierler, Y. and Maratea, M. 2006. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning 36, 345–377.CrossRefGoogle Scholar
Gomes, C. P., Kautz, H., Sabharwal, A. and Selman, B. 2008. Satisfiability solvers. In Handbook of Knowledge Representation, van Harmelen, F., Lifschitz, V., and Porter, B., Eds. Elsevier, 89–134.Google Scholar
Jaffar, J. and Maher, M. J. 1994. Constraint logic programming: A survey. The Journal of Logic Programming 1920, Supplement 1, 503–581. Special Issue: Ten Years of Logic Programming.Google Scholar
Janhunen, T., Liu, G. and Niemel, I. 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.Google Scholar
Lee, J. 2005. A model-theoretic counterpart of loop formulas. In Proc. International Joint Conference on Artificial Intelligence (IJCAI). Professional Book Center, 503–508.Google Scholar
Lierler, Y. 2014. Relating constraint answer set programming languages and algorithms. Artificial Intelligence 207C, 1–22.CrossRefGoogle Scholar
Lierler, Y., Smith, S., Truszczyński, M. and Westlund, A. 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), Russo, C. V. and Zhou, N.-F., Eds. Lecture Notes in Computer Science, vol. 7149. Springer Verlag, Berlin.CrossRefGoogle Scholar
Lierler, Y. and Truszczyński, M. 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 Issue 11, 4–5, 629–646.Google Scholar
Lifschitz, V., Tang, L. R. and Turner, H. 1999. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence 25, 369–389.CrossRefGoogle Scholar
Liu, G., Janhunen, T. 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.Google Scholar
Marek, V. and Truszczyński, M. 1999. Stable models and an alternative logic programming paradigm. In The Logic Programming Paradigm: a 25-Year Perspective. Springer Verlag, 375–398.Google Scholar
Marriott, K., Nethercote, N., Rafeh, R., Stuckey, P. J., Garcia, De La Banda, M. and Wallace, M. 2008. The design of the Zinc modelling language. Constraints 13, 3 (September), 229–267.Google Scholar
Mellarkod, V. S., Gelfond, M. and Zhang, Y. 2008. Integrating answer set programming and constraint logic programming. Annals of Mathematics and Artificial Intelligence 53, 1–4, 251–287.CrossRefGoogle Scholar
Niemelä, I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241–273.Google Scholar
Niemelä, I. and Simons, P. 2000. Extending the Smodels system with cardinality and weight constraints. In Logic-Based Artificial Intelligence, Minker, J., Ed. Kluwer, 491–521.Google Scholar
Nieuwenhuis, R., Oliveras, A. and Tinelli, C. 2006. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53 (6), 937–977.CrossRefGoogle Scholar
Rossi, F., van Beek, P. and Walsh, T. 2008. Constraint programming. In Handbook of Knowledge Representation, van Harmelen, F., Lifschitz, V., and Porter, B., Eds. Elsevier, 181–212.CrossRefGoogle Scholar
Schulte, C. and Stuckey, P. J. 2008. Efficient constraint propagation engines. Transactions on Programming Languages and Systems 31 (1), 2:1–2:43.CrossRefGoogle Scholar
Simons, P., Niemelä, I. and Soininen, T. 2002. Extending and implementing the stable model semantics. Artificial Intelligence 138, 181–234.CrossRefGoogle Scholar
Susman, B. and Lierler, Y. 2016. SMT-based constraint answer set solver EZSMT (system description). In International Conference on Logic Programming (ICLP).Google Scholar
Van Gelder, A., Ross, K. and Schlipf, J. 1991. The well-founded semantics for general logic programs. Journal of ACM 38, 3, 620–650.Google Scholar
Wittocx, J., Mariën, M. and Denecker, M. 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].Google Scholar
Zhang, L., Madigan, C. F., Moskewicz, M. W. and Malik, S. 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.Google Scholar
Zhou, N.-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.Google Scholar