org.sat4j.pb.core

Class PBSolverClause

java.lang.Object

org.sat4j.minisat.core.Solver<PBDataStructureFactory>

org.sat4j.pb.core.PBSolver

org.sat4j.pb.core.PBSolverCP

org.sat4j.pb.core.PBSolverClause

All Implemented Interfaces:

Serializable, ICDCL<PBDataStructureFactory>, Learner, IPBCDCLSolver<PBDataStructureFactory>, IPBSolver, IPBSolverService, IProblem, ISolver, ISolverService, RandomAccessModel, UnitPropagationListener

public class PBSolverClause
extends PBSolverCP

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.pb.core.PBSolver

objectiveFunctionBased, stats

Fields inherited from class org.sat4j.minisat.core.Solver

constrs, dsfactory, EXPENSIVE_SIMPLIFICATION, EXPENSIVE_SIMPLIFICATION_WLONLY, glucose, learnedConstraintsDeletionStrategy, learnts, memory_based, NO_SIMPLIFICATION, out, rootLevel, sharedConflict, SIMPLE_SIMPLIFICATION, slistener, trail, trailLim, undertimeout, voc

Constructor Summary

Constructors

Constructor and Description
PBSolverClause(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

Method Summary

Methods

Modifier and Type	Method and Description
void	claBumpActivity(Constr arg0)
String	toString(String prefix)

Methods inherited from class org.sat4j.pb.core.PBSolverCP

analyze, analyzeCP, updateNumberOfReducedLearnedConstraints, updateNumberOfReductions

Methods inherited from class org.sat4j.pb.core.PBSolver

addAtLeast, addAtLeast, addAtMost, addAtMost, addAtMostOnTheFly, addAtMostOnTheFly, addExactly, addExactly, addPseudoBoolean, getObjectiveFunction, setObjectiveFunction

Methods inherited from class org.sat4j.minisat.core.Solver

addAllClauses, addAtLeast, addAtMost, addAtMostOnTheFly, addBlockingClause, addClause, addClauseOnTheFly, addConstr, addExactly, analyzeAtRootLevel, analyzeFinalConflictInTermsOfAssumptions, assume, backtrack, cancelUntil, claBumpActivity, clearLearntClauses, currentDecisionLevel, decayActivities, decisionLevel, dimacs2internal, enqueue, enqueue, expireTimeout, findModel, findModel, fixedSize, fromLastDecisionLevel, getDSFactory, getIthConstr, getLearnedConstraints, getLiteralsPropagatedAt, getLogger, getLogPrefix, getOrder, getOutLearnt, getRestartStrategy, getSearchListener, getSearchParams, getSimplifier, getSolvingEngine, getStat, getStats, getTimeout, getTimeoutMs, getVariableHeuristics, getVocabulary, initStats, isDBSimplificationAllowed, isNeedToReduceDB, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, learn, model, model, modelWithInternalVariables, nAssigns, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printInfos, printLearntClausesInfos, printStat, printStat, printStat, propagate, realNumberOfVariables, reduceDB, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDataStructureFactory, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLearningStrategy, setLogger, setLogPrefix, setNeedToReduceDB, setOrder, setRestartStrategy, setSearchListener, setSearchParams, setSimplifier, setSimplifier, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setUnitClauseProvider, setVerbose, simplifyDB, sortOnActivity, stop, suggestNextLiteralToBranchOn, toString, truthValue, undoOne, unsatExplanation, unset, varBumpActivity

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.sat4j.minisat.core.ICDCL

getLogger, getOrder, getRestartStrategy, getSearchParams, getSimplifier, getStats, setDataStructureFactory, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, setLearningStrategy, 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, 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, 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

Methods inherited from interface org.sat4j.specs.ISolverService

addAtMostOnTheFly, addClauseOnTheFly, backtrack, currentDecisionLevel, getLearnedConstraints, getLiteralsPropagatedAt, getLogPrefix, getVariableHeuristics, nVars, removeSubsumedConstr, stop, suggestNextLiteralToBranchOn, truthValue

Constructor Detail

PBSolverClause

public PBSolverClause(LearningStrategy<PBDataStructureFactory> learner,
              PBDataStructureFactory dsf,
              IOrder order)

Method Detail

toString

public String toString(String prefix)

Specified by:

toString in interface ISolver

Overrides:

toString in class PBSolverCP

claBumpActivity

public void claBumpActivity(Constr arg0)