Package org.tweetyproject.logics.pl.sat

package org.tweetyproject.logics.pl.sat

Classes

Class	Description
CmdLineSatSolver	This class offers a generic wrapper for command line based SAT solvers.
DimacsMaxSatSolver	Generic class for Dimacs-based MaxSAT solvers.
DimacsSatSolver	Interface for SAT solvers which work on the Dimacs format.
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.
SimpleModelEnumerator	enumerates all models naivly