NanoByte SAT Solver 0.3.0
DPLL Boolean Satisfiability Solver for .NET
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.
 
 Formula (IEnumerable< Clause< T > > clauses)
 Creates a Formula consisting the specified clauses .
 
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.
 
IEnumerable< Literal< T > > GetLiterals ()
 Returns a set of all Literal<T>s referenced in the Formula.
 
Formula< T > Simplify ()
 Returns a simplified copy of the Formula. This applies Unit propagation and Pure Literal elimination.
 
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...
 

Package Functions

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

Properties

bool ContainsEmptyClause [get]
 Indicates whether this Formula contains any empty Clauses and is therefore unsatisfiable.
 
bool IsConsistent [get]
 Indicates whether this Formula is a consistent set of Literals, i.e. consists only non-conflicting Unit Clauses.
 

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> 

Member Function Documentation

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

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