SatSolverState

All Superinterfaces:

java.lang.AutoCloseable

All Known Implementing Classes:

NativeLingelingSolver.LingelingSolverState, SimpleSatSolverState
```
public interface SatSolverState
extends java.lang.AutoCloseable
```
A high level representation of a sat solver state. This is especially useful for incremental sat-solvers, since we do not want to perform sat computations from scratch for every minor modification on some instance.
Note that this interface is meant to be used in high-performance contexts. Therefore, the overhead should be kept as low as possible, which means that no additional preprocessing is performed by its methods.
Hence, the following must hold for add(Collection), add(Disjunction) and remove(Disjunction)
- The disjunctions must be flat
- The disjunctions contain literals only
- The disjunctions do not contain any constants, i.e. Contradiction or Tautology
In other words, methods of this interface do not perform any CNF transformations or optimizations on the input.
There are however no restrictions on how a state should interact with its corresponding sat-solver. Which means that add or remove calls must not be directly translated into calls to the sat-solver, which allows the implementation of mechanisms like caching.
Author:

Mathias Hofer

Method Summary

Modifier and Type	Method	Description
`boolean`	`add(java.util.Collection<Disjunction> clauses)`
`boolean`	`add(Disjunction clause)`	Updates the state of the corresponding SAT-Solver by adding a clause.
`void`	`assume(Proposition proposition, boolean value)`
`boolean`	`remove(Disjunction clause)`	Tries to remove the given clause from the sat instance.
`default boolean`	`satisfiable()`
`Interpretation<PlBeliefSet,PlFormula>`	`witness()`

Methods inherited from interface java.lang.AutoCloseable
close

- Method Detail
  - satisfiable
```
default boolean satisfiable()
```
  - witness
```
Interpretation<PlBeliefSet,PlFormula> witness()
```
  - assume
```
void assume(Proposition proposition,
            boolean value)
```
  - add
```
boolean add(Disjunction clause)
```
    Updates the state of the corresponding SAT-Solver by adding a clause.
    
    Parameters:
    
    clause - a clause containing only literals - no constants!
    
    Returns:
    
    true iff the
  - add
```
boolean add(java.util.Collection<Disjunction> clauses)
```
  - remove
```
boolean remove(Disjunction clause)
```
    Tries to remove the given clause from the sat instance.
    
    Parameters:
    
    clause -
    
    Returns:
    
    true iff the removal was successful