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 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:

• --SortMode RadixSort

• --GoGroundingUsingQuery False

• --UseDynamicVariableGenerator

• --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

• --GroundSolverType GenericDimacsCnf

• --GroundSolverCommand "../Solver-Dir/glucose"

GracefulGraphs

• --GroundSolverType GenericDimacsCnf

• --GroundSolverCommand "../Solver-Dir/glucose"

Weighted-Sequence/Run.sh

• --GroundSolverType GenericDimacsCnf

• --GroundSolverCommand "../Solver-Dir/glucose"

Bottle-Filling

• --DoGroundingUsingEnumeration False

• --CountMode CARD

• --GroundSolverType InternalMXC

Permutation-Pattern-Matching

• --GroundSolverType GenericDimacsCnf

• --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-18), Springer LNCS 7180.