org.sat4j.minisat.core

Interface ICDCL<D extends DataStructureFactory>

Type Parameters:

D -

All Superinterfaces:

IProblem, ISolver, Learner, RandomAccessModel, 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

Methods

Modifier and Type	Method and Description
void	claBumpActivity(Constr confl)
ILogAble	getLogger()
IOrder	getOrder()
RestartStrategy	getRestartStrategy()
SearchParams	getSearchParams()
ISimplifier	getSimplifier()
SolverStats	getStats()
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) Deprecated. renamed into setLearningStrategy()
void	setLearningStrategy(LearningStrategy<D> strategy) Allow to change the learning strategy, i.e. to decide which clauses/constraints should be learned by the solver after conflict analysis.
void	setLogger(ILogAble 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, getSolvingEngine, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSolverKeptHot, isVerbose, modelWithInternalVariables, newVar, nextFreeVarId, printStat, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, setVerbose, toString, unsatExplanation

Methods inherited from interface org.sat4j.specs.IProblem

findModel, findModel, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, nConstraints, newVar, nVars, primeImplicant, primeImplicant, printInfos, printInfos

Methods inherited from interface org.sat4j.specs.RandomAccessModel

model

Methods inherited from interface org.sat4j.specs.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

@Deprecated
void setLearner(LearningStrategy<D> learner)

Deprecated. renamed into setLearningStrategy()

Since:

2.2

See Also:

setLearningStrategy(LearningStrategy)

setLearningStrategy

void setLearningStrategy(LearningStrategy<D> strategy)

Allow to change the learning strategy, i.e. to decide which clauses/constraints should be learned by the solver after conflict analysis.

Since:

2.3.3

setSearchParams

void setSearchParams(SearchParams sp)

getSearchParams

SearchParams getSearchParams()

getStats

SolverStats getStats()

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(ILogAble out)

getLogger

ILogAble getLogger()

claBumpActivity

void claBumpActivity(Constr confl)

Parameters:

outclause -