Package net.sf.tweety.arg.adf.sat

Class AsynchronousSatSolverState

java.lang.Object

net.sf.tweety.arg.adf.sat.AsynchronousSatSolverState

All Implemented Interfaces:

java.lang.AutoCloseable, SatSolverState

public final class AsynchronousSatSolverState
extends java.lang.Object
implements SatSolverState

Executes all operations of the underlying SatSolverState in a (possibly) separate thread, determined by the provided ExecutorService.

Author:

Mathias Hofer

Constructor Summary

Constructors

Constructor	Description
AsynchronousSatSolverState(SatSolverState delegate)
AsynchronousSatSolverState(SatSolverState delegate, java.util.concurrent.ExecutorService executor)

Method Summary

Modifier and Type	Method	Description
boolean	add(java.util.Collection<Disjunction> clauses)	Adds the given set of clauses to the solver state.
boolean	add(Disjunction clause)	Adds the given clause to the solver state.
void	assume(Proposition proposition, boolean value)	Assumes the truth value of the given proposition for the next call to SatSolverState.satisfiable().
void	close()
boolean	satisfiable()	Computes if the current state is satisfiable.
Interpretation<PlBeliefSet,PlFormula>	witness()	Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

AsynchronousSatSolverState

public AsynchronousSatSolverState(SatSolverState delegate)

Parameters:

delegate - the state

AsynchronousSatSolverState

public AsynchronousSatSolverState(SatSolverState delegate,
                                  java.util.concurrent.ExecutorService executor)

Parameters:

delegate - the state

executor - the executor which is used to execute the calls to the delegate state

Method Detail

witness

public Interpretation<PlBeliefSet,PlFormula> witness()

Description copied from interface: SatSolverState

Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.

Specified by:

witness in interface SatSolverState

Returns:

a witness if the state is sat, else returns null

satisfiable

public boolean satisfiable()

Description copied from interface: SatSolverState

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.

Specified by:

satisfiable in interface SatSolverState

Returns:

true if the state is satisfiable, false if it is not

assume

public void assume(Proposition proposition,
                   boolean value)

Description copied from interface: SatSolverState

Assumes the truth value of the given proposition for the next call to SatSolverState.satisfiable(). There can be multiple assumptions, all of them are gone after the next SatSolverState.satisfiable() call.

Specified by:

assume in interface SatSolverState

Parameters:

proposition - the proposition for which we assume a value

value - the value we assume

add

public boolean add(Disjunction clause)

Description copied from interface: SatSolverState

Adds the given clause to the solver state.

Specified by:

add in interface SatSolverState

Parameters:

clause - a clause containing only literals - no constants!

Returns:

true if the clause could be added to the state, false if it failed

add

public boolean add(java.util.Collection<Disjunction> clauses)

Description copied from interface: SatSolverState

Adds the given set of clauses to the solver state.

If one of the clauses cannot be added, the rest of the clauses may or may not be added. Hence, there is no guarantee that this method tries to add the remaining clauses after the first fail. If this method however returns true, then all of the given clauses were successfully added to the state.

Specified by:

add in interface SatSolverState

Parameters:

clauses - a set of clauses

Returns:

true if all of the clauses could be added to the state, false if at least one clause failed

close

public void close()

Specified by:

close in interface java.lang.AutoCloseable

Specified by:

close in interface SatSolverState