See: Description
| Interface | Description |
|---|---|
| AllSATSolver |
Finds all models of a sentence
|
| ClauseBlocker |
A clause blocker prevents an incremental SAT solver from finding models
having certain properties
|
| CNFConverter |
CNF converter
A standarised interface for converting a sentence to conjunctive normal form
(CNF)
|
| Class | Description |
|---|---|
| AllSAT4j |
Wrapper for using sat4j incremental solver
|
| DefaultModelBlocker |
This class blocks every model found considering only relevant variables
(doesn't block switching variables, therefore getting rid of uninteresting
solutions)
|
| ModelIterator |
Iterates over all models of a sentence
|
| PropositionalModel |
A list of literals used as a representation of a satisfying assignment for a
certain formula
|
| TseitinCNFConverter |
Converts a tree formula to CNF using Tseitin method
|