#acl EditorsGroup:read,write,delete,revert,admin All:read
= 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
 * N02-ValvesLocationProblem
 * 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

== References ==
 * Participant [[http://dtai.cs.kuleuven.be/krr/idp|URL]].
 * Wittocx J. et al. ''The idp system: a model expansion system for an extension of classical logic''. LaSh 2008.