| Class | Description |
|---|---|
| LingelingSolver |
A wrapper for the Lingeling SAT solver
(tested with Lingeling version ats1 ce8c04fc97ef07cf279c0c5dcbbc7c5d9904230a).
|
| MarcoMusEnumerator |
Implements a MUs enumerator based on MARCO (http://sun.iwu.edu/~mliffito/marco/).
|
| MimusMusEnumerator |
Implements a MUs enumerator based on MIMUS (http://www.cs.qub.ac.uk/~kmcareavey01/mimus.html).
|
| PlMusEnumerator |
This abstract class models a MUS enumerator for propositional logic, i.e.
|
| Sat4jSolver |
Uses the Sat4j library for SAT solving (note that currently only the light version is used).
|
| SatSolver |
Abstract class for specifying SAT solvers.
|