SimpleIncrementalSatSolver

java.lang.Object
- net.sf.tweety.logics.pl.sat.SatSolver
- - net.sf.tweety.arg.adf.sat.IncrementalSatSolver
  - - net.sf.tweety.arg.adf.sat.SimpleIncrementalSatSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
```
public class SimpleIncrementalSatSolver
extends IncrementalSatSolver
```
A simple wrapper which can be used where instances of IncrementalSatSolver are needed.
Note that this implementation only provides a compatibility layer and no real incremental sat solving behavior. Hence, it is highly recommended to use a real incremental sat solver implementation if possible, otherwise one has to expect poor performance.

Author:

Mathias Hofer

Field Summary

Fields
Modifier and Type Field Description

private SatSolver delegate

Constructor Summary

Constructors
Constructor Description

SimpleIncrementalSatSolver(SatSolver delegate)

Method Summary

Modifier and Type	Method	Description
`SatSolverState`	`createState()`
`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, 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

- Field Detail
  - delegate
```
private SatSolver delegate
```
- Constructor Detail
  - SimpleIncrementalSatSolver
```
public SimpleIncrementalSatSolver(SatSolver delegate)
```
    Parameters:
    
    delegate -
- Method Detail
  - createState
```
public SatSolverState createState()
```
    Specified by:
    
    createState in class IncrementalSatSolver
  - 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.