Abstract
In this paper, we present the Enfragmo system for specifying and solving combinatorial search problems. It supports natural specification of problems by providing users with a rich language, based on an extension of first order logic. Enfragmo takes as input a problem specification and a problem instance and produces a propositional CNF formula representing solutions to the instance, which is sent to a SAT solver. Because the specification language is high level, Enfragmo provides combinatorial problem solving capability to users without expertise in use of SAT solvers or algorithms for solving combinatorial problems. Here, we describe the specification language and implementation of Enfragmo, and give experimental evidence that its performance is comparable to that of related systems. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Aavani, A., Wu, X., Tasharrofi, S., Ternovska, E., & Mitchell, D. (2012). Enfragmo: A system for modelling and solving search problems with logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7180 LNCS, pp. 15–22). https://doi.org/10.1007/978-3-642-28717-6_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
