Solver (SAT4J core 2.3.4 API)

java.lang.Object
- org.sat4j.minisat.core.Solver<D>

All Implemented Interfaces:

Serializable, ICDCL<D>, Learner, IProblem, ISolver, ISolverService, RandomAccessModel, UnitPropagationListener
```
public class Solver<D extends DataStructureFactory>
extends Object
implements ISolverService, ICDCL<D>
```
The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Author:

leberre

See Also:
Serialized Form

Field Summary

Fields
Modifier and Type	Field and Description
`protected IVec<Constr>`	`constrs` Set of original constraints.
`protected D`	`dsfactory`
`ISimplifier`	`EXPENSIVE_SIMPLIFICATION`
`ISimplifier`	`EXPENSIVE_SIMPLIFICATION_WLONLY`
`LearnedConstraintsDeletionStrategy`	`glucose`
`protected LearnedConstraintsDeletionStrategy`	`learnedConstraintsDeletionStrategy`
`protected IVec<Constr>`	`learnts` Set of learned constraints.
`LearnedConstraintsDeletionStrategy`	`memory_based`
`static ISimplifier`	`NO_SIMPLIFICATION`
`protected ILogAble`	`out`
`protected int`	`rootLevel` position of assumptions before starting the search.
`protected Constr`	`sharedConflict`
`ISimplifier`	`SIMPLE_SIMPLIFICATION`
`protected SearchListener`	`slistener`
`protected IVecInt`	`trail` variable assignments (literals) in chronological order.
`protected IVecInt`	`trailLim` position of the decision levels on the trail.
`protected boolean`	`undertimeout`
`protected ILits`	`voc`

Constructor Summary

Constructors
Constructor and Description
`Solver(LearningStrategy<D> learner, D dsf, IOrder order, RestartStrategy restarter)` creates a Solver without LearningListener.
`Solver(LearningStrategy<D> learner, D dsf, SearchParams params, IOrder order, RestartStrategy restarter)`
`Solver(LearningStrategy<D> learner, D dsf, SearchParams params, IOrder order, RestartStrategy restarter, ILogAble logger)`

Method Summary

Methods
Modifier and Type	Method and Description
`void`	`addAllClauses(IVec<IVecInt> clauses)` Create clauses from a set of set of literals.
`IConstr`	`addAtLeast(IVecInt literals, int degree)` Create a cardinality constraint of the type "at least n of those literals must be satisfied"
`IConstr`	`addAtMost(IVecInt literals, int degree)` Create a cardinality constraint of the type "at most n of those literals must be satisfied"
`IConstr`	`addAtMostOnTheFly(int[] literals, int degree)` Add a new pseudo cardinality constraint sum literals <= degree in the solver.
`IConstr`	`addBlockingClause(IVecInt literals)` Add a clause in order to prevent an assignment to occur.
`IConstr`	`addClause(IVecInt literals)` Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
`IConstr`	`addClauseOnTheFly(int[] literals)` Add a new clause in the SAT solver.
`protected IConstr`	`addConstr(Constr constr)`
`IConstr`	`addExactly(IVecInt literals, int n)` Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
`void`	`analyze(Constr confl, Pair results)`
`protected void`	`analyzeAtRootLevel(Constr conflict)`
`IVecInt`	`analyzeFinalConflictInTermsOfAssumptions(Constr confl, IVecInt assumps, int conflictingLiteral)` Derive a subset of the assumptions causing the inconistency.
`boolean`	`assume(int p)`
`void`	`backtrack(int[] reason)` Ask the SAT solver to backtrack.
`protected void`	`cancelUntil(int level)` Cancel several levels of assumptions
`void`	`claBumpActivity(Constr confl)` Propagate activity to a constraint
`void`	`clearLearntClauses()` Remove clauses learned during the solving process.
`int`	`currentDecisionLevel()` To access the current decision level
`protected void`	`decayActivities()`
`int`	`decisionLevel()`
`protected IVecInt`	`dimacs2internal(IVecInt in)`
`boolean`	`enqueue(int p)` satisfies a literal
`boolean`	`enqueue(int p, Constr from)` satisfies a literal
`void`	`expireTimeout()` Expire the timeout of the solver.
`int[]`	`findModel()` Look for a model satisfying all the clauses available in the problem.
`int[]`	`findModel(IVecInt assumps)` Look for a model satisfying all the clauses available in the problem.
`LearnedConstraintsDeletionStrategy`	`fixedSize(int maxsize)`
`protected Set<Integer>`	`fromLastDecisionLevel(IVecInt lits)`
`DataStructureFactory`	`getDSFactory()`
`IConstr`	`getIthConstr(int i)` returns the ith constraint in the solver.
`IVec<Constr>`	`getLearnedConstraints()` Read-Only access to the list of constraints learned and not deleted so far in the solver.
`int[]`	`getLiteralsPropagatedAt(int decisionLevel)` To access the literals propagated at a specific decision level.
`ILogAble`	`getLogger()`
`String`	`getLogPrefix()`
`IOrder`	`getOrder()`
`IVecInt`	`getOutLearnt()`
`RestartStrategy`	`getRestartStrategy()`
`<S extends ISolverService> SearchListener<S>`	`getSearchListener()` Get the current SearchListener.
`SearchParams`	`getSearchParams()`
`ISimplifier`	`getSimplifier()`
`ISolver`	`getSolvingEngine()` Retrieve the real engine in case the engine is decorated by one or several decorator.
`Map<String,Number>`	`getStat()` To obtain a map of the available statistics from the solver.
`SolverStats`	`getStats()`
`int`	`getTimeout()` Useful to check the internal timeout of the solver.
`long`	`getTimeoutMs()` Useful to check the internal timeout of the solver.
`double[]`	`getVariableHeuristics()` Read-Only access to the value of the heuristics for each variable.
`ILits`	`getVocabulary()`
`protected void`	`initStats(SolverStats myStats)`
`boolean`	`isDBSimplificationAllowed()` Indicate whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.
`protected boolean`	`isNeedToReduceDB()`
`boolean`	`isSatisfiable()` Check the satisfiability of the set of constraints contained inside the solver.
`boolean`	`isSatisfiable(boolean global)` Check the satisfiability of the set of constraints contained inside the solver.
`boolean`	`isSatisfiable(IVecInt assumps)` Check the satisfiability of the set of constraints contained inside the solver.
`boolean`	`isSatisfiable(IVecInt assumps, boolean global)` Check the satisfiability of the set of constraints contained inside the solver.
`boolean`	`isSolverKeptHot()` Ask to the solver if it is in "hot" mode, meaning that the heuristics is not reset after call is isSatisfiable().
`boolean`	`isVerbose()` To know if the solver is in verbose mode (output allowed) or not.
`void`	`learn(Constr c)`
`int[]`	`model()` Si un mod?
`boolean`	`model(int var)` Provide the truth value of a specific variable in the model.
`int[]`	`modelWithInternalVariables()` That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance).
`protected int`	`nAssigns()`
`int`	`nConstraints()` To know the number of constraints currently available in the solver.
`int`	`newVar()` Deprecated.
`int`	`newVar(int howmany)` Declare `howmany` variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany.
`int`	`nextFreeVarId(boolean reserve)` Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).
`int`	`nVars()` Read-Only access to the number of variables declared in the solver.
`int[]`	`primeImplicant()` Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.
`boolean`	`primeImplicant(int p)` Check if a given literal is part of the prime implicant computed by the `IProblem.primeImplicant()` method.
`void`	`printInfos(PrintWriter out)` To print additional informations regarding the problem.
`void`	`printInfos(PrintWriter out, String prefix)` To print additional informations regarding the problem.
`void`	`printLearntClausesInfos(PrintWriter out, String prefix)`
`void`	`printStat(PrintStream out, String prefix)` Display statistics to the given output stream Please use writers instead of stream.
`void`	`printStat(PrintWriter out)` Display statistics to the given output writer
`void`	`printStat(PrintWriter out, String prefix)` Display statistics to the given output writer
`Constr`	`propagate()`
`int`	`realNumberOfVariables()` Retrieve the real number of variables used in the solver.
`protected void`	`reduceDB()`
`void`	`registerLiteral(int p)` Tell the solver to consider that the literal is in the CNF.
`boolean`	`removeConstr(IConstr co)` Remove a constraint returned by one of the add method from the solver.
`boolean`	`removeSubsumedConstr(IConstr co)` Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver.
`void`	`reset()` Clean up the internal state of the solver.
`void`	`setDataStructureFactory(D dsf)` Change the internal representation of the constraints.
`void`	`setDBSimplificationAllowed(boolean status)` Set whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.
`void`	`setExpectedNumberOfClauses(int nb)` To inform the solver of the expected number of clauses to read.
`void`	`setKeepSolverHot(boolean keepHot)` Changed the behavior of the SAT solver heuristics between successive calls.
`void`	`setLearnedConstraintsDeletionStrategy(ConflictTimer timer, LearnedConstraintsEvaluationType evaluation)`
`void`	`setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy lcds)`
`void`	`setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType evaluation)`
`void`	`setLearner(LearningStrategy<D> strategy)`
`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`	`setLogPrefix(String prefix)` Set the prefix used to display information.
`void`	`setNeedToReduceDB(boolean needToReduceDB)`
`void`	`setOrder(IOrder h)`
`void`	`setRestartStrategy(RestartStrategy restarter)`
`<S extends ISolverService> void`	`setSearchListener(SearchListener<S> sl)` Allow the user to hook a listener to the solver to be notified of the main steps of the search process.
`void`	`setSearchParams(SearchParams sp)`
`void`	`setSimplifier(ISimplifier simp)` Setup the reason simplification strategy.
`void`	`setSimplifier(SimplificationType simp)` Setup the reason simplification strategy.
`void`	`setTimeout(int t)` To set the internal timeout of the solver.
`void`	`setTimeoutMs(long t)` To set the internal timeout of the solver.
`void`	`setTimeoutOnConflicts(int count)` To set the internal timeout of the solver.
`void`	`setUnitClauseProvider(UnitClauseProvider ucp)` Allow the solver to ask for unit clauses before each restarts.
`void`	`setVerbose(boolean value)` Set the verbosity of the solver
`boolean`	`simplifyDB()`
`protected void`	`sortOnActivity()`
`void`	`stop()` Ask the SAT solver to stop the search.
`void`	`suggestNextLiteralToBranchOn(int l)` Suggests to the SAT solver to branch next on the given literal.
`String`	`toString()`
`String`	`toString(String prefix)` Display a textual representation of the solver configuration.
`Lbool`	`truthValue(int literal)` To access the truth value of a specific literal under current assignment.
`protected void`	`undoOne()`
`IVecInt`	`unsatExplanation()` Retrieve an explanation of the inconsistency in terms of assumption literals.
`void`	`unset(int p)` Unset a unit clause.
`void`	`varBumpActivity(int p)` Update the activity of a variable v.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - out
```
protected ILogAble out
```
  - constrs
```
protected final IVec<Constr> constrs
```
    Set of original constraints.
  - learnts
```
protected final IVec<Constr> learnts
```
    Set of learned constraints.
  - trail
```
protected final IVecInt trail
```
    variable assignments (literals) in chronological order.
  - trailLim
```
protected final IVecInt trailLim
```
    position of the decision levels on the trail.
  - rootLevel
```
protected int rootLevel
```
    position of assumptions before starting the search.
  - voc
```
protected ILits voc
```
  - undertimeout
```
protected volatile boolean undertimeout
```
  - dsfactory
```
protected D extends DataStructureFactory dsfactory
```
  - slistener
```
protected SearchListener slistener
```
  - NO_SIMPLIFICATION
```
public static final ISimplifier NO_SIMPLIFICATION
```
  - SIMPLE_SIMPLIFICATION
```
public final ISimplifier SIMPLE_SIMPLIFICATION
```
  - EXPENSIVE_SIMPLIFICATION
```
public final ISimplifier EXPENSIVE_SIMPLIFICATION
```
  - EXPENSIVE_SIMPLIFICATION_WLONLY
```
public final ISimplifier EXPENSIVE_SIMPLIFICATION_WLONLY
```
  - memory_based
```
public final LearnedConstraintsDeletionStrategy memory_based
```
    Since:
    
    2.1
  - glucose
```
public final LearnedConstraintsDeletionStrategy glucose
```
    Since:
    
    2.1
  - learnedConstraintsDeletionStrategy
```
protected LearnedConstraintsDeletionStrategy learnedConstraintsDeletionStrategy
```
  - sharedConflict
```
protected Constr sharedConflict
```
- Constructor Detail
  - Solver
```
public Solver(LearningStrategy<D> learner,
      D dsf,
      IOrder order,
      RestartStrategy restarter)
```
    creates a Solver without LearningListener. A learningListener must be added to the solver, else it won't backtrack!!! A data structure factory must be provided, else it won't work either.
  - Solver
```
public Solver(LearningStrategy<D> learner,
      D dsf,
      SearchParams params,
      IOrder order,
      RestartStrategy restarter)
```
  - Solver
```
public Solver(LearningStrategy<D> learner,
      D dsf,
      SearchParams params,
      IOrder order,
      RestartStrategy restarter,
      ILogAble logger)
```
- Method Detail
  - dimacs2internal
```
protected IVecInt dimacs2internal(IVecInt in)
```
  - registerLiteral
```
public void registerLiteral(int p)
```
    Description copied from interface: ISolver
    
    Tell the solver to consider that the literal is in the CNF. Since model() only return the truth value of the literals that appear in the solver, it is sometimes required that the solver provides a default truth value for a given literal. This happens for instance for MaxSat.
    
    Specified by:
    
    registerLiteral in interface ISolver
    
    Parameters:
    p - the literal in Dimacs format that should appear in the model.
  - setDataStructureFactory
```
public final void setDataStructureFactory(D dsf)
```
    Description copied from interface: ICDCL
    
    Change the internal representation of the constraints. Note that the heuristics must be changed prior to calling that method.
    
    Specified by:
    
    setDataStructureFactory in interface ICDCL<D extends DataStructureFactory>
    
    Parameters:
    dsf - the internal factory
  - isVerbose
```
public boolean isVerbose()
```
    Description copied from interface: ISolver
    
    To know if the solver is in verbose mode (output allowed) or not.
    
    Specified by:
    
    isVerbose in interface ISolver
    
    Returns:
    true if the solver is verbose.
    Since:
    
    2.2
  - setVerbose
```
public void setVerbose(boolean value)
```
    Description copied from interface: ISolver
    
    Set the verbosity of the solver
    
    Specified by:
    
    setVerbose in interface ISolver
    
    Parameters:
    value -
    Since:
    
    2.2
  - setSearchListener
```
public <S extends ISolverService> void setSearchListener(SearchListener<S> sl)
```
    Description copied from interface: ISolver
    
    Allow the user to hook a listener to the solver to be notified of the main steps of the search process.
    
    Specified by:
    
    setSearchListener in interface ISolver
    
    Parameters:
    sl - a Search Listener.
  - getSearchListener
```
public <S extends ISolverService> SearchListener<S> getSearchListener()
```
    Description copied from interface: ISolver
    
    Get the current SearchListener.
    
    Specified by:
    
    getSearchListener in interface ISolver
    
    Returns:
    a Search Listener.
  - setLearner
```
public void setLearner(LearningStrategy<D> strategy)
```
    Specified by:
    
    setLearner in interface ICDCL<D extends DataStructureFactory>
    
    See Also:
    ICDCL.setLearningStrategy(LearningStrategy)
  - setLearningStrategy
```
public void setLearningStrategy(LearningStrategy<D> strategy)
```
    Description copied from interface: ICDCL
    
    Allow to change the learning strategy, i.e. to decide which clauses/constraints should be learned by the solver after conflict analysis.
    
    Specified by:
    
    setLearningStrategy in interface ICDCL<D extends DataStructureFactory>
  - setTimeout
```
public void setTimeout(int t)
```
    Description copied from interface: ISolver
    
    To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver.
    
    Specified by:
    
    setTimeout in interface ISolver
    
    Parameters:
    t - the timeout (in s)
  - setTimeoutMs
```
public void setTimeoutMs(long t)
```
    Description copied from interface: ISolver
    
    To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver.
    
    Specified by:
    
    setTimeoutMs in interface ISolver
    
    Parameters:
    t - the timeout (in milliseconds)
  - setTimeoutOnConflicts
```
public void setTimeoutOnConflicts(int count)
```
    Description copied from interface: ISolver
    
    To set the internal timeout of the solver. When the timeout is reached, a timeout exception is launched by the solver. Here the timeout is given in number of conflicts. That way, the behavior of the solver should be the same across different architecture.
    
    Specified by:
    
    setTimeoutOnConflicts in interface ISolver
    
    Parameters:
    count - the timeout (in number of conflicts)
  - setSearchParams
```
public void setSearchParams(SearchParams sp)
```
    Specified by:
    
    setSearchParams in interface ICDCL<D extends DataStructureFactory>
  - getSearchParams
```
public SearchParams getSearchParams()
```
    Specified by:
    
    getSearchParams in interface ICDCL<D extends DataStructureFactory>
  - setRestartStrategy
```
public void setRestartStrategy(RestartStrategy restarter)
```
    Specified by:
    
    setRestartStrategy in interface ICDCL<D extends DataStructureFactory>
  - getRestartStrategy
```
public RestartStrategy getRestartStrategy()
```
    Specified by:
    
    getRestartStrategy in interface ICDCL<D extends DataStructureFactory>
  - expireTimeout
```
public void expireTimeout()
```
    Description copied from interface: ISolver
    
    Expire the timeout of the solver.
    
    Specified by:
    
    expireTimeout in interface ISolver
  - nAssigns
```
protected int nAssigns()
```
  - nConstraints
```
public int nConstraints()
```
    Description copied from interface: IProblem
    
    To know the number of constraints currently available in the solver. (without taking into account learned constraints).
    
    Specified by:
    
    nConstraints in interface IProblem
    
    Returns:
    the number of constraints added to the solver
  - learn
```
public void learn(Constr c)
```
    Specified by:
    
    learn in interface Learner
  - decisionLevel
```
public final int decisionLevel()
```
  - newVar
```
@Deprecated
public int newVar()
```
    Deprecated.
    
    Description copied from interface: ISolver
    
    Create a new variable in the solver (and thus in the vocabulary). WE STRONGLY ENCOURAGE TO PRECOMPUTE THE NUMBER OF VARIABLES NEEDED AND TO USE newVar(howmany) INSTEAD. IF YOU EXPERIENCE A PROBLEM OF EFFICIENCY WHEN READING/BUILDING YOUR SAT INSTANCE, PLEASE CHECK THAT YOU ARE NOT USING THAT METHOD.
    
    Specified by:
    
    newVar in interface ISolver
    
    Returns:
    the number of variables available in the vocabulary, which is the identifier of the new variable.
  - newVar
```
public int newVar(int howmany)
```
    Description copied from interface: IProblem
    
    Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany. That feature allows encodings to create additional variables with identifier starting at howmany+1.
    
    Specified by:
    
    newVar in interface IProblem
    
    Parameters:
    howmany - number of variables to create
    
    Returns:
    the total number of variables available in the solver (the highest variable number)
    See Also:
    IProblem.nVars()
  - addClause
```
public IConstr addClause(IVecInt literals)
                  throws ContradictionException
```
    Description copied from interface: ISolver
    
    Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. (classical Dimacs way of representing literals).
    
    Specified by:
    
    addClause in interface ISolver
    
    Parameters:
    literals - a set of literals
    
    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 it contains only falsified literals after unit propagation
    See Also:
    ISolver.removeConstr(IConstr)
  - removeConstr
```
public boolean removeConstr(IConstr co)
```
    Description copied from interface: ISolver
    
    Remove a constraint returned by one of the add method from the solver. All learned clauses will be cleared. Current implementation does not handle properly the case of unit clauses.
    
    Specified by:
    
    removeConstr in interface ISolver
    
    Parameters:
    co - a constraint returned by one of the add method.
    
    Returns:
    true if the constraint was successfully removed.
  - removeSubsumedConstr
```
public boolean removeSubsumedConstr(IConstr co)
```
    Description copied from interface: ISolverService
    
    Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver. Unlike the removeConstr() method, learned clauses will NOT be cleared. That method is expected to be used to remove constraints used in the optimization process. In order to prevent a wrong from the user, the method will only work if the argument is the last constraint added to the solver. An illegal argument exception will be thrown in other cases.
    
    Specified by:
    
    removeSubsumedConstr in interface ISolver
    
    Specified by:
    
    removeSubsumedConstr in interface ISolverService
    
    Parameters:
    co - a constraint returned by one of the add method. It must be the latest constr added to the solver.
    
    Returns:
    true if the constraint was successfully removed.
    Since:
    
    2.1
  - addAllClauses
```
public void addAllClauses(IVec<IVecInt> clauses)
                   throws ContradictionException
```
    Description copied from interface: ISolver
    
    Create clauses from a set of set of literals. This is convenient to create in a single call all the clauses (mandatory for the distributed version of the solver). It is mainly a loop to addClause().
    
    Specified by:
    
    addAllClauses in interface ISolver
    
    Parameters:
    clauses - a vector of set (VecInt) of literals in the dimacs format. The vector can be reused since the solver is not supposed to keep a reference to that vector.
    
    Throws:
    
    ContradictionException - iff the vector of literals is empty or if it contains only falsified literals after unit propagation
    See Also:
    ISolver.addClause(IVecInt)
  - addAtMost
```
public IConstr addAtMost(IVecInt literals,
                int degree)
                  throws ContradictionException
```
    Description copied from interface: ISolver
    
    Create a cardinality constraint of the type "at most n of those literals must be satisfied"
    
    Specified by:
    
    addAtMost in interface ISolver
    
    Parameters:
    literals - a set of literals The vector can be reused since the solver is not supposed to keep a reference to that vector.
    degree - the degree (n) 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 it contains more than degree satisfied literals after unit propagation
    See Also:
    ISolver.removeConstr(IConstr)
  - addAtLeast
```
public IConstr addAtLeast(IVecInt literals,
                 int degree)
                   throws ContradictionException
```
    Description copied from interface: ISolver
    
    Create a cardinality constraint of the type "at least n of those literals must be satisfied"
    
    Specified by:
    
    addAtLeast in interface ISolver
    
    Parameters:
    literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.
    degree - the degree (n) 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 degree literals are not remaining unfalsified after unit propagation
    See Also:
    ISolver.removeConstr(IConstr)
  - addExactly
```
public IConstr addExactly(IVecInt literals,
                 int n)
                   throws ContradictionException
```
    Description copied from interface: ISolver
    
    Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
    
    Specified by:
    
    addExactly in interface ISolver
    
    Parameters:
    literals - a set of literals. The vector can be reused since the solver is not supposed to keep a reference to that vector.
    n - the number of literals that must be satisfied
    
    Returns:
    a reference to the constraint added to the solver. It might return an object representing a group of constraints.
    
    Throws:
    
    ContradictionException - iff the constraint is trivially unsatisfiable.
  - simplifyDB
```
public boolean simplifyDB()
```
  - model
```
public int[] model()
```
    Si un mod?le est trouv?, ce vecteur contient le mod?le.
    
    Specified by:
    
    model in interface IProblem
    
    Returns:
    un mod?le de la formule.
    See Also:
    IProblem.isSatisfiable(), IProblem.isSatisfiable(IVecInt)
  - enqueue
```
public boolean enqueue(int p)
```
    Description copied from interface: UnitPropagationListener
    
    satisfies a literal
    
    Specified by:
    
    enqueue in interface UnitPropagationListener
    
    Parameters:
    p - a literal
    
    Returns:
    true if the assignment looks possible, false if a conflict occurs.
  - enqueue
```
public boolean enqueue(int p,
              Constr from)
```
    Description copied from interface: UnitPropagationListener
    
    satisfies a literal
    
    Specified by:
    
    enqueue in interface UnitPropagationListener
    
    Parameters:
    p - a literal
    from - a reason explaining why p should be satisfied.
    
    Returns:
    true if the assignment looks possible, false if a conflict occurs.
  - analyze
```
public void analyze(Constr confl,
           Pair results)
             throws TimeoutException
```
    Throws:
    
    TimeoutException - if the timeout is reached during conflict analysis.
  - analyzeFinalConflictInTermsOfAssumptions
```
public IVecInt analyzeFinalConflictInTermsOfAssumptions(Constr confl,
                                               IVecInt assumps,
                                               int conflictingLiteral)
```
    Derive a subset of the assumptions causing the inconistency.
    
    Parameters:
    confl - the last conflict of the search, occuring at root level.
    assumps - the set of assumption literals
    conflictingLiteral - the literal detected conflicting while propagating assumptions.
    
    Returns:
    a subset of assumps causing the inconsistency.
    Since:
    
    2.2
  - setSimplifier
```
public void setSimplifier(SimplificationType simp)
```
    Description copied from interface: ICDCL
    
    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.
    
    Specified by:
    
    setSimplifier in interface ICDCL<D extends DataStructureFactory>
    
    Parameters:
    simp - a simplification type.
  - setSimplifier
```
public void setSimplifier(ISimplifier simp)
```
    Description copied from interface: ICDCL
    
    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.
    
    Specified by:
    
    setSimplifier in interface ICDCL<D extends DataStructureFactory>
  - getSimplifier
```
public ISimplifier getSimplifier()
```
    Specified by:
    
    getSimplifier in interface ICDCL<D extends DataStructureFactory>
  - undoOne
```
protected void undoOne()
```
  - claBumpActivity
```
public void claBumpActivity(Constr confl)
```
    Propagate activity to a constraint
    
    Parameters:
    confl - a constraint
  - varBumpActivity
```
public void varBumpActivity(int p)
```
    Description copied from interface: VarActivityListener
    
    Update the activity of a variable v.
    
    Parameters:
    p - a literal (v<<1 or v<<1^1)
  - propagate
```
public final Constr propagate()
```
    Returns:
    null if not conflict is found, else a conflicting constraint.
  - assume
```
public boolean assume(int p)
```
    Returns:
    false ssi conflit imm?diat.
  - cancelUntil
```
protected void cancelUntil(int level)
```
    Cancel several levels of assumptions
    
    Parameters:
    level -
  - analyzeAtRootLevel
```
protected void analyzeAtRootLevel(Constr conflict)
```
  - primeImplicant
```
public int[] primeImplicant()
```
    Description copied from interface: IProblem
    
    Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.
    
    Specified by:
    
    primeImplicant in interface IProblem
    
    Returns:
    a prime implicant of the formula as an array of literal, Dimacs format.
  - primeImplicant
```
public boolean primeImplicant(int p)
```
    Description copied from interface: IProblem
    
    Check if a given literal is part of the prime implicant computed by the IProblem.primeImplicant() method.
    
    Specified by:
    
    primeImplicant in interface IProblem
    
    Parameters:
    p - a literal in Dimacs format
    
    Returns:
    true iff p belongs to IProblem.primeImplicant()
  - model
```
public boolean model(int var)
```
    Description copied from interface: RandomAccessModel
    
    Provide the truth value of a specific variable in the model. That method should be called AFTER isSatisfiable() if the formula is satisfiable. Else an exception UnsupportedOperationException is launched.
    
    Specified by:
    
    model in interface RandomAccessModel
    
    Parameters:
    var - the variable id in Dimacs format
    
    Returns:
    the truth value of that variable in the model
    See Also:
    #model()
  - clearLearntClauses
```
public void clearLearntClauses()
```
    Description copied from interface: ISolver
    
    Remove clauses learned during the solving process.
    
    Specified by:
    
    clearLearntClauses in interface ISolver
  - reduceDB
```
protected final void reduceDB()
```
  - sortOnActivity
```
protected void sortOnActivity()
```
    Parameters:
    learnts -
  - decayActivities
```
protected void decayActivities()
```
  - isSatisfiable
```
public boolean isSatisfiable()
                      throws TimeoutException
```
    Description copied from interface: IProblem
    
    Check the satisfiability of the set of constraints contained inside the solver.
    
    Specified by:
    
    isSatisfiable in interface IProblem
    
    Returns:
    true iff the set of constraints is satisfiable, else false.
    
    Throws:
    
    TimeoutException
  - isSatisfiable
```
public boolean isSatisfiable(boolean global)
                      throws TimeoutException
```
    Description copied from interface: IProblem
    
    Check the satisfiability of the set of constraints contained inside the solver.
    
    Specified by:
    
    isSatisfiable in interface IProblem
    
    Parameters:
    global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
    
    Returns:
    true iff the set of constraints is satisfiable, else false.
    
    Throws:
    
    TimeoutException
  - isSatisfiable
```
public boolean isSatisfiable(IVecInt assumps)
                      throws TimeoutException
```
    Description copied from interface: IProblem
    
    Check the satisfiability of the set of constraints contained inside the solver.
    
    Specified by:
    
    isSatisfiable in interface IProblem
    
    Parameters:
    assumps - a set of literals (represented by usual non null integers in Dimacs format).
    
    Returns:
    true if the set of constraints is satisfiable when literals are satisfied, else false.
    
    Throws:
    
    TimeoutException
  - fixedSize
```
public final LearnedConstraintsDeletionStrategy fixedSize(int maxsize)
```
  - setLearnedConstraintsDeletionStrategy
```
public void setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy lcds)
```
    Specified by:
    
    setLearnedConstraintsDeletionStrategy in interface ICDCL<D extends DataStructureFactory>
  - isSatisfiable
```
public boolean isSatisfiable(IVecInt assumps,
                    boolean global)
                      throws TimeoutException
```
    Description copied from interface: IProblem
    
    Check the satisfiability of the set of constraints contained inside the solver.
    
    Specified by:
    
    isSatisfiable in interface IProblem
    
    Parameters:
    assumps - a set of literals (represented by usual non null integers in Dimacs format).
    global - whether that call is part of a global process (i.e. optimization) or not. if (global), the timeout will not be reset between each call.
    
    Returns:
    true if the set of constraints is satisfiable when literals are satisfied, else false.
    
    Throws:
    
    TimeoutException
  - printInfos
```
public void printInfos(PrintWriter out)
```
    Description copied from interface: IProblem
    
    To print additional informations regarding the problem.
    
    Specified by:
    
    printInfos in interface IProblem
    
    Parameters:
    out - the place to print the information
    See Also:
    #setLogPrefix(String)
  - printInfos
```
public void printInfos(PrintWriter out,
              String prefix)
```
    Description copied from interface: IProblem
    
    To print additional informations regarding the problem.
    
    Specified by:
    
    printInfos in interface IProblem
    
    Parameters:
    out - the place to print the information
    prefix - the prefix to put in front of each line
  - printLearntClausesInfos
```
public void printLearntClausesInfos(PrintWriter out,
                           String prefix)
```
    Since:
    
    2.1
  - getStats
```
public SolverStats getStats()
```
    Specified by:
    
    getStats in interface ICDCL<D extends DataStructureFactory>
  - initStats
```
protected void initStats(SolverStats myStats)
```
    Parameters:
    myStats -
    Since:
    
    2.2
  - getOrder
```
public IOrder getOrder()
```
    Specified by:
    
    getOrder in interface ICDCL<D extends DataStructureFactory>
  - setOrder
```
public void setOrder(IOrder h)
```
    Specified by:
    
    setOrder in interface ICDCL<D extends DataStructureFactory>
  - getVocabulary
```
public ILits getVocabulary()
```
  - reset
```
public void reset()
```
    Description copied from interface: ISolver
    
    Clean up the internal state of the solver. Note that such method should also be called when you no longer need the solver because the state of the solver may prevent the GC to proceed. There is a known issue for instance where failing to call reset() on a solver will keep timer threads alive and exhausts memory.
    
    Specified by:
    
    reset in interface ISolver
  - nVars
```
public int nVars()
```
    Description copied from interface: ISolverService
    
    Read-Only access to the number of variables declared in the solver.
    
    Specified by:
    
    nVars in interface IProblem
    
    Specified by:
    
    nVars in interface ISolverService
    
    Returns:
    the maximum variable id (Dimacs format) reserved in the solver.
    See Also:
    IProblem.newVar(int)
  - addConstr
```
protected IConstr addConstr(Constr constr)
```
    Parameters:
    constr - a constraint implementing the Constr interface.
    
    Returns:
    a reference to the constraint for external use.
  - getDSFactory
```
public DataStructureFactory getDSFactory()
```
  - getOutLearnt
```
public IVecInt getOutLearnt()
```
  - getIthConstr
```
public IConstr getIthConstr(int i)
```
    returns the ith constraint in the solver.
    
    Parameters:
    i - the constraint number (begins at 0)
    
    Returns:
    the ith constraint
  - printStat
```
public void printStat(PrintStream out,
             String prefix)
```
    Description copied from interface: ISolver
    
    Display statistics to the given output stream Please use writers instead of stream.
    
    Specified by:
    
    printStat in interface ISolver
    
    prefix - the prefix to put in front of each line
    See Also:
    ISolver.printStat(PrintWriter, String)
  - printStat
```
public void printStat(PrintWriter out)
```
    Description copied from interface: ISolver
    
    Display statistics to the given output writer
    
    Specified by:
    
    printStat in interface ISolver
    
    See Also:
    ISolver.setLogPrefix(String)
  - printStat
```
public void printStat(PrintWriter out,
             String prefix)
```
    Description copied from interface: ISolver
    
    Display statistics to the given output writer
    
    Specified by:
    
    printStat in interface ISolver
    
    prefix - the prefix to put in front of each line
  - 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
    
    Parameters:
    prefix - the prefix to use on each line.
    
    Returns:
    a textual description of the solver internals.
  - toString
```
public String toString()
```
    Overrides:
    
    toString in class Object
  - getTimeout
```
public int getTimeout()
```
    Description copied from interface: ISolver
    
    Useful to check the internal timeout of the solver.
    
    Specified by:
    
    getTimeout in interface ISolver
    
    Returns:
    the internal timeout of the solver (in seconds)
  - getTimeoutMs
```
public long getTimeoutMs()
```
    Description copied from interface: ISolver
    
    Useful to check the internal timeout of the solver.
    
    Specified by:
    
    getTimeoutMs in interface ISolver
    
    Returns:
    the internal timeout of the solver (in milliseconds)
    Since:
    
    2.1
  - setExpectedNumberOfClauses
```
public void setExpectedNumberOfClauses(int nb)
```
    Description copied from interface: ISolver
    
    To inform the solver of the expected number of clauses to read. This is an optional method, that is called when the p cnf line is read in dimacs formatted input file. Note that this method is supposed to be called AFTER a call to newVar(int)
    
    Specified by:
    
    setExpectedNumberOfClauses in interface ISolver
    
    Parameters:
    nb - the expected number of clauses.
    See Also:
    IProblem.newVar(int)
  - getStat
```
public Map<String,Number> getStat()
```
    Description copied from interface: ISolver
    
    To obtain a map of the available statistics from the solver. Note that some keys might be specific to some solvers.
    
    Specified by:
    
    getStat in interface ISolver
    
    Returns:
    a Map with the name of the statistics as key.
  - findModel
```
public int[] findModel()
                throws TimeoutException
```
    Description copied from interface: IProblem
    
    Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable() and model() methods, as shown in the pseudo-code: if (isSatisfiable()) { return model(); } return null;
    
    Specified by:
    
    findModel in interface IProblem
    
    Returns:
    a model of the formula as an array of literals to satisfy, or null if no model is found
    
    Throws:
    
    TimeoutException - if a model cannot be found within the given timeout.
  - findModel
```
public int[] findModel(IVecInt assumps)
                throws TimeoutException
```
    Description copied from interface: IProblem
    
    Look for a model satisfying all the clauses available in the problem. It is an alternative to isSatisfiable(IVecInt) and model() methods, as shown in the pseudo-code: if (isSatisfiable(assumpt)) { return model(); } return null;
    
    Specified by:
    
    findModel in interface IProblem
    
    Returns:
    a model of the formula as an array of literals to satisfy, or null if no model is found
    
    Throws:
    
    TimeoutException - if a model cannot be found within the given timeout.
  - isDBSimplificationAllowed
```
public boolean isDBSimplificationAllowed()
```
    Description copied from interface: ISolver
    
    Indicate whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables. Note that the solver should not be allowed to perform such simplification when constraint removal is planned.
    
    Specified by:
    
    isDBSimplificationAllowed in interface ISolver
  - setDBSimplificationAllowed
```
public void setDBSimplificationAllowed(boolean status)
```
    Description copied from interface: ISolver
    
    Set whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables. Note that the solver should not be allowed to perform such simplification when constraint removal is planned.
    
    Specified by:
    
    setDBSimplificationAllowed in interface ISolver
  - nextFreeVarId
```
public int nextFreeVarId(boolean reserve)
```
    Description copied from interface: ISolver
    
    Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number). Note that a previous call to newVar(max) will reserve in the solver the variable identifier from 1 to max, so nextFreeVarId() would return max+1, even if some variable identifiers smaller than max are not used. By default, the method will always answer by the maximum variable identifier used so far + 1. The number of variables reserved in the solver is accessible through the ISolver.realNumberOfVariables() method.
    
    Specified by:
    
    nextFreeVarId in interface ISolver
    
    Parameters:
    reserve - if true, the maxVarId is updated in the solver, i.e. successive calls to nextFreeVarId(true) will return increasing variable id while successive calls to nextFreeVarId(false) will always answer the same.
    
    Returns:
    a variable identifier not in use in the constraints already inside the solver.
    Since:
    
    2.1
    
    See Also:
    ISolver.realNumberOfVariables()
  - addBlockingClause
```
public IConstr addBlockingClause(IVecInt literals)
                          throws ContradictionException
```
    Description copied from interface: ISolver
    
    Add a clause in order to prevent an assignment to occur. This happens usually when iterating over models for instance.
    
    Specified by:
    
    addBlockingClause in interface ISolver
    
    Returns:
    
    Throws:
    
    ContradictionException
    Since:
    
    2.1
  - unset
```
public void unset(int p)
```
    Description copied from interface: UnitPropagationListener
    
    Unset a unit clause. The effect of such method is to unset all truth values on the stack until the given literal is found (that literal included).
    
    Specified by:
    
    unset in interface UnitPropagationListener
    
    Since:
    
    2.1
  - setLogPrefix
```
public void setLogPrefix(String prefix)
```
    Description copied from interface: ISolver
    
    Set the prefix used to display information.
    
    Specified by:
    
    setLogPrefix in interface ISolver
    
    Parameters:
    prefix - the prefix to be in front of each line of text
    Since:
    
    2.2
  - getLogPrefix
```
public String getLogPrefix()
```
    Specified by:
    
    getLogPrefix in interface ISolver
    
    Specified by:
    
    getLogPrefix in interface ISolverService
    
    Returns:
    the string used to prefix the output.
    Since:
    
    2.2
  - unsatExplanation
```
public IVecInt unsatExplanation()
```
    Description copied from interface: ISolver
    
    Retrieve an explanation of the inconsistency in terms of assumption literals. This is only application when isSatisfiable(assumps) is used. Note that !isSatisfiable(assumps)&&assumps.contains(unsatExplanation()) should hold.
    
    Specified by:
    
    unsatExplanation in interface ISolver
    
    Returns:
    a subset of the assumptions used when calling isSatisfiable(assumps). Will return null if not applicable (i.e. no assumptions used).
    Since:
    
    2.2
    
    See Also:
    IProblem.isSatisfiable(IVecInt), IProblem.isSatisfiable(IVecInt, boolean)
  - modelWithInternalVariables
```
public int[] modelWithInternalVariables()
```
    Description copied from interface: ISolver
    
    That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance). If no variables are added in the solver, then Arrays.equals(model(),modelWithInternalVariables()). In case new variables are added to the solver, then the number of models returned by that method is greater of equal to the number of models returned by model() when using a ModelIterator.
    
    Specified by:
    
    modelWithInternalVariables in interface ISolver
    
    Returns:
    an array of literals, in Dimacs format, corresponding to a model of the formula over all the variables declared in the solver.
    Since:
    
    2.3.1
    
    See Also:
    IProblem.model(), ModelIterator
  - realNumberOfVariables
```
public int realNumberOfVariables()
```
    Description copied from interface: ISolver
    
    Retrieve the real number of variables used in the solver. In many cases, realNumberOfVariables()==nVars(). However, when working with SAT encodings or translation from MAXSAT to PMS, one can have realNumberOfVariables()>nVars(). Those additional variables are supposed to be created using the ISolver.nextFreeVarId(boolean) method.
    
    Specified by:
    
    realNumberOfVariables in interface ISolver
    
    Returns:
    the number of variables reserved in the solver.
    Since:
    
    2.3.1
    
    See Also:
    ISolver.nextFreeVarId(boolean)
  - stop
```
public void stop()
```
    Description copied from interface: ISolverService
    
    Ask the SAT solver to stop the search.
    
    Specified by:
    
    stop in interface ISolverService
    
    Since:
    
    2.3.2
  - backtrack
```
public void backtrack(int[] reason)
```
    Description copied from interface: ISolverService
    
    Ask the SAT solver to backtrack. It is mandatory to provide a reason for backtracking, in terms of literals (which should be falsified under current assignment). The reason is not added to the clauses of the solver: only the result of the analysis is stored in the learned clauses. Note that these clauses may be removed latter.
    
    Specified by:
    
    backtrack in interface ISolverService
    
    Parameters:
    reason - a set of literals, in Dimacs format, currently falsified, i.e. for (int l : reason) assert truthValue(l) == Lbool.FALSE
    Since:
    
    2.3.2
  - truthValue
```
public Lbool truthValue(int literal)
```
    Description copied from interface: ISolverService
    
    To access the truth value of a specific literal under current assignment.
    
    Specified by:
    
    truthValue in interface ISolverService
    
    Parameters:
    literal - a Dimacs literal, i.e. a non-zero integer.
    
    Returns:
    true or false if the literal is assigned, else undefined.
    Since:
    
    2.3.2
  - currentDecisionLevel
```
public int currentDecisionLevel()
```
    Description copied from interface: ISolverService
    
    To access the current decision level
    
    Specified by:
    
    currentDecisionLevel in interface ISolverService
    
    Since:
    
    2.3.2
  - getLiteralsPropagatedAt
```
public int[] getLiteralsPropagatedAt(int decisionLevel)
```
    Description copied from interface: ISolverService
    
    To access the literals propagated at a specific decision level.
    
    Specified by:
    
    getLiteralsPropagatedAt in interface ISolverService
    
    Parameters:
    decisionLevel - a decision level between 0 and #currentDecisionLevel()
    Since:
    
    2.3.2
  - suggestNextLiteralToBranchOn
```
public void suggestNextLiteralToBranchOn(int l)
```
    Description copied from interface: ISolverService
    
    Suggests to the SAT solver to branch next on the given literal.
    
    Specified by:
    
    suggestNextLiteralToBranchOn in interface ISolverService
    
    Parameters:
    l - a literal in Dimacs format.
    Since:
    
    2.3.2
  - isNeedToReduceDB
```
protected boolean isNeedToReduceDB()
```
  - setNeedToReduceDB
```
public void setNeedToReduceDB(boolean needToReduceDB)
```
    Specified by:
    
    setNeedToReduceDB in interface ICDCL<D extends DataStructureFactory>
  - setLogger
```
public void setLogger(ILogAble out)
```
    Specified by:
    
    setLogger in interface ICDCL<D extends DataStructureFactory>
  - getLogger
```
public ILogAble getLogger()
```
    Specified by:
    
    getLogger in interface ICDCL<D extends DataStructureFactory>
  - getVariableHeuristics
```
public double[] getVariableHeuristics()
```
    Description copied from interface: ISolverService
    
    Read-Only access to the value of the heuristics for each variable. Note that for efficiency reason, the real array storing the value of the heuristics is returned. DO NOT CHANGE THE VALUES IN THAT ARRAY.
    
    Specified by:
    
    getVariableHeuristics in interface ISolverService
    
    Returns:
    the value of the heuristics for each variable (using Dimacs index).
  - getLearnedConstraints
```
public IVec<Constr> getLearnedConstraints()
```
    Description copied from interface: ISolverService
    
    Read-Only access to the list of constraints learned and not deleted so far in the solver. Note that for efficiency reason, the real list of constraints managed by the solver is returned. DO NOT MODIFY THAT LIST NOR ITS CONSTRAINTS.
    
    Specified by:
    
    getLearnedConstraints in interface ISolverService
    
    Returns:
    the constraints learned and kept so far by the solver.
  - setLearnedConstraintsDeletionStrategy
```
public void setLearnedConstraintsDeletionStrategy(ConflictTimer timer,
                                         LearnedConstraintsEvaluationType evaluation)
```
    Specified by:
    
    setLearnedConstraintsDeletionStrategy in interface ICDCL<D extends DataStructureFactory>
    
    Parameters:
    timer - when to apply constraints cleanup.
    evaluation - the strategy used to evaluate learned clauses.
    Since:
    
    2.3.2
  - setLearnedConstraintsDeletionStrategy
```
public void setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType evaluation)
```
    Specified by:
    
    setLearnedConstraintsDeletionStrategy in interface ICDCL<D extends DataStructureFactory>
    
    Parameters:
    evaluation - the strategy used to evaluate learned clauses.
    Since:
    
    2.3.2
  - isSolverKeptHot
```
public boolean isSolverKeptHot()
```
    Description copied from interface: ISolver
    
    Ask to the solver if it is in "hot" mode, meaning that the heuristics is not reset after call is isSatisfiable(). This is only useful in case of repeated calls to the solver with same set of variables.
    
    Specified by:
    
    isSolverKeptHot in interface ISolver
    
    Returns:
    true iff the solver keep the heuristics value unchanged across calls.
  - setKeepSolverHot
```
public void setKeepSolverHot(boolean keepHot)
```
    Description copied from interface: ISolver
    
    Changed the behavior of the SAT solver heuristics between successive calls. If the value is true, then the solver will be "hot" on reuse, i.e. the heuristics will not be reset. Else the heuristics will be reset.
    
    Specified by:
    
    setKeepSolverHot in interface ISolver
    
    Parameters:
    keepHot - true to keep the heuristics values across calls, false either.
  - addClauseOnTheFly
```
public IConstr addClauseOnTheFly(int[] literals)
```
    Description copied from interface: ISolverService
    
    Add a new clause in the SAT solver. The new clause may contain new variables. The clause may be falsified, in that case, the difference with backtrack() is that the new clause is appended to the solver as a regular clause. Thus it will not be removed by aggressive clause deletion. The clause may be assertive at a given decision level. In that case, the solver should backtrack to the proper decision level. In other cases, the search should simply proceed.
    
    Specified by:
    
    addClauseOnTheFly in interface ISolverService
    
    Parameters:
    literals - a set of literals in Dimacs format.
  - getSolvingEngine
```
public ISolver getSolvingEngine()
```
    Description copied from interface: ISolver
    
    Retrieve the real engine in case the engine is decorated by one or several decorator. This can be used for instance to setup the engine, which requires to bypass all the decorators. It is thus safe to downcast the ISolver to an ICDCL interface. We cannot directly return an ICDCL object because we are not on the same abstraction level here.
    
    Specified by:
    
    getSolvingEngine in interface ISolver
    
    Returns:
    the solver
  - addAtMostOnTheFly
```
public IConstr addAtMostOnTheFly(int[] literals,
                        int degree)
```
    Description copied from interface: ISolverService
    
    Add a new pseudo cardinality constraint sum literals <= degree in the solver. The constraint must be falsified under current assignment.
    
    Specified by:
    
    addAtMostOnTheFly in interface ISolverService
    
    Parameters:
    literals -
    degree - the maximal number of literals which can be satisfied.
  - fromLastDecisionLevel
```
protected Set<Integer> fromLastDecisionLevel(IVecInt lits)
```
  - setUnitClauseProvider
```
public void setUnitClauseProvider(UnitClauseProvider ucp)
```
    Description copied from interface: ISolver
    
    Allow the solver to ask for unit clauses before each restarts.
    
    Specified by:
    
    setUnitClauseProvider in interface ISolver
    
    Parameters:
    ucp - an object able to provide unit clauses.

Class Solver<D extends DataStructureFactory>

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

out

constrs

learnts

trail

trailLim

rootLevel

voc

undertimeout

dsfactory

slistener

NO_SIMPLIFICATION

SIMPLE_SIMPLIFICATION

EXPENSIVE_SIMPLIFICATION

EXPENSIVE_SIMPLIFICATION_WLONLY

memory_based

glucose

learnedConstraintsDeletionStrategy

sharedConflict

Constructor Detail

Solver

Solver

Solver

Method Detail

dimacs2internal

registerLiteral

setDataStructureFactory

isVerbose

setVerbose

setSearchListener

getSearchListener

setLearner

setLearningStrategy

setTimeout

setTimeoutMs

setTimeoutOnConflicts

setSearchParams

getSearchParams

setRestartStrategy

getRestartStrategy

expireTimeout

nAssigns

nConstraints

learn

decisionLevel

newVar

newVar

addClause

removeConstr

removeSubsumedConstr

addAllClauses

addAtMost

addAtLeast

addExactly

simplifyDB

model

enqueue

enqueue

analyze

analyzeFinalConflictInTermsOfAssumptions

setSimplifier

setSimplifier

getSimplifier

undoOne

claBumpActivity

varBumpActivity

propagate

assume

cancelUntil

analyzeAtRootLevel

primeImplicant

primeImplicant

model

clearLearntClauses

reduceDB