Class PicosatSatSolver

java.lang.Object
org.tweetyproject.sat.picosat.PicosatSatSolver
All Implemented Interfaces:
AutoCloseable, SatSolver
public final class PicosatSatSolver extends Object implements SatSolver
This class provides an implementation of the `SatSolver` interface using the PicoSAT SAT solver. PicoSAT is a popular and efficient solver for boolean satisfiability problems.

The class manages interactions with the native PicoSAT solver via bindings, allowing for the creation of variables, addition of clauses, and checking of satisfiability.

  • Constructor Summary

    Constructors
    Constructor
    Description
    PicosatSatSolver()
    Initializes a new instance of the PicoSAT SAT solver.

  • 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.
    boolean
    satisfiable(int[] assumptions)
    Checks if the formula is satisfiable under the given assumptions.
    boolean[]
    witness(int[] literals, int[] assumptions)
    Returns the truth assignment of the given variables under the specified assumptions.

    Methods inherited from class java.lang.Object

    equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

    Methods inherited from interface org.tweetyproject.sat.SatSolver

    satisfiable, witness

  • Constructor Details

    • PicosatSatSolver

      public PicosatSatSolver()
      Initializes a new instance of the PicoSAT SAT solver.

      This constructor initializes the PicoSAT solver instance by calling the native `init` method through the `Binding` class. The handle to the PicoSAT instance is stored in the `handle` field, and the variable index is initialized to `1`.

  • Method Details

    • satisfiable

      public boolean satisfiable(int[] assumptions)
      Description copied from interface: SatSolver
      Checks if the formula is satisfiable under the given assumptions.
      Specified by:
      satisfiable in interface SatSolver
      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

      public boolean[] witness(int[] literals, int[] assumptions)
      Description copied from interface: SatSolver
      Returns the truth assignment of the given variables under the specified assumptions.
      Specified by:
      witness in interface SatSolver
      Parameters:
      literals - 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

      public void add(int[] clause)
      Description copied from interface: SatSolver
      Adds the given clause to the SAT solver state.

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

      Specified by:
      add in interface SatSolver
      Parameters:
      clause - the clause to add

    • newVar

      public int newVar()
      Description copied from interface: SatSolver
      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.

      Specified by:
      newVar in interface SatSolver
      Returns:
      the integer representation

    • close

      public void close()
      Specified by:
      close in interface AutoCloseable
      Specified by:
      close in interface SatSolver