Package eu.bandm.tools.dpll

Class SAT.Clause<P>

java.lang.Object

java.util.AbstractCollection<SAT.Literal<? extends P>>

eu.bandm.tools.dpll.SAT.Clause<P>

All Implemented Interfaces:

Iterable<SAT.Literal<? extends P>>, Collection<SAT.Literal<? extends P>>

Enclosing class:

SAT<P>

protected abstract static class SAT.Clause<P>
extends AbstractCollection<SAT.Literal<? extends P>>

Disjunction of literals.

Literals are accessible via the unmodifiable collection interface.

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	Clause()

Method Summary

Modifier and Type	Method	Description
abstract @Opt SAT.Literal<? extends P>	getUnit()	Extract unit literal.
abstract boolean	isFalse()	Check whether this clause is unsatisfiable.
abstract boolean	isTrue()	Check whether this clause is tautological.
abstract boolean	isUnit()	Check whether this clause is unitary.
(package private) static <P> SAT.Clause<P>	or(SAT.Literal<? extends P>... lits)
(package private) static <P> SAT.Clause<P>	or(SAT.Literal<? extends P> first, SAT.Clause<P> rest)
(package private) abstract SAT.Clause<P>	propagate(SAT.Literal<? extends P> lit)
int	score()

Methods inherited from class java.util.AbstractCollection

add, addAll, clear, contains, containsAll, isEmpty, iterator, remove, removeAll, retainAll, size, toArray, toArray, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface java.util.Collection

equals, hashCode, parallelStream, removeIf, spliterator, stream, toArray

Methods inherited from interface java.lang.Iterable

forEach

Constructor Details

Clause

protected Clause()

Method Details

isTrue

public abstract boolean isTrue()

Check whether this clause is tautological.

Returns:

true if this clause is true under all interpretations; false otherwise.

isFalse

public abstract boolean isFalse()

Check whether this clause is unsatisfiable.

Returns:

true if this clause is false under all interpretations; false otherwise.

isUnit

public abstract boolean isUnit()

Check whether this clause is unitary.

Returns:

true if this clause contains exactly one literal; false otherwise.

getUnit

@Opt
public abstract @Opt SAT.Literal<? extends P> getUnit()

Extract unit literal.

Returns:

if this clause contains exactly one literal, it is returned; null otherwise.

score

public int score()

propagate

abstract SAT.Clause<P> propagate(SAT.Literal<? extends P> lit)

or

static <P> SAT.Clause<P> or(SAT.Literal<? extends P> first,
 SAT.Clause<P> rest)

or

@SafeVarargs
static <P> SAT.Clause<P> or(SAT.Literal<? extends P>... lits)