• Classes
    This class offers a generic wrapper for command line based SAT solvers.
    Implements a MUs enumerator based on MARCO (
    Provides a generic class for implementing MaxSAT solvers, i.e.
    Implements a MUs enumerator based on MIMUS (
    Provides an interface to the open-wbo MaxSAT solver, see
    This abstract class models a MUS enumerator for propositional logic, i.e.
    Uses the Sat4j library for SAT solving (note that currently only the light version is used).
    Abstract class for specifying SAT solvers.
    This class provides a simple reference implementation of the DPLL (Davis–Putnam–Logemann–Loveland) algorithm for satisfiability testing, see e.g