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()
     
    boolean
    satisfiable(int[] assumptions)
     
    default boolean[]
    witness(int[] variables)
    Returns the truth assignment of the given variables.
    boolean[]
    witness(int[] variables, int[] assumptions)
     

  • Method Details

    • satisfiable

      default boolean satisfiable()

    • satisfiable

      boolean satisfiable(int[] assumptions)

    • witness

      default boolean[] witness(int[] variables)
      Returns the truth assignment of the given variables.
      Parameters:
      variables -
      Returns:
      the truth assignment of the given variables.

    • witness

      boolean[] witness(int[] variables, int[] 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:

    • close

      void close()
      Specified by:
      close in interface AutoCloseable