welcome: please sign in
location: Diff for "Participants\Enfragmo"
Differences between revisions 1 and 4 (spanning 3 versions)
⇤ ← Revision 1 as of 2013-05-23 22:31:57 →
Size: 78
Editor: FrancescoCalimeri
Comment:
← Revision 4 as of 2013-05-28 21:28:26 → ⇥
Size: 2419
Editor: FrancescoCalimeri
Comment:
Deletions are marked like this. Additions are marked like this.
Line 3: Line 3:
== TO APPEAR == = 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 [[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.

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:

The following are the settings of parameters for each domain where default settings were not used.

Stable-Marriage

GracefulGraphs

Weighted-Sequence/Run.sh

Bottle-Filling

Permutation-Pattern-Matching

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.

ASP Competition 2013: Participants\Enfragmo (last edited 2013-05-31 13:32:12 by FrancescoCalimeri)