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