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

Type Parameters:

D -

All Superinterfaces:

IProblem, ISolver, Learner, Serializable, UnitPropagationListener

All Known Subinterfaces:

IPBCDCLSolver<D>

All Known Implementing Classes:

PBSolver, PBSolverCautious, PBSolverClause, PBSolverCP, PBSolverResCP, PBSolverResolution, PBSolverWithImpliedClause, 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 -