IDP 3

Team

• Bart Bogaerts (KU Leuven)
• Maurice Bruynooghe (KU Leuven)
• Broes De Cat (KU Leuven)
• Marc Denecker (KU Leuven)
• Jo Devriendt (KU Leuven)
• Joachim Jansen (KU Leuven)
• Pieter Van Hertum (KU Leuven)
• Stef De Pooter (KU Leuven)

Description

IDP 3 uses FO(ID,Agg) + Lua as input language.

Model generation/optimization is achieved by lifted unit propagation + grounding with bounds (possibly using XSB for evaluating definitions) + applying the search algorithm MinisatID.

The integration with Lua (with logic components as first-class citizens) is used for pre- and postprocessing and to implement more complex inferences.

System Settings

System versions:

• IDP 3.1.4
• MinisatID 3.7.4
• XSB 3.3

We will refer to the following options:

• cpsupport = using finite domain variables and constraints during search
• lazy grounding = interleaving grounding and search.
• xsb = evaluation of definitions with only 2-valued open symbols before search, by applying the XSB Prolog system.
• symmetrybreaking = automated symmetry detection + addition of static symmetry breaking formulas to the theory.
• groundwithbounds = derive bounds on necessary variable instantations during grounding. by reasoning based on the input interpretation + improve the order of instantiation.
• liftedunitpropagation = apply approximative unit propagation on the non-ground theory.

By default, the first 4 are disabled and the last 2 are enabled. Only options not taking their default value are mentioned.

System Track: lazy grounding, xsb, cpsupport.

• FO(.)^IDP is used as input language.

Model-and-Solve Track:

• N01 Permutation Pattern Matching: cpsupport, groundwithbounds off, liftedunitpropagation off
• N02 Valves Location Problem: symmetrybreaking, cpsupport
• N04 Connected Density Maximum Still life: symmetrybreaking, cpsupport, xsb
• N05 Graceful Graphs: cpsupport
• N06 Bottle Filling
• N07 Nomystery: symmetrybreaking
• N08 Sokoban: xsb, symmetrybreaking
• N09 Ricochet Robots
• N12 Strategic Companies
• O10 Crossing Minimization: xsb, cpsupport
• O11 Reachability: liftedunitpropagation off, lazy grounding
• O13 Solitaire: cpsupport
• O14 Weighted Sequence Problem: cpsupport, groundwithbounds off, liftedunitpropagation off
• O15 Stable Marriage: xsb, cpsupport
• O16 Incremental Scheduling: symmetrybreaking, xsb, cpsupport

References

• Participant URL.

• Wittocx J., Marien M. and Denecker M., The idp system: a model expansion system for an extension of classical logic. LASH 2008.