Package org.tweetyproject.arg.adf.sat

Interface SatSolverState

All Superinterfaces:

AutoCloseable

All Known Implementing Classes:

AsynchronousCloseSatSolverState, SynchronizedSatSolverState

public interface SatSolverState
extends 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(Literal literal)	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.
Set<Literal>	witness()	Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.
Set<Literal>	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

Set<Literal> 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

Set<Literal> witness(Collection<? extends Literal> filter)

Parameters:

filter - filter

Returns:

Set

assume

void assume(Literal literal)

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:

literal - the atom for which we assume a value

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 AutoCloseable