org.metacsp.booleanSAT

Class BooleanSatisfiabilitySolver

java.lang.Object

org.metacsp.framework.ConstraintSolver

org.metacsp.booleanSAT.BooleanSatisfiabilitySolver

All Implemented Interfaces:

java.io.Serializable

public class BooleanSatisfiabilitySolver
extends ConstraintSolver

The BooleanSatisfiabilitySolver provides a means to reason upon Boolean Satisfiability constraint problems. It is based on the off the shelf SAT4J solver, available at www.sat4j.org. The solver's variables are BooleanVariables, which can be bound by BooleanConstraints. The latter are disjunctive Boolean clauses, thus the collection of all BooleanConstraints in a ConstraintNetwork represents a well-formed-formula (wff) in Conjunctive Normal Form (CNF). Note that BooleanConstraints can be instantiated with a factory method from non-CNF formulas (see BooleanConstraint.createBooleanConstraints(BooleanVariable[], String).

Author:

Federico Pecora

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class org.metacsp.framework.ConstraintSolver

ConstraintSolver.OPTIONS

Field Summary

Fields

Modifier and Type	Field and Description
protected int	BVIDs
static int	MAX_SAT_CLAUSES
static int	MAX_SAT_VARS

Fields inherited from class org.metacsp.framework.ConstraintSolver

autoprop, components, constraintTypes, IDs, logger, name, nesting, noPropOnVarCreation, numcalls, skipPropagation, spacing, theNetwork, variableType

Constructor Summary

Constructors

Constructor and Description
BooleanSatisfiabilitySolver() Create a new BooleanSatisfiabilitySolver that will accept at most MAX_SAT_VARS BooleanVariables and MAX_SAT_CLAUSES BooleanConstraints.
BooleanSatisfiabilitySolver(int maxVars, int maxClauses) Create a new BooleanSatisfiabilitySolver.
BooleanSatisfiabilitySolver(int maxVars, int maxClauses, boolean propagateOnVarCreation) Create a new BooleanSatisfiabilitySolver.

Method Summary

Modifier and Type	Method and Description
protected boolean	addConstraintsSub(Constraint[] c) This method must be implemented by the developer of the specific ConstraintSolver class.
protected BooleanVariable[]	createVariablesSub(int num) This method must be implemented by the developer of the specific ConstraintSolver class.
boolean	enumeratesModels() Returns whether this BooleanSatisfiabilitySolver enumerates models.
boolean	propagate() Propagate the constraint network.
void	registerValueChoiceFunctions()
protected void	removeConstraintsSub(Constraint[] c) This method must be implemented by the developer of the specific ConstraintSolver class.
protected void	removeVariablesSub(Variable[] v) This method must be implemented by the developer of the specific ConstraintSolver class.
void	setEnumerateModels(boolean enumerateModels) Sets whether this BooleanSatisfiabilitySolver should enumerate models or not.

Methods inherited from class org.metacsp.framework.ConstraintSolver

addConstraint, addConstraintNoPropagation, addConstraints, addConstraintsDebug, addConstraintsNoPropagation, containsVariable, createVariable, createVariable, createVariables, createVariables, createVariablesSub, deplenish, getComponent, getComponents, getConstraintNetwork, getConstraints, getConstraints, getDescription, getID, getOption, getVariable, getVariables, getVariables, getVariables, isCompatible, maskConstraints, removeConstraint, removeConstraints, removeVariable, removeVariables, setComponent, setComponents, setConstraintNetwork, setName, setOptions, toString, unmaskConstraints

Methods inherited from class java.lang.Object

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

Field Detail

MAX_SAT_VARS

public static final int MAX_SAT_VARS

See Also:

Constant Field Values

MAX_SAT_CLAUSES

public static final int MAX_SAT_CLAUSES

See Also:

Constant Field Values

BVIDs

protected int BVIDs

Constructor Detail

BooleanSatisfiabilitySolver

public BooleanSatisfiabilitySolver()

Create a new BooleanSatisfiabilitySolver that will accept at most MAX_SAT_VARS BooleanVariables and MAX_SAT_CLAUSES BooleanConstraints.

BooleanSatisfiabilitySolver

public BooleanSatisfiabilitySolver(int maxVars,
                                   int maxClauses)

Create a new BooleanSatisfiabilitySolver. This solver will accept at most maxVars BooleanVariables and maxClauses BooleanConstraints.

Parameters:

maxVars -

maxClauses -

BooleanSatisfiabilitySolver

public BooleanSatisfiabilitySolver(int maxVars,
                                   int maxClauses,
                                   boolean propagateOnVarCreation)

Create a new BooleanSatisfiabilitySolver. This solver will accept at most maxVars BooleanVariables and maxClauses BooleanConstraints.

Parameters:

maxVars -

maxClauses -

Method Detail

setEnumerateModels

public void setEnumerateModels(boolean enumerateModels)

Sets whether this BooleanSatisfiabilitySolver should enumerate models or not.

Parameters:

enumerateModels - Whether this BooleanSatisfiabilitySolver should enumerate models or not.

enumeratesModels

public boolean enumeratesModels()

Returns whether this BooleanSatisfiabilitySolver enumerates models.

Returns:

true iff this BooleanSatisfiabilitySolver enumerates models.

propagate

public boolean propagate()

Description copied from class: ConstraintSolver

Propagate the constraint network.

Specified by:

propagate in class ConstraintSolver

Returns:

A boolean value indicating whether propagation was successful.

addConstraintsSub

protected boolean addConstraintsSub(Constraint[] c)

Description copied from class: ConstraintSolver

This method must be implemented by the developer of the specific ConstraintSolver class. It should implement all operations necessary to add multiple constraints, and should return true upon success, false otherwise.

Specified by:

addConstraintsSub in class ConstraintSolver

Parameters:

c - The constraints to add.

Returns:

true iff the constraints were added to the ConstraintNetwork.

removeConstraintsSub

protected void removeConstraintsSub(Constraint[] c)

Description copied from class: ConstraintSolver

This method must be implemented by the developer of the specific ConstraintSolver class. Should implement all operations necessary to remove a batch of constraints.

Specified by:

removeConstraintsSub in class ConstraintSolver

Parameters:

c - The constraints to remove.

createVariablesSub

protected BooleanVariable[] createVariablesSub(int num)

Description copied from class: ConstraintSolver

This method must be implemented by the developer of the specific ConstraintSolver class. It should implement all operations necessary to create a batch of variable for the specific type of ConstraintSolver.

Specified by:

createVariablesSub in class ConstraintSolver

Parameters:

num - The number of variables to create.

Returns:

A batch of new Variable for this ConstraintSolver.

removeVariablesSub

protected void removeVariablesSub(Variable[] v)

Description copied from class: ConstraintSolver

This method must be implemented by the developer of the specific ConstraintSolver class. It should implement all operations necessary to remove a batch of variables for the specific type of ConstraintSolver.

Specified by:

removeVariablesSub in class ConstraintSolver

Parameters:

v - The Variables to remove.

registerValueChoiceFunctions

public void registerValueChoiceFunctions()

Specified by:

registerValueChoiceFunctions in class ConstraintSolver