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