edu.kit.iti.formal.lights.sat

Class Clause

java.lang.Object

edu.kit.iti.formal.lights.sat.Clause

public class Clause
extends Object

The Class Clause represents DIMACS clauses.

A clause is a list of integers different from 0. A clause is to be interpreted as the disjunction of the literals that are represented by the integer values. In DIMACS, literals are represented by integers. Positive numbers 1,2,... represent the first, second, ... propositional variable. Negative numbers -1,-2, ... represent the negation of the first, second, ... variable. For instance, the formula (¬A ∨ B) ∧ (C ∨ ¬B) can be represented as the two clauses {-1, 2} and {3, -2}.

Creation of clauses

Clauses are immutable objects. After creation, the values of their fields cannot be changed. If you want to add literals to an existing clause, you can use the methods concat(int) which result in new clauses without changing the receiver of the method call.

Constructor Summary

Constructors

Constructor and Description
Clause(int... literals) Instantiates a new clause from a list of literals.

Method Summary

Modifier and Type	Method and Description
Clause	concat(int literal) Get a clause that represents this clause augmented by an additional literal.
static List<Clause>	exactlySetN(int n, int v1, int v2, int v3, int v4) create a list of dimacs clauses to express that exactly n of 4 variables are set to true.
int	getMaxVar() Get the largest index of all literals in the clause.
int[]	toArray() Extract the integer values of this clause into an array.
String	toString() A clause is textually represented as a list in square brackets.

Methods inherited from class java.lang.Object

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

Constructor Detail

Clause

public Clause(int... literals)
       throws IllegalArgumentException

Instantiates a new clause from a list of literals.

Parameters:

literals - a list of zero or more literal integers (different from 0)

Throws:

IllegalArgumentException - iff the list of literals contains the value 0.

Method Detail

concat

public Clause concat(int literal)
              throws IllegalArgumentException

Get a clause that represents this clause augmented by an additional literal. The parameter must not be 0.

Parameters:

literal - the additional literal

Returns:

the clause corresponding to this clause extended by literal.

Throws:

IllegalArgumentException - if the arguments is 0

toString

public String toString()

A clause is textually represented as a list in square brackets.

For example: The expression new Clause(-1,2,2).toString() yields "[-1,2,2]".

Overrides:

toString in class Object

toArray

public int[] toArray()

Extract the integer values of this clause into an array.

For example: The expression Clause.make(-1,2,2).toArray() yields [-1,2,2]. The result is freshly created. You may safely change it.

Returns:

a freshly created array of integers

getMaxVar

public int getMaxVar()

Get the largest index of all literals in the clause.

The index of a literal is the used variable number, i.e. the absolute value.

For example: The expression new Clause(-1,2,2).getMaxVar() yields 2. The expression new Clause(5,-7).getMaxVar() yields 7.

Returns:

the largest index of all literals in the clause. 0 for the empty clause.

exactlySetN

public static List<Clause> exactlySetN(int n,
                                       int v1,
                                       int v2,
                                       int v3,
                                       int v4)

create a list of dimacs clauses to express that exactly n of 4 variables are set to true.

The resulting list is a freshly created list of Clauses.

Parameters:

n - the number of variables that have to be true. 0 <= n <= 4

v1 - a dimacs variable, > 0

v2 - a dimacs variable, > 0

v3 - a dimacs variable, > 0

v4 - a dimacs variable, > 0

Returns:

a freshly created list of Clauses encoding that n-out-of-4 variables are true