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 final 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

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, 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
  - SimpleIncrementalSatSolver
```
public SimpleIncrementalSatSolver(SatSolver delegate)
```
    Parameters:
    
    delegate - the solver to delegate to
- 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>
    
    Overrides:
    
    getWitness in class IncrementalSatSolver
    
    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.
    
    Overrides:
    
    isSatisfiable in class IncrementalSatSolver
    
    Parameters:
    
    formulas - a set of formulas.
    
    Returns:
    
    "true" if the set is consistent.