Package org.tweetyproject.arg.adf.sat
Interface SatSolverState
 All Superinterfaces:
AutoCloseable
 All Known Implementing Classes:
AsynchronousCloseSatSolverState
,SynchronizedSatSolverState
A high level representation of a sat solver state.
There are no restrictions on how a state should interact with its corresponding satsolver. 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 TypeMethodDescriptionboolean
Adds the given clause to the solver state.void
Assumes the truth value of the given proposition for the next call tosatisfiable()
.void
close()
boolean
Computes if the current state is satisfiable.witness()
Returns a witness of the satisfiability of all the clauses in the state, ornull
if the state is unsatisfiable.witness(Collection<? extends Literal> filter)

Method Details

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
Returns a witness of the satisfiability of all the clauses in the state, ornull
if the state is unsatisfiable. Returns:
 a witness if the state is sat, else returns
null

witness

assume
Assumes the truth value of the given proposition for the next call tosatisfiable()
. There can be multiple assumptions, all of them are gone after the nextsatisfiable()
call. Parameters:
literal
 the atom for which we assume a value

add
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 interfaceAutoCloseable
