SatSolverState

All Superinterfaces:

java.lang.AutoCloseable

All Known Implementing Classes:

AsynchronousCloseSatSolverState, AsynchronousSatSolverState
```
public interface SatSolverState
extends java.lang.AutoCloseable
```
A high level representation of a sat solver state.
There are no restrictions on how a state should interact with its corresponding sat-solver. Which means that add calls must not immediately result in calls to the underlying sat solver. This allows the implementation of mechanisms like caching.

Author:

Mathias Hofer

Method Summary

Modifier and Type	Method	Description
`boolean`	`add(Clause clause)`	Adds the given clause to the solver state.
`void`	`assume(Atom atom, boolean value)`	Assumes the truth value of the given proposition for the next call to `satisfiable()`.
`void`	`close()`
`boolean`	`satisfiable()`	Computes if the current state is satisfiable.
`java.util.Set<Atom>`	`witness()`	Returns a witness of the satisfiability of all the clauses in the state, or `null` if the state is unsatisfiable.
`java.util.Set<Atom>`	`witness(java.util.Collection<Atom> filter)`

- Method Detail
  - satisfiable
```
boolean satisfiable()
```
    Computes if the current state is satisfiable. Also takes made assumptions into account.
    Note that it is up to the implementation if the current satisfiability status is cached or if it is computed for every call.
    
    Returns:
    
    true if the state is satisfiable, false if it is not
  - witness
```
java.util.Set<Atom> witness()
```
    Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.
    
    Returns:
    
    a witness if the state is sat, else returns null
  - witness
```
java.util.Set<Atom> witness(java.util.Collection<Atom> filter)
```
  - assume
```
void assume(Atom atom,
            boolean value)
```
    Assumes the truth value of the given proposition for the next call to satisfiable(). There can be multiple assumptions, all of them are gone after the next satisfiable() call.
    
    Parameters:
    
    atom - the atom for which we assume a value
    
    value - the value we assume
  - add
```
boolean add(Clause clause)
```
    Adds the given clause to the solver state.
    
    Parameters:
    
    clause - a clause containing only literals - no constants!
    
    Returns:
    
    true if the clause could be added to the state, false if it failed
  - close
```
void close()
```
    Specified by:
    
    close in interface java.lang.AutoCloseable