Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-18T20:07:56.520Z Has data issue: false hasContentIssue false
  • English
  • Français

Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches

Published online by Cambridge University Press:  02 November 2021

YULIYA LIERLER Open the ORCID record for YULIYA LIERLER [Opens in a new window]
YULIYA LIERLER*
Affiliation:
University of Nebraska Omaha, Omaha, NE 68182, USA (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning putting together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. CASP demonstrates promising results, including the development of a multitude of solvers: acsolver, clingcon, ezcsp, idp, inca, dingo, mingo, aspmt2smt, clingo[l,dl], and ezsmt. It opens new horizons for declarative programming applications such as solving complex train scheduling problems. Systems designed to find solutions to constraint answer set programs can be grouped according to their construction into, what we call, integrational or translational approaches. The focus of this paper is an overview of the key ingredients of the design of constraint answer set solvers drawing distinctions and parallels between integrational and translational approaches. The paper also provides a glimpse at the kind of programs its users develop by utilizing a CASP encoding of Traveling Salesman problem for illustration. In addition, we place the CASP technology on the map among its automated reasoning peers as well as discuss future possibilities for the development of CASP.

Keywords

answer set programmingconstraintssatisfiability modulo theories
Type
Survey Article
Information
Theory and Practice of Logic Programming , Volume 23 , Issue 1 , January 2023 , pp. 195 - 225
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

Footnotes

*

I would like to acknowledge and cordially thank many of my collaborators with whom we had a chance to contribute to an exciting field of Constraint Answer Set Programming and many of my colleagues who have fostered my understanding of the subject matter: Marcello Balduccini, Broes De Cat, Marc Denecker, Martin Gebser, Michael Gelfond, Tomi Janhunen, Roland Kaminski, Martin Nyx Brain, Joohyung Lee, Ilkka Niemelä, Max Ostrowski, Torsten Schaub, Peter Schueller, Da Shen, Benjamin Susman, Cesare Tinelli, Miroslaw Truszczynski, Philipp Wanko, Yuanlin Zhang. Thank you for the years of an incredible journey. Also, I would like to thank the anonymous reviewers for their valuable feedback, which helped to bring the article to this form. This work was partially supported by the NSF 1707371 grant.

References

Abels, D., Jordi, J., Ostrowski, M., Schaub, T., Toletti, A. and Wanko, P. 2019. Train scheduling with hybrid ASP. In Logic Programming and Nonmonotonic Reasoning - 15th International Conference, LPNMR 2019, Philadelphia, PA, USA, 3–7 June 2019, Proceedings, Balduccini, M., Lierler, Y. and Woltran, S., Eds. Lecture Notes in Computer Science, vol. 11481. Springer, 3–17.Google Scholar
Andres, B., Kaufmann, B., Matheis, O. and Schaub, T. 2012. Unsatisfiability-based optimization in clasp. In Technical Communications of the 28th International Conference on Logic Programming (ICLP’12), Dovier, A. and Costa, V. S., Eds. Leibniz International Proceedings in Informatics (LIPIcs), vol. 17. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 211–221.Google Scholar
Balduccini, M. 2011. Industrial-size scheduling with ASP+cp. In Logic Programming and Nonmonotonic Reasoning - 11th International Conference (LPNMR). Lecture Notes in Computer Science, vol. 6645. Springer-Verlag, 284–296.Google Scholar
Balduccini, M. 2013. ASP with non-herbrand partial functions: a language and system for practical use. Theory and Practice of Logic Programming 13, 547–561.CrossRefGoogle Scholar
Balduccini, M. and Gelfond, M. 2005. Model-based reasoning for complex flight systems. In Proceedings of Infotech@Aerospace (American Institute of Aeronautics and Astronautics).Google Scholar
Balduccini, M., Gelfond, M., Nogueira, M., Watson, R. and Barry, M. 2001. An A-Prolog decision support system for the Space Shuttle. In Working Notes of the AAAI Spring Symposium on Answer Set Programming.Google Scholar
Balduccini, M. and Lierler, Y. 2017. Constraint answer set solver EZCSP and why integration schemas matter. Theory and Practice of Logic Programming 17, 4, 462–515.CrossRefGoogle Scholar
Balduccini, M., Magazzeni, D., Maratea, M. and Leblanc, E. C. 2017. CASP solutions for planning in hybrid domains. Theory and Practice of Logic Programming 17, 4, 591–633.CrossRefGoogle Scholar
Banbara, M., Gebser, M., Inoue, K., Ostrowski, M., Peano, A., Schaub, T., Soh, T., Tamura, N. and Weise, M. 2015. aspartame: solving constraint satisfaction problems with answer set programming. In Logic Programming and Nonmonotonic Reasoning, Calimeri, F., Ianni, G. and Truszczynski, M., Eds. Springer International Publishing, Cham, 112–126.Google Scholar
Banbara, M., Kaufmann, B., Ostrowski, M. and Schaub, T. 2017. Clingcon: the next generation. Theory and Practice of Logic Programming (TPLP) 17, 4, 408–461.CrossRefGoogle Scholar
Barrett, C., Conway, C. L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A. and Tinelli, C. 2011. Cvc4. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11). LNCS, vol. 6806. Springer.CrossRefGoogle Scholar
Barrett, C., Fontaine, P. and Tinelli, C. 2015. The SMT-LIB Standard: version 2.5. Tech. rep., Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org.Google Scholar
Barrett, C., Sebastiani, R., Seshia, S. A. and Tinelli, C. 2008. Satisfiability modulo theories. In Handbook of Satisfiability, Biere, A., Heule, M., van Maaren, H. and Walsch, T., Eds. IOS Press, 737–797.Google Scholar
Barrett, C. and Tinelli, C. 2014. Satisfiability modulo theories. In Handbook of Model Checking, Clarke, E., Henzinger, T. and Veith, H., Eds. Springer.Google Scholar
Bartholomew, M. 2016. Answer Set Programming Modulo Theories. Ph.D. thesis, Arizona State University.Google Scholar
Bartholomew, M. and Lee, J. 2013. Functional stable model semantics and answer set programming modulo theories. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI). 718––724.Google Scholar
Bartholomew, M. and Lee, J. 2014. System aspmt2smt: computing ASPMT theories by SMT solvers. In Logics in Artificial Intelligence: 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, 24–26 September 2014. Proceedings. Springer International Publishing, Cham, 529–542.Google Scholar
Biavaschi, S. 2017. Automated reasoning methods in hybrid systems. Annual Report of “Scuola Superiore dell’Università di Udine”.Google Scholar
Biere, A., Cimatti, A., Clarke, E. M., Strichman, O. and Zhu, Y. 2003. Bounded model checking. Advances in Computers 58, 117–148.CrossRefGoogle Scholar
Bomanson, J., Gebser, M., Janhunen, T., Kaufmann, B. and Schaub, T. 2016. Answer set programming modulo acyclicity. Fundamenta Informaticae 147, 63–91.CrossRefGoogle Scholar
Bomanson, J., Janhunen, T. and Niemelä, I. 2020. Applying visible strong equivalence in answer-set program transformations. Transactions on Computational Logic 21, 4, 33:1–33:41.Google Scholar
Brain, M., Erdem, E., Inoue, K., Oetsch, J., Puehrer, J., Tompits, H. and Yilmaz, C. 2012. Event-sequence testing using answer-set programming. International Journal on Advances in Software 5, 3&4.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
Bromberger, M., Sturm, T. and Weidenbach, C. 2015. Linear integer arithmetic revisited. In Automated Deduction - CADE-25, Felty, A. P. and Middeldorp, A., Eds. Springer International Publishing, Cham, 623–637.Google Scholar
Cabalar, P., Fandinno, J. and Lierler, Y. 2020. Modular answer set programming as a formal specification language. Theory and Practice of Logic Programming 20, 5, 767–782.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.CrossRefGoogle Scholar
Calimeri, F., Cozza, S., Ianni, G. and Leone, N. 2008. Computable functions in ASP: theory and implementation. In Proceedings of International Conference on Logic Programming (ICLP), 407–424.Google Scholar
Calimeri, F., Faber, W., Gebser, M., Ianni, G., Kaminski, R., Krennwallner, T., Leone, N., Maratea, M., Ricca, F. and Schaub, T. 2019. ASP-core-2 input language format. Theory and Practice of Logic Programming 20, 2, 294–309.CrossRefGoogle Scholar
Calimeri, F., Gebser, M., Maratea, M. and Ricca, F. 2016. Design and results of the fifth answer set programming competition. Artificial Intelligence 231, 151–181.CrossRefGoogle 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 Proceedings of the International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). Springer-Verlag, Berlin, Heidelberg, 388–403.Google Scholar
Carlsson, M. and Fruehwirth, T. 2014. SICStus PROLOG User’s Manual 4.3. Books On Demand - Proquest.Google Scholar
Clark, K. 1978. Negation as failure. In Logic and Data Bases, Gallaire, H. and Minker, J., Eds. Plenum Press, New York, 293–322.Google Scholar
Cohen, M. B., Dwyer, M. B. and Shi, J. 2008. Constructing interaction test suites for highly-configurable systems in the presence of constraints: a greedy approach. IEEE Transactions on Software Engineering 34, 5, 633–650.CrossRefGoogle Scholar
De Moura, L. and Bjørner, N. 2008. Z3: an efficient SMT solver. In Proceedings 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., Lierler, Y., Truszczynski, M. and Vennekens, J. 2019. The informal semantics of answer set programming: a Tarskian perspective. arXiv:1901.09125.Google Scholar
Dovier, A., Formisano, A. and Pontelli, E. 2009. An empirical study of constraint logic programming and answer set programming solutions of combinatorial problems. Journal of Experimental & Theoretical Artificial Intelligence 21, 2, 79–121.CrossRefGoogle Scholar
Drescher, C. and Walsh, T. 2010. A translational approach to constraint answer set solving. Theory and Practice of Logic Programming (TPLP) 10, 4–6, 465–480.CrossRefGoogle Scholar
Drescher, C. and Walsh, T. 2011. Translation-based constraint answer set solving. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI). AAAI Press, 2596–2601.Google Scholar
Dutertre, B. 2017. yices. URL: http://yices.csl.sri.com/. [Accessed: 2018].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 Proceedings of 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 ICLP, Demoen, B. and Lifschitz, V., Eds. Lecture Notes in Computer Science, vol. 3132. Springer-Verlag, 73–89.Google Scholar
Erdoğan, S. and Lifschitz, V. 2004. Definitions in answer set programming. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 114–126.CrossRefGoogle Scholar
Fages, F. 1994. Consistency of Clark’s completion and existence of stable models. Journal of Methods of Logic in Computer Science 1, 51–60.Google Scholar
Fandinno, J., Lifschitz, V., Lühne, P. and Schaub, T. 2020. Verifying tight logic programs with Anthem and Vampire. Theory and Practice of Logic Programming 20, 5, 735–750.CrossRefGoogle Scholar
Ferraris, P. and Lifschitz, V. 2005. Weight constraints as nested expressions. Theory and Practice of Logic Programming 5, 45–74.CrossRefGoogle Scholar
Garvin, B. J., Cohen, M. B. and Dwyer, M. B. 2011. Evaluating improvements to a meta-heuristic search for constrained interaction testing. Empirical Software Engineering 16, 1, 61–102.CrossRefGoogle Scholar
Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T. and Wanko, P. 2016. Theory solving made easy with Clingo 5. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016), Carro, M., King, A., Saeedloei, N. and Vos, M. D., Eds. OpenAccess Series in Informatics (OASIcs), vol. 52. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2:1–2:15.Google Scholar
Gebser, M., Kaminski, R., Kaufmann, B. and Schaub, T. 2009. On the Implementation of Weight Constraint Rules in Conflict-Driven ASP Solvers. Springer, Berlin, Heidelberg, 250–264.CrossRefGoogle Scholar
Gebser, M., Kaminski, R., König, A. and Schaub, T. 2011. Advances in gringo series 3. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). Springer, 345–351.Google Scholar
Gebser, M., Kaufmann, B., Neumann, A. and Schaub, T. 2007. Conflict-driven answer set enumeration. In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning. LPNMR’07. Springer-Verlag, Berlin, Heidelberg, 136–148.Google Scholar
Gebser, M., König, A., Schaub, T., Thiele, S. and Veber, P. 2010. The bioASP library: ASP solutions for systems biology. In 22nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2010. IEEE Computer Society, 383–389.Google Scholar
Gebser, M., Lee, J. and Lierler, Y. 2011. On elementary loops of logic programs. Theory and Practice of Logic Programming 11, 6, 953–988.CrossRefGoogle Scholar
Gebser, M., Ostrowski, M. and Schaub, T. 2009. Constraint answer set solving. In Proceedings of 25th International Conference on Logic Programming (ICLP). Springer-Verlag, 235–249.Google Scholar
Gebser, M., Schaub, T. and Thiele, S. 2007. Gringo: a new grounder for answer set programming. In Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning, 266–271.Google 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.CrossRefGoogle Scholar
Gutin, G. and Punnen, A., Eds. 2007. The Traveling Salesman Problem and Its Variations. Springer-Verlag.CrossRefGoogle Scholar
IBM 2009. IBM ILOG AMPL Version 12.1 User’s Guide. IBM. URL: http://www.ibm.com/software/commerce/optimization/cplex-optimizer/.Google Scholar
Jaffar, J. and Maher, M. 1994. Constraint logic programming: a survey. Journal of Logic Programming 19, 20, 503–581.CrossRefGoogle Scholar
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. DOI: 10.3166/jancl.16.35-86.CrossRefGoogle Scholar
Janhunen, T., Kaminski, R., Ostrowski, M., Schellhorn, S., Wanko, P. and Schaub, T. 2017. Clingo goes linear constraints over reals and integers. Theory and Practice of Logic Programming 17, 5–6, 872–888.CrossRefGoogle 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
Janhunen, T., Niemelä, I. and Sevalnev, M. 2009. Computing stable models via reductions to difference logic. In Logic Programming and Nonmonotonic Reasoning. Springer, Berlin, Heidelberg, 142–154.Google Scholar
Kautz, H. and Selman, B. 1992. Planning as satisfiability. In Proceedings of European Conference on Artificial Intelligence (ECAI), 359–363.Google Scholar
Kowalski, R. A. 1974. Predicate logic as programming language. In Proceedings of International Federation of Information Processing Conference, J. L. Rosenfeld, Ed. North–Holland, Stockholm, Sweden, 569–574.Google Scholar
Kowalski, R. A. 1988. The early years of logic programming. Communications of the ACM 31, 1, 38–43.CrossRefGoogle Scholar
Lawler, E. L., Lenstra, J. K., Kan, A. H. G. R. and Shmoys, D. B., Eds. 1985. The Traveling Salesman Problem: A Guided Tour of Combinatorial Optimization. Wiley.Google Scholar
Lee, J. and Meng, Y. 2013. Answer set programming modulo theories and reasoning about continuous changes. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), Beijing, China, 3–9 August 2013.Google Scholar
Lierler, Y. 2010. SAT-based Answer Set Programming. Ph.D. thesis, University of Texas at Austin.Google Scholar
Lierler, Y. 2014. Relating constraint answer set programming languages and algorithms. Artificial Intelligence 207C, 1–22.Google Scholar
Lierler, Y. 2017. What is answer set programming to propositional satisfiability. Constraints 22, 307–337.CrossRefGoogle Scholar
Lierler, Y., Smith, S., Truszczyński, M. and Westlund, A. 2012. Weighted-sequence problem: ASP vs cASP and declarative vs problem oriented solving. In Proceedings of the 14th International Symposium on Practical Aspects of Declarative Languages, PADL 2012, Russo, C. V. and Zhou, N.-F., Eds. Lecture Notes in Computer Science, vol. 7149. Springer-Verlag, 63–77.Google Scholar
Lierler, Y. and Susman, B. 2017. On relation between constraint answer set programming and satisfiability modulo theories. Theory and Practice of Logic Programming 17, 4, 559–590.CrossRefGoogle Scholar
Lierler, Y. and Truszczyński, M. 2011. Transition systems for model generators — a unifying approach. In Theory and Practice of Logic Programming, 27th Int’l. Conference on Logic Programming (ICLP) Special Issue 11, 4–5, 629–646.Google Scholar
Lifschitz, V. 2002. Answer set programming and plan generation. Artificial Intelligence 138, 39–54.CrossRefGoogle Scholar
Lifschitz, V. 2017. Achievements in answer set programming. TPLP 17, 5–6, 961–973.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
Lin, F. and Wang, Y. 2008. Answer set programming with functions. In Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), 454–465.Google 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
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
Nethercote, N., Stuckey, P., Becket, R., Brand, S., Duck, G. and Tack, G. 2007. MiniZinc: towards a standard cp modelling language. In Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming, 529–543.Google Scholar
Niemelä, I. 1999. Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241–273.CrossRefGoogle Scholar
Niemelä, I. 2008. Stable models and difference logic. Annals of Mathematics and Artificial Intelligence 53, 313–329.CrossRefGoogle Scholar
Niemelä, I. and Simons, P. 2000. Extending the Smodels system with cardinality and weight constraints. In Logic-Based Artificial Intelligence, J. Minker, Ed. Kluwer, 491–521.Google Scholar
Nieuwenhuis, R. and Oliveras, A. 2005. DPLL(T) with exhaustive theory propagation and its application to difference logic. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05), vol. 3576. LNCS. Springer.CrossRefGoogle 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
Nudelman, E., Devkar, A., Shoham, Y., Leyton-Brown, K. and Hoos, H. 2004. SATzilla: an algorithm portfolio for SAT. In SAT Competition.Google Scholar
Ostrowski, M. 2018. Modern Constraint Answer Set Solving. Ph.D. thesis, University of Potsdam.Google Scholar
Palù, R. D., Dovier, A. and Fogolari, F. 2004. Constraint logic programming approach to protein structure prediction. BMC Bioinformatics 5, 2004.Google Scholar
Palu, A. D., Dovier, A. and Pontelli, E. 2010. Computing approximate solutions of the protein structure determination problem using global constraints on discrete crystal lattices. International Journal of Data Mining and Bioinformatics 4, 1, 1–20.CrossRefGoogle Scholar
Prasad, M. R., Biere, A. and Gupta, A. 2005. A survey of recent advances in SAT-based formal verification. STTT 7, 2, 156–173.CrossRefGoogle Scholar
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. Theory and Practice of Logic Programming 12, 3, 361–381.CrossRefGoogle Scholar
Rintanen, J. 2012. Planning as satisfiability: heuristics. Artificial Intelligence 193, 45–86.CrossRefGoogle Scholar
Robinson, N., Gretton, C., Pham, D.-N. and Sattar, A. 2010. Cost-optimal planning using weighted MaxSAT. In ICAPS 2010 Workshop on Constraint Satisfaction Techniques for Planning and Scheduling (COPLAS10).Google Scholar
Rosis, A. F. D., Eiter, T., Redl, C. and Ricca, F. 2015. Constraint answer set programming based on hex-programs. In Eighth Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2015), Cork, Ireland.Google 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
Shen, D. and Lierler, Y. 2018a. SMT-based answer set solver CMODELS-DIFF (system description). In Proceedings of the 34th International Conference on Logic Programming (ICLP).Google Scholar
Shen, D. and Lierler, Y. 2018b. SMT-based constraint answer set solver EZSMT+ for non-tight programs. In Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR).Google Scholar
Susman, B. and Lierler, Y. 2016. SMT-based constraint answer set solver EZSMT (system description). In Proceedings of 32th International Conference on Logic Programming (ICLP). Dagstuhl Publishing, OpenAccess Series in Informatics (OASIcs).Google Scholar
Tinelli, C. and Barrett, C. 2015. AUFLIRA. http://smtlib.cs.uiowa.edu/logics-all.shtml#AUFLIRA. [Accessed: 2018].Google Scholar
Wielemaker, J., Schrijvers, T., Triska, M. and Lager, T. 2012. SWI-Prolog. Theory and Practice of Logic Programming 12, 1–2, 67–96.CrossRefGoogle Scholar
Wintersteiger, C. M., Bjørner, N. and de Moura, L. 2016. Z3. URL: https://github.com/Z3Prover/z3/releases/tag/z3-4.5.0. [Accessed: 2018].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.Google Scholar
Young, R., Balduccini, M. and Israney, A. 2017. CASP for robot control in hybrid domains. In Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP17).CrossRefGoogle Scholar
Zhou, N. 2012. The language features and architecture of B-Prolog. Theory and Practice of Logic Programming 12, 1–2, 189–218.CrossRefGoogle Scholar