org.metacsp.booleanSAT

Class BooleanConstraint

java.lang.Object

org.metacsp.framework.Constraint

org.metacsp.booleanSAT.BooleanConstraint

All Implemented Interfaces:

java.io.Serializable, java.lang.Cloneable

public class BooleanConstraint
extends Constraint

Class for representing disjunctive Boolean clauses, e.g., (x1 v x2 v ~x3). Note that BooleanConstraints can be instantiated with a factory method from non-CNF formulas (see createBooleanConstraints(BooleanVariable[], String).

Author:

Federico Pecora

See Also:

Serialized Form

Field Summary

Fields inherited from class org.metacsp.framework.Constraint

annotation, autoRemovable, color, id, logger, masked, numIDs, scope

Constructor Summary

Constructors

Constructor and Description
BooleanConstraint(BooleanVariable[] scope, boolean[] positive) Create a BooleanConstraint given its scope and a specification of the polarity of literals.

Method Summary

Modifier and Type	Method and Description
java.lang.Object	clone()
static BooleanConstraint[]	createBooleanConstraints(BooleanVariable[] scope, java.lang.String wff) A factory method for creating BooleanConstraints from an arbitrary propositional logic formula (wff).
java.lang.String	getEdgeLabel() Every Constraint should implement this method - its value is what is drawn by the ConstraintNetwork rendering methods.
org.sat4j.core.VecInt	getLiterals()
boolean	isEquivalent(Constraint c) Method for assessing the "equivalence" between two constraints.
java.lang.String	toString() Every Constraint should implement a toString method (used by the ConstraintNetwork rendering methods).

Methods inherited from class org.metacsp.framework.Constraint

getAnnotation, getColor, getDescription, getID, getScope, isAutoRemovable, isMasked, isSkippableSolver, isUnary, mask, setAnnotation, setAutoRemovable, setColor, setScope, skipSolver, unmask

Methods inherited from class java.lang.Object

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

Constructor Detail

BooleanConstraint

public BooleanConstraint(BooleanVariable[] scope,
                         boolean[] positive)

Create a BooleanConstraint given its scope and a specification of the polarity of literals.

Parameters:

scope - The scope of the clause.

positive - Polarity of literals.

Method Detail

createBooleanConstraints

public static BooleanConstraint[] createBooleanConstraints(BooleanVariable[] scope,
                                                           java.lang.String wff)

A factory method for creating BooleanConstraints from an arbitrary propositional logic formula (wff). Allowed connectives are ^ (and), v (or), ~ (not), -> (implies), <-> (iff)}. Atoms in the formula should be named "xN" where x is in [a-z] and N is in {1..scope.length}. The signature of the formula must contain all and only the variables in the scope. The conversion to CNF is provided by the propositional logic CNFTransformer class of the aima-java library (see aima-java.googlecode.com).
Note: the given wff must be composed of binary clauses (i.e., all parantheses must be made explicit). For example, the following wff
(x1 ^ x2) ^ (x2 v ~x3 ^ x4) ^ (~x1 v x3) ^ (x2 v ~x3 ^ ~x4)
must be input as
((((x1 ^ x2) ^ (x2 v (~x3 ^ x4))) ^ (~x1 v x3)) ^ (x2 v (~x3 ^ ~x4)))
or as
(((x1 ^ x2) ^ (x2 v (~x3 ^ x4))) ^ ((~x1 v x3) ^ (x2 v (~x3 ^ ~x4))))

Parameters:

scope - The BooleanVariables referred to in the formula.

wff - An arbitrary propositional logic formula.

Returns:

One or more BooleanConstraints representing the given formula in CNF.

getLiterals

public org.sat4j.core.VecInt getLiterals()

toString

public java.lang.String toString()

Description copied from class: Constraint

Every Constraint should implement a toString method (used by the ConstraintNetwork rendering methods).

Specified by:

toString in class Constraint

Returns:

the String representation of this Constraint.

getEdgeLabel

public java.lang.String getEdgeLabel()

Description copied from class: Constraint

Every Constraint should implement this method - its value is what is drawn by the ConstraintNetwork rendering methods.

Specified by:

getEdgeLabel in class Constraint

Returns:

a String representation of the constraint to be used for ConstraintNetwork rendering.

clone

public java.lang.Object clone()

Specified by:

clone in class Constraint

isEquivalent

public boolean isEquivalent(Constraint c)

Description copied from class: Constraint

Method for assessing the "equivalence" between two constraints. This is not used for lookups nor comparisons (hence, it is not the equals method).

Specified by:

isEquivalent in class Constraint

Parameters:

c - The Constraint to compare against.

Returns:

true iff the two constraints are considered to be equivalent.