DSF {org.sat4j.minisat.constraints.ClausalDataStructureCB, org.sat4j.minisat.constraints.ClausalDataStructureCBWL, org.sat4j.minisat.constraints.ClausalDataStructureWL, org.sat4j.minisat.constraints.MixedDataStructureDaniel, org.sat4j.minisat.constraints.MixedDataStructureWithBinary, org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary}[org.sat4j.minisat.constraints.MixedDataStructureDaniel]
LEARNING {org.sat4j.minisat.learning.ActiveLearning, org.sat4j.minisat.learning.FixedLengthLearning, org.sat4j.minisat.learning.LimitedLearning, org.sat4j.minisat.learning.MiniSATLearning, org.sat4j.minisat.learning.NoLearningButHeuristics, org.sat4j.minisat.learning.NoLearningNoHeuristics}[org.sat4j.minisat.learning.LimitedLearning]
activityPercent {0.5,0.75,0.9,0.95,1.0}[0.95]
maxLength {1,2,3,4,5}[3]
limit {0,5,10,20,40}[10]
ORDER {org.sat4j.minisat.orders.JWOrder,org.sat4j.minisat.orders.MyOrder, org.sat4j.minisat.orders.PureOrder, org.sat4j.minisat.orders.VarOrderHeap, org.sat4j.minisat.orders.VarOrderHeapObjective}[org.sat4j.minisat.orders.VarOrderHeap]  #  org.sat4j.minisat.orders.VarOrder 
period {0,10,20,30,40}[20]
SIMP {NO_SIMPLIFICATION, SIMPLE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION}[EXPENSIVE_SIMPLIFICATION]
varDecay {0.8,0.85,0.9,0.95,1.0}[0.95]
claDecay {0.999}[0.999]
conflictBoundIncFactor {1.1,1.3,1.5,1.7,2.0}[1.5]
initConflictBound {100,200,500,1000,5000,30000,100000}[100]

Conditionals:
activityPercent|LEARNING in {org.sat4j.minisat.learning.ActiveLearning}
maxLength|LEARNING in {org.sat4j.minisat.learning.FixedLengthLearning}
limit|LEARNING in {org.sat4j.minisat.learning.LimitedLearning}
period|ORDER in {org.sat4j.minisat.orders.PureOrder}
	
Forbidden:
{DSF=org.sat4j.minisat.constraints.MixedDataStructureWithBinary,SIMP=SIMPLE_SIMPLIFICATION}
{DSF=org.sat4j.minisat.constraints.MixedDataStructureWithBinary,SIMP=EXPENSIVE_SIMPLIFICATION}
{DSF=org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary,SIMP=SIMPLE_SIMPLIFICATION}
{DSF=org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary,SIMP=EXPENSIVE_SIMPLIFICATION}

{DSF=org.sat4j.minisat.constraints.ClausalDataStructureCB,SIMP=SIMPLE_SIMPLIFICATION}
{DSF=org.sat4j.minisat.constraints.ClausalDataStructureCB,SIMP=EXPENSIVE_SIMPLIFICATION}
{DSF=org.sat4j.minisat.constraints.ClausalDataStructureCBWL,SIMP=SIMPLE_SIMPLIFICATION}
{DSF=org.sat4j.minisat.constraints.ClausalDataStructureCBWL,SIMP=EXPENSIVE_SIMPLIFICATION}

{ORDER=org.sat4j.minisat.orders.JWOrder,DSF=org.sat4j.minisat.constraints.ClausalDataStructureCB}
{ORDER=org.sat4j.minisat.orders.JWOrder,DSF=org.sat4j.minisat.constraints.ClausalDataStructureCBWL}
{ORDER=org.sat4j.minisat.orders.JWOrder,DSF=org.sat4j.minisat.constraints.ClausalDataStructureWL}
{ORDER=org.sat4j.minisat.orders.JWOrder,DSF=org.sat4j.minisat.constraints.MixedDataStructureDaniel}
{ORDER=org.sat4j.minisat.orders.JWOrder,DSF=org.sat4j.minisat.constraints.MixedDataStructureWithBinary}
	
{ORDER=org.sat4j.minisat.orders.MyOrder,DSF=org.sat4j.minisat.constraints.MixedDataStructureDaniel}
{ORDER=org.sat4j.minisat.orders.MyOrder,DSF=org.sat4j.minisat.constraints.ClausalDataStructureCB}
{ORDER=org.sat4j.minisat.orders.MyOrder,DSF=org.sat4j.minisat.constraints.ClausalDataStructureWL}
{ORDER=org.sat4j.minisat.orders.MyOrder,DSF=org.sat4j.minisat.constraints.ClausalDataStructureCBWL}
{ORDER=org.sat4j.minisat.orders.MyOrder,DSF=org.sat4j.minisat.constraints.MixedDataStructureDaniel}