IncrementalSatSolver

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

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

Direct Known Subclasses:

NativeLingelingSolver, NativeMinisatSolver, NativePicosatSolver, SimpleIncrementalSatSolver
```
public abstract class IncrementalSatSolver
extends SatSolver
```

Constructor Summary

Constructors
Constructor Description

IncrementalSatSolver()

Method Summary

Modifier and Type	Method	Description
`abstract 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
  - IncrementalSatSolver
```
public IncrementalSatSolver()
```
- Method Detail
  - createState
```
public abstract SatSolverState createState()
```
  - 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.