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)
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-WeightedSequenceProblem: cpsupport, groundwithbounds off, liftedunitpropagation off
O15-StableMarriage: xsb, cpsupport
O16-IncrementalScheduling: symmetrybreaking, xsb, cpsupport