org.sat4j.pb.core
Interface IPBCDCLSolver<D extends PBDataStructureFactory>

Type Parameters:
D -
All Superinterfaces:
ICDCL<D>, IPBSolver, IProblem, ISolver, Learner, Serializable, UnitPropagationListener
All Known Implementing Classes:
PBSolver, PBSolverCautious, PBSolverClause, PBSolverCP, PBSolverResCP, PBSolverResolution, PBSolverWithImpliedClause

public interface IPBCDCLSolver<D extends PBDataStructureFactory>
extends IPBSolver, ICDCL<D>

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

Author:
sroussel

Method Summary
 void claBumpActivity(Constr arg0)
           
 
Methods inherited from interface org.sat4j.pb.IPBSolver
addAtLeast, addAtLeast, addAtMost, addAtMost, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction
 
Methods inherited from interface org.sat4j.minisat.core.ICDCL
getLogger, getOrder, getRestartStrategy, getSimplifier, setDataStructureFactory, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLogger, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchParams, setSimplifier, setSimplifier
 
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

claBumpActivity

void claBumpActivity(Constr arg0)


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