Package org.tweetyproject.arg.adf.sat

Interface IndexedSatSolverState

All Superinterfaces:

AutoCloseable

public interface IndexedSatSolverState
extends AutoCloseable

The IndexedSatSolverState interface represents a state of a SAT solver with indexed literals. It provides methods for querying satisfiability, retrieving the truth values of literals, and managing clauses within the solver state. This interface extends AutoCloseable to ensure proper resource management.

Author:

Matthias Thimm

Method Summary

Modifier and Type	Method	Description
void	add(int[] clause)	Adds a clause to the current SAT solver state.
void	close()	Closes the SAT solver state and releases any resources associated with it.
boolean	satisfiable()	Checks whether the current SAT solver state is satisfiable with the current set of clauses.
boolean	satisfiable(int[] assumptions)	Checks whether the current SAT solver state is satisfiable given a set of assumptions.
int[]	witness(int[] literals)	Retrieves the truth values of the given literals in the current SAT solver state.
int[]	witness(int[] literals, int[] assumptions)	Retrieves the truth values of the given literals in the current SAT solver state, considering the specified assumptions.

Method Details

satisfiable

boolean satisfiable()

Checks whether the current SAT solver state is satisfiable with the current set of clauses.

Returns:

true if the current state is satisfiable, false otherwise

satisfiable

boolean satisfiable(int[] assumptions)

Checks whether the current SAT solver state is satisfiable given a set of assumptions.

Parameters:

assumptions - an array of literals representing assumptions; literals should be indexed and in the form of positive (true) or negative (false) integers

Returns:

true if the state is satisfiable with the given assumptions, false otherwise

witness

int[] witness(int[] literals)

Retrieves the truth values of the given literals in the current SAT solver state.

The returned array contains values where 0 represents false and 1 represents true.

Parameters:

literals - an array of literals whose truth values are to be retrieved

Returns:

an array of integers where each entry corresponds to the truth value of the given literals (0 for false, 1 for true)

witness

int[] witness(int[] literals,
 int[] assumptions)

Retrieves the truth values of the given literals in the current SAT solver state, considering the specified assumptions.

The returned array contains values where 0 represents false and 1 represents true.

Parameters:

literals - an array of literals whose truth values are to be retrieved

assumptions - an array of literals representing assumptions to be considered during retrieval

Returns:

an array of integers where each entry corresponds to the truth value of the given literals (0 for false, 1 for true), considering the assumptions

add

void add(int[] clause)

Adds a clause to the current SAT solver state. A clause is represented as an array of literals, where each literal is an integer (positive for true, negative for false).

Parameters:

clause - an array of literals representing the clause to be added

close

void close()

Closes the SAT solver state and releases any resources associated with it. This method should be called when the solver state is no longer needed to ensure proper resource management.

Specified by:

close in interface AutoCloseable