Namespace NanoByte.SatSolver
CDCL Boolean Satisfiability Solver.
Classes
- AtMostOneConstraint<T>
A constraint that no more than one of its literals may be true.
- Clause<T>
A Boolean Clause. Consists of a set of Literal<T>s of which at least one must be true.
- Formula<T>
A Boolean Formula. Consists of a set of Clause<T>s which all must be true.
- Literal
Factory methods for Literal<T>s.
- Model<T>
A satisfying assignment for a SatProblem<T>. Variables that were never constrained may be missing.
- SatProblem<T>
A mutable SAT problem builder.
- Solver<T>
A Boolean Satisfiability Solver.
Structs
- Literal<T>
A Boolean Literal.