NanoByte SAT Solver
Public Member Functions | Static Public Member Functions | Public Attributes | Package Functions | Properties | List of all members
NanoByte.SatSolver.Formula< T > Class Template Reference

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

Inheritance diagram for NanoByte.SatSolver.Formula< T >:

Public Member Functions

 Formula ()
 Creates an empty Formula. More...
 
 Formula (IEnumerable< Clause< T >> clauses)
 Creates a Formula consisting the specified clauses . More...
 
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. More...
 
IEnumerable< Literal< T > > GetLiterals ()
 Returns a set of all Literal<T>s referenced in the Formula. More...
 
Formula< T > Simplify ()
 Returns a simplified copy of the Formula. This applies Unit propagation and Pure Literal elimination. More...
 
override string ToString ()
 
bool Equals (Formula< T > other)
 
override bool Equals (object obj)
 
override int GetHashCode ()
 

Static Public Member Functions

static Formula< T > operator& (Formula< T > formula, Clause< T > clause)
 Creates a Formula<T> consisting of all Clauses from an existing Formula plus an additional Clause<T>. More...
 
static Formula< T > operator& (Clause< T > clause, Formula< T > formula)
 Creates a Formula<T> consisting of all Clauses from an existing Formula plus an additional Clause<T>. More...
 

Public Attributes

bool ContainsEmptyClause => this.Any(clause => clause.IsEmpty)
 Indicates whether this Formula contains any empty Clauses and is therefore unsatisfiable. More...
 

Package Functions

Formula< T > PropagateUnits ()
 Returns a copy of the Formula simplified by propagating all Unit Clauses. More...
 
Formula< T > EliminatePureLiterals ()
 Returns a copy of the Formula simplified by remove all Clauses that contain Pure Literals. More...
 

Properties

bool IsConsistent [get]
 Indicates whether this Formula is a consistent set of Literals, i.e. consists only non-conflicting Unit Clauses. More...
 

Detailed Description

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

Template Parameters
TThe underlying type used to identify/compare Literals.
Type Constraints
T :IEquatable<T> 

Constructor & Destructor Documentation

◆ Formula() [1/2]

Creates an empty Formula.

◆ Formula() [2/2]

NanoByte.SatSolver.Formula< T >.Formula ( IEnumerable< Clause< T >>  clauses)
inline

Creates a Formula consisting the specified clauses .

Member Function Documentation

◆ EliminatePureLiterals()

Formula<T> NanoByte.SatSolver.Formula< T >.EliminatePureLiterals ( )
inlinepackage

Returns a copy of the Formula simplified by remove all Clauses that contain Pure Literals.

◆ GetLiterals()

IEnumerable<Literal<T> > NanoByte.SatSolver.Formula< T >.GetLiterals ( )

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

◆ GetPureLiterals()

IEnumerable<Literal<T> > NanoByte.SatSolver.Formula< T >.GetPureLiterals ( )
inline

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.

◆ operator&() [1/2]

static Formula<T> NanoByte.SatSolver.Formula< T >.operator& ( Clause< T >  clause,
Formula< T >  formula 
)
static

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

Parameters
clauseThe additional Clause.
formulaThe existing Formula.

◆ operator&() [2/2]

static Formula<T> NanoByte.SatSolver.Formula< T >.operator& ( Formula< T >  formula,
Clause< T >  clause 
)
static

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

Parameters
formulaThe existing Formula.
clauseThe additional Clause.

◆ PropagateUnits()

Formula<T> NanoByte.SatSolver.Formula< T >.PropagateUnits ( )
package

Returns a copy of the Formula simplified by propagating all Unit Clauses.

◆ Simplify()

Formula<T> NanoByte.SatSolver.Formula< T >.Simplify ( )
inline

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

Member Data Documentation

◆ ContainsEmptyClause

bool NanoByte.SatSolver.Formula< T >.ContainsEmptyClause => this.Any(clause => clause.IsEmpty)

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

Property Documentation

◆ IsConsistent

bool NanoByte.SatSolver.Formula< T >.IsConsistent
get

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


The documentation for this class was generated from the following file: