Package org.tweetyproject.arg.adf.sat

Interface SatSolverState

All Superinterfaces:
AutoCloseable
All Known Implementing Classes:
AsynchronousCloseSatSolverState, SynchronizedSatSolverState
public interface SatSolverState extends AutoCloseable
A high level representation of a sat solver state.

There are no restrictions on how a state should interact with its corresponding sat-solver. Which means that add calls must not immediately result in calls to the underlying sat solver. This allows the implementation of mechanisms like caching.

Author:
Mathias Hofer

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    add(Clause clause)
    Adds the given clause to the solver state.
    void
    assume(Literal literal)
    Assumes the truth value of the given proposition for the next call to satisfiable().
    void
    close()
     
    boolean
    satisfiable()
    Computes if the current state is satisfiable.
    Set<Literal>
    witness()
    Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.
    Set<Literal>
    witness(Collection<? extends Literal> filter)
     

  • Method Details

    • satisfiable

      boolean satisfiable()
      Computes if the current state is satisfiable. Also takes made assumptions into account.

      Note that it is up to the implementation if the current satisfiability status is cached or if it is computed for every call.

      Returns:
      true if the state is satisfiable, false if it is not

    • witness

      Set<Literal> witness()
      Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.
      Returns:
      a witness if the state is sat, else returns null

    • witness

      Set<Literal> witness(Collection<? extends Literal> filter)
      Parameters:
      filter - filter
      Returns:
      Set

    • assume

      void assume(Literal literal)
      Assumes the truth value of the given proposition for the next call to satisfiable(). There can be multiple assumptions, all of them are gone after the next satisfiable() call.
      Parameters:
      literal - the atom for which we assume a value

    • add

      boolean add(Clause clause)
      Adds the given clause to the solver state.
      Parameters:
      clause - a clause containing only literals - no constants!
      Returns:
      true if the clause could be added to the state, false if it failed

    • close

      void close()
      Specified by:
      close in interface AutoCloseable