Package net.sf.tweety.arg.adf.sat

Interface SatSolverState

  • All Superinterfaces:
    java.lang.AutoCloseable
    All Known Implementing Classes:
    AsynchronousCloseSatSolverState, AsynchronousSatSolverState, SimpleSatSolverState
    public interface SatSolverState
extends java.lang.AutoCloseable
    A high level representation of a sat solver state. This is especially useful for incremental sat-solvers, since we do not want to perform sat computations from scratch for every minor modification on some instance.

    Note that this interface is meant to be used in high-performance contexts. Therefore, the overhead should be kept as low as possible, which means that no additional preprocessing is performed by its methods.

    Hence, the following must hold for add(Collection) and add(Disjunction)

    • The disjunctions must be flat
    • The disjunctions contain literals only
    • The disjunctions do not contain any constants, i.e. Contradiction or Tautology

    In other words, methods of this interface do not perform any CNF transformations or preprocessing on the input.

    There are however no restrictions on how a state should interact with its corresponding sat-solver. Which means that add calls must not be directly translated into calls to the sat-solver, which allows the implementation of mechanisms like caching.

    Author:
    Mathias Hofer

    • Method Summary

      Modifier and Type Method Description
      default boolean add​(java.util.Collection<Disjunction> clauses)
      Adds the given set of clauses to the solver state.
      boolean add​(Disjunction clause)
      Adds the given clause to the solver state.
      void assume​(Proposition proposition, boolean value)
      Assumes the truth value of the given proposition for the next call to satisfiable().
      void close()  
      default boolean satisfiable()
      Computes if the current state is satisfiable.
      Interpretation<PlBeliefSet,​PlFormula> witness()
      Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.

    • Method Detail

      • satisfiable

        default 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

        Interpretation<PlBeliefSet,​PlFormula> 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

      • assume

        void assume​(Proposition proposition,
            boolean value)
        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:
        proposition - the proposition for which we assume a value
        value - the value we assume

      • add

        boolean add​(Disjunction 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

      • add

        default boolean add​(java.util.Collection<Disjunction> clauses)
        Adds the given set of clauses to the solver state.

        If one of the clauses cannot be added, the rest of the clauses may or may not be added. Hence, there is no guarantee that this method tries to add the remaining clauses after the first fail. If this method however returns true, then all of the given clauses were successfully added to the state.

        Parameters:
        clauses - a set of clauses
        Returns:
        true if all of the clauses could be added to the state, false if at least one clause failed

      • close

        void close()
        Specified by:
        close in interface java.lang.AutoCloseable