Package net.sf.tweety.logics.pl.sat

Class Summary

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/).
MaxSatSolver	Provides a generic class for implementing MaxSAT solvers, i.e.
MimusMusEnumerator	Implements a MUs enumerator based on MIMUS (http://www.cs.qub.ac.uk/~kmcareavey01/mimus.html).
OpenWboSolver	Provides an interface to the open-wbo MaxSAT solver, see https://github.com/sat-group/open-wbo.
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.
SimpleDpllSolver	This class provides a simple reference implementation of the DPLL (Davis–Putnam–Logemann–Loveland) algorithm for satisfiability testing, see e.g https://en.wikipedia.org/wiki/DPLL_algorithm.