#acl EditorsGroup:read,write,delete,revert,admin All:read = 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: * --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 [[http://www.cs.sfu.ca/research/groups/mxp/|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.