Package org.tweetyproject.sat

Interface SatSolver

All Superinterfaces:

AutoCloseable

All Known Implementing Classes:

LingelingSatSolver, MinisatSatSolver, PicosatSatSolver

public interface SatSolver
extends AutoCloseable

A minimalistic, low-level and stateful SAT solver interface.

The goal of this interface is to provide a common and overhead-less interface to (usually) native SAT solver implementations. This is mirrored in the design of the methods of this interface. Hence, literals are represented as signed integers analogous to DIMACS format, this usually allows for a direct delegation to some native function, without any intermediate mapping layer. Further consider witness(int[]) for instance, by explicitly stating the propositional variables as a parameter, it is not necessary for the implementation to memorize the used variables, which results in less memory overhead.

Author:

Mathias Hofer

Method Summary

Modifier and Type	Method	Description
void	add(int... clause)	Adds the given clause to the SAT solver state.
void	close()
int	newVar()	Creates and returns the integer representation of a fresh propositional variable.
default boolean	satisfiable()	Checks if the formula is satisfiable without any assumptions.
boolean	satisfiable(int[] assumptions)	Checks if the formula is satisfiable under the given assumptions.
default boolean[]	witness(int[] variables)	Returns the truth assignment of the given variables assuming no assumptions.
boolean[]	witness(int[] variables, int[] assumptions)	Returns the truth assignment of the given variables under the specified assumptions.

Method Details

satisfiable

default boolean satisfiable()

Checks if the formula is satisfiable without any assumptions.

This is a default method that delegates to satisfiable(int[]) with an empty array of assumptions.

Returns:

true if the formula is satisfiable, false otherwise.

satisfiable

boolean satisfiable(int[] assumptions)

Checks if the formula is satisfiable under the given assumptions.

Parameters:

assumptions - an array of literals that are assumed to be true. If the array is empty, no assumptions are made.

Returns:

true if the formula is satisfiable under the assumptions, false otherwise.

witness

default boolean[] witness(int[] variables)

Returns the truth assignment of the given variables assuming no assumptions.

This is a default method that delegates to witness(int[], int[]) with an empty array of assumptions.

Parameters:

variables - an array of variable indices for which the truth assignment is requested.

Returns:

an array of booleans representing the truth assignment of the given variables.

witness

boolean[] witness(int[] variables,
 int[] assumptions)

Returns the truth assignment of the given variables under the specified assumptions.

Parameters:

variables - an array of variable indices for which the truth assignment is requested.

assumptions - an array of literals that are assumed to be true. If the array is empty, no assumptions are made.

Returns:

an array of booleans representing the truth assignment of the given variables under the assumptions.

add

void add(int... clause)

Adds the given clause to the SAT solver state.

Note that contrary to DIMACS format, a trailing '0' is not required!

Parameters:

clause - the clause to add

newVar

int newVar()

Creates and returns the integer representation of a fresh propositional variable.

It is necessary to only use variables returned by this method, since some solvers require to first allocate and maintain a data structure of the variables before they can be used in clauses. Hence, using integers not returned by this method may work for some solvers, but not for others.

Returns:

the integer representation

close

void close()

Specified by:

close in interface AutoCloseable