org.sat4j.pb.core

Class PBSolverCP

java.lang.Object

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

org.sat4j.pb.core.PBSolver

org.sat4j.pb.core.PBSolverCP

All Implemented Interfaces:

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

Direct Known Subclasses:

PBSolverCautious, PBSolverClause, PBSolverResCP, PBSolverWithImpliedClause

public class PBSolverCP
extends PBSolver

Author:

parrain To change the template for this generated type comment go to Window - Preferences - Java - Code Generation - Code and Comments

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
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)

Method Summary

Methods

Modifier and Type	Method and Description
void	analyze(Constr myconfl, Pair results)
void	analyzeCP(Constr myconfl, Pair results)
void	claBumpActivity(Constr confl)
String	toString(String prefix) Display a textual representation of the solver configuration.
protected void	updateNumberOfReducedLearnedConstraints(IConflict confl)
protected void	updateNumberOfReductions(IConflict confl)

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, 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, 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, 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.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

Methods inherited from interface org.sat4j.specs.ISolverService

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

Constructor Detail

PBSolverCP

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

Parameters:

acg -

learner -

dsf -

PBSolverCP

public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
          PBDataStructureFactory dsf,
          SearchParams params,
          IOrder order,
          RestartStrategy restarter)

PBSolverCP

public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
          PBDataStructureFactory dsf,
          SearchParams params,
          IOrder order)

Method Detail

analyze

public void analyze(Constr myconfl,
           Pair results)
             throws TimeoutException

Overrides:

analyze in class Solver<PBDataStructureFactory>

Throws:

TimeoutException - if the timeout is reached during conflict analysis.

analyzeCP

public void analyzeCP(Constr myconfl,
             Pair results)
               throws TimeoutException

Throws:

TimeoutException

toString

public String toString(String prefix)

Description copied from interface: ISolver

Display a textual representation of the solver configuration.

Specified by:

toString in interface ISolver

Overrides:

toString in class Solver<PBDataStructureFactory>

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.

updateNumberOfReductions

protected void updateNumberOfReductions(IConflict confl)

updateNumberOfReducedLearnedConstraints

protected void updateNumberOfReducedLearnedConstraints(IConflict confl)

claBumpActivity

public void claBumpActivity(Constr confl)

Parameters:

outclause -