org.sat4j.pb.core
Class PBSolverWithImpliedClause

java.lang.Object
  extended by org.sat4j.minisat.core.Solver<PBDataStructureFactory>
      extended by org.sat4j.pb.core.PBSolver
          extended by org.sat4j.pb.core.PBSolverCP
              extended by org.sat4j.pb.core.PBSolverWithImpliedClause
All Implemented Interfaces:
Serializable, ICDCL<PBDataStructureFactory>, Learner, UnitPropagationListener, IPBCDCLSolver<PBDataStructureFactory>, IPBSolver, IProblem, ISolver, ISolverService

public class PBSolverWithImpliedClause
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, SIMPLE_SIMPLIFICATION, slistener, trail, trailLim, undertimeout, voc
 
Constructor Summary
PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
           
 
Method Summary
 IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree)
          Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied"
 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, addExactly, addExactly, getObjectiveFunction, setObjectiveFunction
 
Methods inherited from class org.sat4j.minisat.core.Solver
addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, addClause, 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, getSimplifier, 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, printLearntClausesInfos, printStat, printStat, propagate, realNumberOfVariables, reduceDB, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDataStructureFactory, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearnedConstraintsDeletionStrategy, setLearner, 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, 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, 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
 

Constructor Detail

PBSolverWithImpliedClause

public PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner,
                                 PBDataStructureFactory dsf,
                                 IOrder order)
Method Detail

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt literals,
                                IVec<BigInteger> coeffs,
                                boolean moreThan,
                                BigInteger degree)
                         throws ContradictionException
Description copied from interface: IPBSolver
Create a Pseudo-Boolean constraint of the type "at least n or at most n of those literals must be satisfied"

Specified by:
addPseudoBoolean in interface IPBSolver
Overrides:
addPseudoBoolean in class PBSolver
Parameters:
literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.
coeffs - the coefficients of the literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.
moreThan - true if it is a constraint >= degree, false if it is a constraint <= degree
degree - the degree of the cardinality constraint
Returns:
a reference to the constraint added in the solver, to use in removeConstr().
Throws:
ContradictionException - iff the vector of literals is empty or if the constraint is falsified after unit propagation
See Also:
ISolver.removeConstr(IConstr)

toString

public String toString(String prefix)
Specified by:
toString in interface ISolver
Overrides:
toString in class PBSolverCP

claBumpActivity

public void claBumpActivity(Constr arg0)


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