Enfragmo
Team
- Amir Aavani (Simon Fraser University)
- Shahab Tasharrofi (Simon Fraser University)
- Alireza Ensan (Simon Fraser University)
- Rui Ge (Simon Fraser University)
- Eugenia Ternoska (Simon Fraser University)
- David Mitchell (Simon Fraser University)
Description
Enfragmo is a grounding-based solver. The problem specification language is multi-sorted first order logic extended with arithmetic and aggregate operators. Given a problem specification and a problem instance, it produces a propositional CNF formula representing the solutions to the instance, and passes this to a SAT solver. The SAT solver choice is a command-line parameter, which can be set to compiled-in versions of MiniSAT or MXG, or any external solver.
System Settings
Internal version of Enfragmo: 4432
Command-line parameters and their default values:
--GoGroundingUsingQuery False
--DoGroundingUsingEnumeration True
--CountMode DC
- --CNFGateFlattening 1
- --CNFTseitinMemorization 1
- --UseInteractiveUP 1
--GroundingMode TFGrounder
--MinOrMaxMode DC
--GroundSolverType InternalMiniSAT
The following are the settings of parameters for each domain where default settings were not used.
Stable-Marriage
--DoGroundingUsingQuery True
--GroundSolverCommand "../Solver-Dir/glucose"
GracefulGraphs
--GroundSolverCommand "../Solver-Dir/glucose"
Weighted-Sequence/Run.sh
--GroundSolverCommand "../Solver-Dir/glucose"
Bottle-Filling
--DoGroundingUsingEnumeration False
--CountMode CARD
--GroundSolverType InternalMXC
Permutation-Pattern-Matching
--GroundSolverCommand "../Solver-Dir/glucose"
References
System URL: http://www.cs.sfu.ca/research/groups/mxp/
Participant URL.
Aavani A. et al. Enfragmo: A System for Modelling and Solving Search Problems with Logic, Proc., 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'12), Springer LNCS 7180.