org.sat4j.minisat.core
Class Solver

java.lang.Object
  org.sat4j.minisat.core.Solver

All Implemented Interfaces:

java.io.Serializable, Learner, UnitPropagationListener, IProblem, ISolver

Direct Known Subclasses:

PBSolver

public class Solver
extends java.lang.Object
implements ISolver, UnitPropagationListener, Learner, java.io.Serializable

Author:

leberre

See Also:

Serialized Form

Field Summary

static org.sat4j.minisat.core.Solver.ISimplifier	NO_SIMPLIFICATION
org.sat4j.minisat.core.Solver.ISimplifier	SIMPLE_SIMPLIFICATION

Constructor Summary

Solver(AssertingClauseGenerator acg, LearningStrategy learner, DataStructureFactory dsf, IOrder order)
creates a Solver without LearningListener.

Solver(AssertingClauseGenerator acg, LearningStrategy learner, DataStructureFactory dsf, SearchParams params, IOrder order)

Method Summary

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	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	addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
int	analyze(Constr confl, Handle<Constr> outLearntRef)
boolean	assume(int p)
void	claBumpActivity(Constr confl) Propagate activity to a constraint
int	decisionLevel()
static int	decode2dimacs(int p) decode the internal representation of a literal into Dimacs format.
boolean	enqueue(int p) Satisfait un litt?
boolean	enqueue(int p, Constr from) Put the literal on the queue of assignments to be done.
DataStructureFactory	getDSFactory()
IConstr	getIthConstr(int i) returns the ith constraint in the solver.
IOrder	getOrder()
IVecInt	getOutLearnt()
java.util.Map<java.lang.String,java.lang.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.
ILits	getVocabulary()
boolean	isSatisfiable() 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.
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	nConstraints() To know the number of constraints currently available in the solver.
int	newVar() Create a new variable in the solver (and thus in the vocabulary).
int	newVar(int howmany) Create howmany variables in the solver (and thus in the vocabulary).
int	nVars() To know the number of variables used in the solver.
void	printStat(java.io.PrintStream out, java.lang.String prefix) Display statistics to the given output stream Please use writers instead of stream.
void	printStat(java.io.PrintWriter out, java.lang.String prefix) Display statistics to the given output writer
Constr	propagate()
boolean	removeConstr(IConstr co) Remove a constraint returned by one of the add method from the solver.
void	reset() Clean up the internal state of the solver.
void	setDataStructureFactory(DataStructureFactory dsf) Change the internatal representation of the contraints.
void	setExpectedNumberOfClauses(int nb) To inform the solver of the expected number of clauses to read.
void	setOrder(IOrder h)
void	setSearchListener(SearchListener sl)
void	setSimplifier(org.sat4j.minisat.core.Solver.ISimplifier simp)
void	setTimeout(int t) To set the internal timeout of the solver.
boolean	simplifyDB()
java.lang.String	toString()
java.lang.String	toString(java.lang.String prefix) Display a textual representation of the solver configuration.
void	varBumpActivity(int p) Update the activity of a variable v.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

NO_SIMPLIFICATION

public static final org.sat4j.minisat.core.Solver.ISimplifier NO_SIMPLIFICATION

SIMPLE_SIMPLIFICATION

public final org.sat4j.minisat.core.Solver.ISimplifier SIMPLE_SIMPLIFICATION

Constructor Detail

Solver

public Solver(AssertingClauseGenerator acg,
              LearningStrategy learner,
              DataStructureFactory dsf,
              IOrder order)

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.

Parameters:

acg - an asserting clause generator

Solver

public Solver(AssertingClauseGenerator acg,
              LearningStrategy learner,
              DataStructureFactory dsf,
              SearchParams params,
              IOrder order)

Method Detail

setDataStructureFactory

public void setDataStructureFactory(DataStructureFactory dsf)

Change the internatal representation of the contraints. Note that the heuristics must be changed prior to calling that method.

Parameters:

dsf - the internal factory

setSearchListener

public void setSearchListener(SearchListener sl)

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)

nConstraints

public int nConstraints()

Description copied from interface: IProblem

To know the number of constraints currently available in the solver. (without taking into account learnt constraints).

Specified by:

nConstraints in interface IProblem

Returns:

the number of contraints added to the solver

learn

public void learn(Constr c)

Specified by:

learn in interface Learner

decisionLevel

public int decisionLevel()

newVar

public int newVar()

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: ISolver

Create howmany variables in the solver (and thus in the vocabulary).

Specified by:

newVar in interface ISolver

Parameters:

howmany - number of variables to create

Returns:

the total number of variables available in the solver (the highest variable number)

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. (clasical 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 learnt clauses will be cleared.

Specified by:

removeConstr in interface ISolver

Parameters:

co - a constraint returned by one of the add method.

Returns:

true if the constraint was sucessfully removed.

addPseudoBoolean

public IConstr addPseudoBoolean(IVecInt literals,
                                IVec<java.math.BigInteger> coeffs,
                                boolean moreThan,
                                java.math.BigInteger degree)
                         throws ContradictionException

Description copied from interface: ISolver

Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

Specified by:

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

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

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)

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 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 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)

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.

enqueue

public boolean enqueue(int p)

Satisfait un litt?ral

Specified by:

enqueue in interface UnitPropagationListener

Parameters:

p - le litt?ral

Returns:

true si tout se passe bien, false si un conflit appara?t.

enqueue

public boolean enqueue(int p,
                       Constr from)

Put the literal on the queue of assignments to be done.

Specified by:

enqueue in interface UnitPropagationListener

Parameters:

p - the literal.

from - the reason to propagate that literal, else null

Returns:

true if the asignment can be made, false if a conflict is detected.

analyze

public int analyze(Constr confl,
                   Handle<Constr> outLearntRef)

setSimplifier

public void setSimplifier(org.sat4j.minisat.core.Solver.ISimplifier simp)

decode2dimacs

public static int decode2dimacs(int p)

decode the internal representation of a literal into Dimacs format.

Parameters:

p - the literal in internal representation

Returns:

the literal in dimacs representation

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

model

public boolean model(int var)

Description copied from interface: IProblem

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 IProblem

Parameters:

var - the variable id in Dimacs format

Returns:

the truth value of that variable in the model

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(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

getStats

public SolverStats getStats()

getOrder

public IOrder getOrder()

setOrder

public void setOrder(IOrder h)

getVocabulary

public ILits getVocabulary()

reset

public void reset()

Description copied from interface: ISolver

Clean up the internal state of the solver.

Specified by:

reset in interface ISolver

nVars

public int nVars()

Description copied from interface: IProblem

To know the number of variables used in the solver.

Specified by:

nVars in interface IProblem

Returns:

the number of variables created using newVar().

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(java.io.PrintStream out,
                      java.lang.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(java.io.PrintWriter out,
                      java.lang.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 java.lang.String toString(java.lang.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 java.lang.String toString()

Overrides:

toString in class java.lang.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 second)

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.

Specified by:

setExpectedNumberOfClauses in interface ISolver

Parameters:

nb - the expected number of clauses.

getStat

public java.util.Map<java.lang.String,java.lang.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.