Package org.tweetyproject.sat.minisat

Class MinisatSatSolver

java.lang.Object
org.tweetyproject.sat.minisat.MinisatSatSolver
All Implemented Interfaces:
AutoCloseable, SatSolver
public final class MinisatSatSolver extends Object implements SatSolver

  • Constructor Summary

    Constructors
    Constructor
    Description
    MinisatSatSolver()
     

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

    Methods inherited from class java.lang.Object

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

  • Constructor Details

    • MinisatSatSolver

      public MinisatSatSolver()

  • Method Details

    • satisfiable

      public boolean satisfiable()
      Specified by:
      satisfiable in interface SatSolver

    • satisfiable

      public boolean satisfiable(int[] assumptions)
      Specified by:
      satisfiable in interface SatSolver

    • witness

      public boolean[] witness(int[] atoms)
      Description copied from interface: SatSolver
      Returns the truth assignment of the given variables.
      Specified by:
      witness in interface SatSolver
      Returns:
      the truth assignment of the given variables.

    • witness

      public boolean[] witness(int[] atoms, int[] assumptions)
      Specified by:
      witness in interface SatSolver

    • 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:

    • close

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