Abstract
Given a finite domain, grounding is the the process of creating a variable-free first-order formula equivalent to a first-order sentence. As the first-order sentences can be used to describe a combinatorial search problem, efficient grounding algorithms would help in solving such problems effectively and makes advanced solver technology (such as SAT) accessible to a wider variety of users. One promising method for grounding is based on the relational algebra from the field of Database research. In this paper, we describe the extension of this method to ground formulas of first-order logic extended with arithmetic, expansion functions and aggregate operators. Our method allows choice of particular CNF representations for complex constraints, easily.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Frisch, A.M., Grum, M., Jefferson, C., Hernandez, B.M., Miguel, I.: The design of ESSENCE: a constraint language for specifying combinatorial problems. In: Proc. IJCAI 2007 (2007)
Mitchell, D., Ternovska, E.: A framework for representing and solving NP search problems. In: Proc. AAAI 2005 (2005)
Gent, I., Jefferson, C., Miguel, I.: Minion: A fast, scalable, constraint solver. In: ECAI 2006: 17th European Conference on Artificial Intelligence, Proceedings Including Prestigious Applications of Intelligent Systems (PAIS 2006), Riva del Garda, Italy, August 29-September 1, vol. 98, p. 98. Ios Pr. Inc., Amsterdam (2006)
Patterson, M., Liu, Y., Ternovska, E., Gupta, A.: Grounding for model expansion in k-guarded formulas with inductive definitions. In: Proc. IJCAI 2007, pp. 161–166 (2007)
Mohebali, R.: A method for solving NP search based on model expansion and grounding. Master’s thesis, Simon Fraser University (2006)
Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in constructive mathematics and mathematical logic 2(115-125), 10–13 (1968)
Lynce, I., Marques-Silva, J.: Efficient haplotype inference with boolean satisfiability. In: AAAI. AAAI Press, Menlo Park (2006)
Rendl, A.: Effective compilation of constraint models (2010)
Nethercote, N., Stuckey, P., Becket, R., Brand, S., Duck, G., Tack, G.: MiniZinc: Towards a standard CP modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007)
Wittocx, J., Mariën, M., De Pooter, S.: The idp system (2008), Obtainable via www.cs.kuleuven.be/dtai/krr/software.html
Wittocx, J.: Finite domain and symbolic inference methods for extensions of first-order logic. AI Communications (2010) (accepted)
AsÃn, R., Nieuwenhuis, R., Oliveras, A., RodrÃguez-Carbonell, E.: Cardinality Networks and Their Applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 167–180. Springer, Heidelberg (2009)
Eén, N.: SAT Based Model Checking. PhD thesis (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aavani, A., Wu, X.(., Ternovska, E., Mitchell, D. (2011). Grounding Formulas with Complex Terms. In: Butz, C., Lingras, P. (eds) Advances in Artificial Intelligence. Canadian AI 2011. Lecture Notes in Computer Science(), vol 6657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21043-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-21043-3_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21042-6
Online ISBN: 978-3-642-21043-3
eBook Packages: Computer ScienceComputer Science (R0)