Class Formula<T>

Namespace

NanoByte.SatSolver

Assembly

NanoByte.SatSolver.dll

A Boolean Formula. Consists of a set of Clause<T>s which all must be true.

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

Type Parameters

T

The underlying type used to identify/compare Literals.

Inheritance

object

HashSet<Clause<T>>

Formula<T>

Implements

ISerializable

IDeserializationCallback

ISet<Clause<T>>

ICollection<Clause<T>>

IEnumerable<Clause<T>>

IEnumerable

IEquatable<Formula<T>>

Inherited Members

HashSet<Clause<T>>.Clear()

HashSet<Clause<T>>.Contains(Clause<T>)

HashSet<Clause<T>>.CopyTo(Clause<T>[], int)

HashSet<Clause<T>>.Remove(Clause<T>)

HashSet<Clause<T>>.GetEnumerator()

HashSet<Clause<T>>.GetObjectData(SerializationInfo, StreamingContext)

HashSet<Clause<T>>.OnDeserialization(object)

HashSet<Clause<T>>.Add(Clause<T>)

HashSet<Clause<T>>.UnionWith(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.IntersectWith(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.ExceptWith(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.SymmetricExceptWith(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.IsSubsetOf(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.IsProperSubsetOf(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.IsSupersetOf(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.IsProperSupersetOf(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.Overlaps(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.SetEquals(IEnumerable<Clause<T>>)

HashSet<Clause<T>>.CopyTo(Clause<T>[])

HashSet<Clause<T>>.CopyTo(Clause<T>[], int, int)

HashSet<Clause<T>>.RemoveWhere(Predicate<Clause<T>>)

HashSet<Clause<T>>.TrimExcess()

HashSet<Clause<T>>.CreateSetComparer()

HashSet<Clause<T>>.Count

HashSet<Clause<T>>.Comparer

object.Equals(object, object)

object.ReferenceEquals(object, object)

object.GetType()

object.MemberwiseClone()

Constructors

Formula()

Creates an empty Formula.

public Formula()

Formula(IEnumerable<Clause<T>>)

Creates a Formula consisting the specified clauses.

public Formula(IEnumerable<Clause<T>> clauses)

Parameters

clauses IEnumerable<Clause<T>>

Properties

ContainsEmptyClause

Indicates whether this Formula contains any empty Clauses and is therefore unsatisfiable.

public bool ContainsEmptyClause { get; }

Property Value

bool

IsConsistent

Indicates whether this Formula is a consistent set of Literals, i.e. consists only non-conflicting Unit Clauses.

public bool IsConsistent { get; }

Property Value

bool

Methods

Equals(Formula<T>?)

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

public bool Equals(Formula<T>? other)

Parameters

other Formula<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.

GetLiterals()

Returns a set of all Literal<T>s referenced in the Formula.

public IEnumerable<Literal<T>> GetLiterals()

Returns

IEnumerable<Literal<T>>

GetPureLiterals()

Returns a set of all Literal<T>s referenced in the Formula that are pure, i.e. do not occur both negated and non-negated.

public IEnumerable<Literal<T>> GetPureLiterals()

Returns

IEnumerable<Literal<T>>

Simplify()

Returns a simplified copy of the Formula. This applies Unit propagation and Pure Literal elimination.

public Formula<T> Simplify()

Returns

Formula<T>

ToString()

Returns a string that represents the current object.

public override string ToString()

Returns

string

A string that represents the current object.

Operators

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

Creates a Formula<T> consisting of all Clauses from an existing Formula plus an additional Clause<T>.

public static Formula<T> operator &(Clause<T> clause, Formula<T> formula)

Parameters

clause Clause<T>

The additional Clause.

formula Formula<T>

The existing Formula.

Returns

Formula<T>

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

Creates a Formula<T> consisting of all Clauses from an existing Formula plus an additional Clause<T>.

public static Formula<T> operator &(Formula<T> formula, Clause<T> clause)

Parameters

formula Formula<T>

The existing Formula.

clause Clause<T>

The additional Clause.

Returns

Formula<T>