SimpleDpllSolver

java.lang.Object
- net.sf.tweety.logics.pl.sat.SatSolver
- - net.sf.tweety.logics.pl.sat.SimpleDpllSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
```
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 Description

SimpleDpllSolver()

Method Summary

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

Methods inherited from class net.sf.tweety.logics.pl.sat.SatSolver
convertToDimacs, convertToDimacs, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver, setTempFolder

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Constructor Detail
  - SimpleDpllSolver
```
public SimpleDpllSolver()
```
- Method Detail
  - getWitness
```
public Interpretation<PlBeliefSet,PlFormula> getWitness(java.util.Collection<PlFormula> 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 ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
    
    Specified by:
    
    getWitness in class SatSolver
    
    Parameters:
    
    formulas - a set of formulas
    
    Returns:
    
    some model of the formulas or null.
  - isSatisfiable
```
public boolean isSatisfiable(java.util.Collection<PlFormula> 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.