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

Class SimpleSatSolverState

  • All Implemented Interfaces:
    java.lang.AutoCloseable, SatSolverState
    public final class SimpleSatSolverState
extends java.lang.Object
implements SatSolverState
    A dummy state that can be used in combination with non-incremental Sat-Solvers and SimpleIncrementalSatSolver at positions where a SatSolverState is required.

    Maintains an internal collection of disjunctions.

    Author:
    Mathias Hofer

    • Method Summary

      Modifier and Type Method Description
      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 SatSolverState.satisfiable().
      void close()  
      Interpretation<PlBeliefSet,​PlFormula> witness()
      Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.

      • Methods inherited from class java.lang.Object

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

    • Constructor Detail

      • SimpleSatSolverState

        public SimpleSatSolverState​(SatSolver solver)
        Parameters:
        solver - the solver to use

    • Method Detail

      • close

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

      • add

        public boolean add​(Disjunction clause)
        Description copied from interface: SatSolverState
        Adds the given clause to the solver state.
        Specified by:
        add in interface SatSolverState
        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

        public boolean add​(java.util.Collection<Disjunction> clauses)
        Description copied from interface: SatSolverState
        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.

        Specified by:
        add in interface SatSolverState
        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