net.sf.tweety.logics.pl.sat

Class SimpleDpllSolver

java.lang.Object

net.sf.tweety.logics.pl.sat.SatSolver

net.sf.tweety.logics.pl.sat.SimpleDpllSolver

All Implemented Interfaces:

net.sf.tweety.logics.commons.analysis.BeliefSetConsistencyTester<PropositionalFormula>, net.sf.tweety.logics.commons.analysis.ConsistencyTester<net.sf.tweety.commons.BeliefSet<PropositionalFormula>>, net.sf.tweety.logics.commons.analysis.ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula>

public class SimpleDpllSolver
extends SatSolver

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. The order of the variables is simply taken by the standard iterator of the induced signature. Only unit propagation is used for satisfiability testing.

Author:

Matthias Thimm

Constructor Summary

Constructors

Constructor and Description
SimpleDpllSolver()

Method Summary

Modifier and Type	Method and Description
net.sf.tweety.commons.Interpretation<PlBeliefSet,PropositionalFormula>	getWitness(Collection<PropositionalFormula> formulas) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
boolean	isSatisfiable(Collection<PropositionalFormula> formulas) Checks whether the given set of formulas is satisfiable.

Methods inherited from class net.sf.tweety.logics.pl.sat.SatSolver

convertToDimacs, convertToDimacs, createTmpDimacsFile, createTmpDimacsFile, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver, setTempFolder

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SimpleDpllSolver

public SimpleDpllSolver()

Method Detail

getWitness

public net.sf.tweety.commons.Interpretation<PlBeliefSet,PropositionalFormula> getWitness(Collection<PropositionalFormula> formulas)

Description copied from class: SatSolver

If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.

Specified by:

getWitness in interface net.sf.tweety.logics.commons.analysis.ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula>

Specified by:

getWitness in class SatSolver

Returns:

some model of the formulas or null.

isSatisfiable

public boolean isSatisfiable(Collection<PropositionalFormula> formulas)

Description copied from class: SatSolver

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class SatSolver

Parameters:

formulas - a set of formulas.

Returns:

"true" if the set is consistent.