org.sat4j.minisat.core
Interface ICDCL<D extends DataStructureFactory>

Type Parameters:
D -
All Superinterfaces:
IProblem, ISolver, Learner, Serializable, UnitPropagationListener
All Known Implementing Classes:
Solver

public interface ICDCL<D extends DataStructureFactory>
extends ISolver, UnitPropagationListener, Learner

Abstraction for Conflict Driven Clause Learning Solver. Allows to easily access the various options available to setup the solver.

Author:
daniel

Method Summary
 void claBumpActivity(Constr confl)
           
 ICDCLLogger getLogger()
           
 IOrder getOrder()
           
 RestartStrategy getRestartStrategy()
           
 ISimplifier getSimplifier()
           
 void setDataStructureFactory(D dsf)
          Change the internal representation of the constraints.
 void setLearnedConstraintsDeletionStrategy(ConflictTimer timer, LearnedConstraintsEvaluationType evaluation)
           
 void setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy lcds)
           
 void setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType evaluation)
           
 void setLearner(LearningStrategy<D> learner)
           
 void setLogger(ICDCLLogger out)
           
 void setNeedToReduceDB(boolean needToReduceDB)
           
 void setOrder(IOrder h)
           
 void setRestartStrategy(RestartStrategy restarter)
           
 void setSearchParams(SearchParams sp)
           
 void setSimplifier(ISimplifier simp)
          Setup the reason simplification strategy.
 void setSimplifier(SimplificationType simp)
          Setup the reason simplification strategy.
 
Methods inherited from interface org.sat4j.specs.ISolver
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addExactly, clearLearntClauses, expireTimeout, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, unsatExplanation
 
Methods inherited from interface org.sat4j.specs.IProblem
findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos
 
Methods inherited from interface org.sat4j.minisat.core.UnitPropagationListener
enqueue, enqueue, unset
 
Methods inherited from interface org.sat4j.minisat.core.VarActivityListener
varBumpActivity
 
Methods inherited from interface org.sat4j.minisat.core.Learner
learn
 

Method Detail

setDataStructureFactory

void setDataStructureFactory(D dsf)
Change the internal representation of the constraints. Note that the heuristics must be changed prior to calling that method.

Parameters:
dsf - the internal factory

setLearner

void setLearner(LearningStrategy<D> learner)
Since:
2.2

setSearchParams

void setSearchParams(SearchParams sp)

setRestartStrategy

void setRestartStrategy(RestartStrategy restarter)

getRestartStrategy

RestartStrategy getRestartStrategy()

setSimplifier

void setSimplifier(SimplificationType simp)
Setup the reason simplification strategy. By default, there is no reason simplification. NOTE THAT REASON SIMPLIFICATION DOES NOT WORK WITH SPECIFIC DATA STRUCTURE FOR HANDLING BOTH BINARY AND TERNARY CLAUSES.

Parameters:
simp - a simplification type.

setSimplifier

void setSimplifier(ISimplifier simp)
Setup the reason simplification strategy. By default, there is no reason simplification. NOTE THAT REASON SIMPLIFICATION IS ONLY ALLOWED FOR WL CLAUSAL data structures. USING REASON SIMPLIFICATION ON CB CLAUSES, CARDINALITY CONSTRAINTS OR PB CONSTRAINTS MIGHT RESULT IN INCORRECT RESULTS.

Parameters:
simp -

getSimplifier

ISimplifier getSimplifier()

setLearnedConstraintsDeletionStrategy

void setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy lcds)
Parameters:
lcds -
Since:
2.1

setLearnedConstraintsDeletionStrategy

void setLearnedConstraintsDeletionStrategy(ConflictTimer timer,
                                           LearnedConstraintsEvaluationType evaluation)
Parameters:
timer - when to apply constraints cleanup.
evaluation - the strategy used to evaluate learned clauses.
Since:
2.3.2

setLearnedConstraintsDeletionStrategy

void setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType evaluation)
Parameters:
evaluation - the strategy used to evaluate learned clauses.
Since:
2.3.2

getOrder

IOrder getOrder()

setOrder

void setOrder(IOrder h)

setNeedToReduceDB

void setNeedToReduceDB(boolean needToReduceDB)

setLogger

void setLogger(ICDCLLogger out)

getLogger

ICDCLLogger getLogger()

claBumpActivity

void claBumpActivity(Constr confl)
Parameters:
outclause -


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.