Table of Contents

Class Clause<T>

Namespace
NanoByte.SatSolver
Assembly
NanoByte.SatSolver.dll

A Boolean Clause. Consists of a set of Literal<T>s of which at least one must be true.

public class Clause<T> : HashSet<Literal<T>>, ISerializable, IDeserializationCallback, ISet<Literal<T>>, ICollection<Literal<T>>, IEnumerable<Literal<T>>, IEnumerable, IEquatable<Clause<T>> where T : IEquatable<T>

Type Parameters

T

The underlying type used to identify/compare Literals.

Inheritance
Clause<T>
Implements
Inherited Members

Constructors

Clause()

Creates an empty Clause.

public Clause()

Clause(IEnumerable<Literal<T>>)

Creates a Clause consisting the specified literals.

public Clause(IEnumerable<Literal<T>> literals)

Parameters

literals IEnumerable<Literal<T>>

Properties

IsEmpty

Indicates whether this Clause is empty and therefore unsatisfiable.

public bool IsEmpty { get; }

Property Value

bool

IsUnit

Indicates whether this is a Unit Clause, i.e. contains exactly one Literal.

public bool IsUnit { get; }

Property Value

bool

Methods

Equals(Clause<T>?)

Indicates whether the current object is equal to another object of the same type.

public bool Equals(Clause<T>? other)

Parameters

other Clause<T>

An object to compare with this object.

Returns

bool

true if the current object is equal to the other parameter; otherwise, false.

Equals(object?)

Determines whether the specified object is equal to the current object.

public override bool Equals(object? obj)

Parameters

obj object

The object to compare with the current object.

Returns

bool

true if the specified object is equal to the current object; otherwise, false.

GetHashCode()

Serves as a hash function for a particular type.

public override int GetHashCode()

Returns

int

A hash code for the current object.

ToString()

Returns a string that represents the current object.

public override string ToString()

Returns

string

A string that represents the current object.

Without(Literal<T>)

Returns a negated copy of this Clause without the specified literal.

public Clause<T> Without(Literal<T> literal)

Parameters

literal Literal<T>

Returns

Clause<T>

Operators

operator &(Clause<T>, Clause<T>)

Creates a Formula<T> consisting of two Clause<T>s.

public static Formula<T> operator &(Clause<T> clause1, Clause<T> clause2)

Parameters

clause1 Clause<T>

The first Clause.

clause2 Clause<T>

The second Clause.

Returns

Formula<T>

operator |(Clause<T>, Literal<T>)

Creates a Clause<T> consisting of all Literals from an existing Clause plus an additional Literal<T>.

public static Clause<T> operator |(Clause<T> clause, Literal<T> literal)

Parameters

clause Clause<T>

The existing Clause.

literal Literal<T>

The additional Literal.

Returns

Clause<T>

operator |(Literal<T>, Clause<T>)

Creates a Clause<T> consisting of all Literals from an existing Clause plus an additional Literal<T>.

public static Clause<T> operator |(Literal<T> literal, Clause<T> clause)

Parameters

literal Literal<T>

The additional Literal.

clause Clause<T>

The existing Clause.

Returns

Clause<T>