Class Formula<T>

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

Inheritance
Object
Formula<T>
Implements
Namespace: NanoByte.SatSolver
Assembly: NanoByte.SatSolver.dll
Syntax
public class Formula<T> : HashSet<Clause<T>> where T : IEquatable<T>
Type Parameters
Name Description
T

The underlying type used to identify/compare Literals.

Constructors

Formula()

Creates an empty Formula.

Declaration
public Formula()

Formula(IEnumerable<Clause<T>>)

Creates a Formula consisting the specified clauses.

Declaration
public Formula(IEnumerable<Clause<T>> clauses)
Parameters
Type Name Description
IEnumerable<Clause<T>> clauses

Properties

ContainsEmptyClause

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

Declaration
public bool ContainsEmptyClause { get; }
Property Value
Type Description
Boolean

IsConsistent

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

Declaration
public bool IsConsistent { get; }
Property Value
Type Description
Boolean

Methods

Equals(Formula<T>)

Declaration
public bool Equals(Formula<T> other)
Parameters
Type Name Description
Formula<T> other
Returns
Type Description
Boolean

Equals(Object)

Declaration
public override bool Equals(object obj)
Parameters
Type Name Description
Object obj
Returns
Type Description
Boolean

GetHashCode()

Declaration
public override int GetHashCode()
Returns
Type Description
Int32

GetLiterals()

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

Declaration
public IEnumerable<Literal<T>> GetLiterals()
Returns
Type Description
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.

Declaration
public IEnumerable<Literal<T>> GetPureLiterals()
Returns
Type Description
IEnumerable<Literal<T>>

Simplify()

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

Declaration
public Formula<T> Simplify()
Returns
Type Description
Formula<T>

ToString()

Declaration
public override string ToString()
Returns
Type Description
String

Operators

BitwiseAnd(Clause<T>, Formula<T>)

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

Declaration
public static Formula<T> operator &(Clause<T> clause, Formula<T> formula)
Parameters
Type Name Description
Clause<T> clause

The additional Clause.
Formula<T> formula

The existing Formula.
Returns
Type Description
Formula<T>

BitwiseAnd(Formula<T>, Clause<T>)

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

Declaration
public static Formula<T> operator &(Formula<T> formula, Clause<T> clause)
Parameters
Type Name Description
Formula<T> formula

The existing Formula.
Clause<T> clause

The additional Clause.
Returns
Type Description
Formula<T>

Implements