org.sat4j.tools
Class DimacsOutputSolver

java.lang.Object
  org.sat4j.tools.AbstractOutputSolver
      org.sat4j.tools.DimacsOutputSolver

All Implemented Interfaces:

Serializable, IProblem, ISolver

public class DimacsOutputSolver
extends AbstractOutputSolver

Solver used to display in a writer the CNF instance in Dimacs format. That solver is useful to produce CNF files to be used by third party solvers.

Author:

leberre

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.tools.AbstractOutputSolver

firstConstr, fixedNbClauses, nbclauses, nbvars

Constructor Summary

DimacsOutputSolver()

DimacsOutputSolver(PrintWriter pw)

Method Summary

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	addExactly(IVecInt literals, int n) Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
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).
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) 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() To know the number of variables used in the solver as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.
boolean	primeImplicant(int p) Check if a given literal is part of the prime implicant computed by the IProblem.primeImplicant() method.
int	realNumberOfVariables() Retrieve the real number of variables used in the solver.
void	registerLiteral(int p) Tell the solver to consider that the literal is in the CNF.
void	reset() Clean up the internal state of the solver.
void	setExpectedNumberOfClauses(int nb) To inform the solver of the expected number of clauses to read.
String	toString(String prefix) Display a textual representation of the solver configuration.

Methods inherited from class org.sat4j.tools.AbstractOutputSolver

addAllClauses, addBlockingClause, clearLearntClauses, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, model, primeImplicant, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, setDBSimplificationAllowed, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, unsatExplanation

Methods inherited from class java.lang.Object

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

Constructor Detail

DimacsOutputSolver

public DimacsOutputSolver()

DimacsOutputSolver

public DimacsOutputSolver(PrintWriter pw)

Method Detail

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.

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

Overrides:

newVar in class AbstractOutputSolver

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

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)

Parameters:

nb - the expected number of clauses.

See Also:

IProblem.newVar(int)

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

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)

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"

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"

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

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.

reset

public void reset()

Description copied from interface: ISolver

Clean up the internal state of the solver.

toString

public String toString(String prefix)

Description copied from interface: ISolver

Display a textual representation of the solver configuration.

Parameters:

prefix - the prefix to use on each line.

Returns:

a textual description of the solver internals.

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

Overrides:

nConstraints in class AbstractOutputSolver

Returns:

the number of constraints added to the solver

nVars

public int nVars()

Description copied from interface: IProblem

To know the number of variables used in the solver as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.

Specified by:

nVars in interface IProblem

Overrides:

nVars in class AbstractOutputSolver

Returns:

the number of variables created using newVar().

See Also:

IProblem.newVar(int)

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.

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

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.

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.

Returns:

the number of variables reserved in the solver.

Since:

2.3.1

See Also:

ISolver.nextFreeVarId(boolean)

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.

Parameters:

p - the literal in Dimacs format that should appear in the model.

Since:

2.3.1

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.

Parameters:

p - a literal in Dimacs format

Returns:

true iff p belongs to IProblem.primeImplicant()

Since:

2.3.2