Enfragmo: A System for Modelling and Solving Search Problems with Logic

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.

Authors

• Amir Aavani
• Xiongnan (Newman) Wu
• Shahab Tasharrofi
• Eugenia Ternovska
• David G. Mitchell

Keywords

No keywords are indexed for this paper.