NanoByte SAT Solver
Public Member Functions | Static Public Member Functions | Public Attributes | 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...
 

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

◆ 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 & ( 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.

◆ operator &() [2/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.

◆ 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: