Package eu.bandm.tools.dpll

Class SATSolver.State<P>

java.lang.Object
eu.bandm.tools.dpll.SATSolver.State<P>
Type Parameters:
P - the type of propositional variables
Enclosing class:
SATSolver<P>
public static class SATSolver.State<P> extends Object
A state of a DPLL-based solution process.

Every state pairs two formulas: An arbitrary formula form in conjunctive normal form that remains to be solved, and a disjunction-free "solution candidate" formula solution that records all committed solution steps. Together, they entail the original goal, which is not retained.

The solution process proceeds by in-place eager heuristics and state transitions where the formula to be solved becomes successively smaller, and terminates in either of two cases:

  • A state is terminal and successful, if the formula to be solved is atomically true; then the solution candidate is an actual solution.
  • A state is terminal and failing, if the formula to be solved is atomically false; then no solution exists, because the original goal is unsatisfiable.

Typical changes to a state by eager heuristics invoke commit(Literal<P>) to add a unit clause to solution and simplify form accordingly. Such changes are guaranteed to be logically sound; if a subclass implements other changes, soundness must be enforced explicitly. The overall outcome of the solution process is unspecified if unsound changes are applied.

Splitting

The solution process may have to split() into branches, where either branch may lead to a solution. The default strategy to explore branches is sequential backtracking; this can be changed by subclasses.

Splitting is effected by making copies of the current state. By contrast, eager heuristics that do not involve a split act by side effect on a state object, and may change the values of form and solution subject to the transition rules stated above.

Entry Point

The main entry point for a solution process is solve(). The state may compute the solution itself if it is already terminal, or becomes terminal due to eager heuristics, or it may delegate to other states.

See Also:

  • Field Details

    • form

      protected Formula<P> form
      The remaining formula to be solved.

    • solution

      protected Formula<P> solution
      The solution candidate that records all committed steps.

  • Constructor Details

    • State

      protected State(Formula<P> form)
      Creates a new state with the given formula and the empty solution candidate.
      Parameters:
      form - the formula to solve

    • State

      protected State(Formula<P> form, Formula<P> solution)
      Creates a new state with the given formula empty solution candidate.
      Parameters:
      form - the formula to solve
      solution - the solution candidate

  • Method Details

    • with

      protected SATSolver.State<P> with(Literal<P> literal)
      Creates a copy of this state with a given unit clause added to the formula.

      Subclasses should override this method to create instances of themselves.

      This implementation invokes new State(Formula, Formula).

      Parameters:
      literal - the literal to add
      Returns:
      a new state where the formula to be solved is augmented by a unit clause of the given literal, and the solution is the same as for this state.

    • choose

      protected Literal<P> choose()
      Chooses a literal to resolve.

      Subclasses may override this method to implement a custom strategy.

      The default strategy chooses the first literal of the first clause, as per form.iterator().next().iterator().next().

      Returns:
      a literal occurring in form
      Throws:
      NoSuchElementException - if form is not a nonempty formula of nonempty clauses

    • solve

      public Formula<P> solve()
      Returns a solution for this state.

      This method first tries to simplify the current state by applying eager heuristics. If this results in the formula to be solved becoming atomic, then the process terminates. Otherwise, the state space is explored by splitting.

      Returns:
      a satisfiable disjunction-free formula that entails the original goal; or a false formula if it is unsatisfiable.
      See Also:

    • split

      protected Formula<P> split()
      Finds a solution by splitting this state.
      Returns:
      a satisfiable disjunction-free formula that entails the original goal; or a false formula if it is unsatisfiable.

    • split

      protected Formula<P> split(SATSolver.State<P> s1, SATSolver.State<P> s2)
      Finds a solution from either of two split states.

      Subclasses may override this method to customize the search strategy.

      The default implementation uses sequential exploration.

      Parameters:
      s1 - the one state to explore
      s2 - the other state to explore
      Returns:
      a satisfiable disjunction-free formula that entails the original goal; or a false formula if it is unsatisfiable.
      See Also:

    • sequential

      protected Formula<P> sequential(SATSolver.State<P> s1, SATSolver.State<P> s2)
      Finds a solution from either of two split states by sequential exploration.

      s1 is tried first. Only if it does not yield a solution s2 is tried also.

      Parameters:
      s1 - the first state to explore
      s2 - the second state to explore
      Returns:
      a satisfiable disjunction-free formula that entails the original goal; or a false formula if it is unsatisfiable.

    • fix

      protected void fix(Runnable action)
      Repeats an action on this state until a fixpoint is reached.

      The action is executed at least once. If the values of form and/or solution have changed as a side effect, it is repeated as long as there are further changes.

      Parameters:
      action - the action to iterate
      See Also:

    • changeBy

      protected boolean changeBy(Runnable action)
      Executes an action on this state and detects changes.

      Subclasses may override this method to detect changes to extra state attributes.

      The default implementation detects changes to form and solution.

      Parameters:
      action - the action to iterate
      Returns:
      true if the state has changed due to side effects, false otherwise.

    • propagateUnits

      protected void propagateUnits()
      Commits to all literals occuring as unit clauses.

    • assignPure

      protected void assignPure()
      Commits to all literals occuring purely.

    • eagerHeuristics

      protected void eagerHeuristics()
      Performs eager heuristics on this state.

      Subclasses may override this method to add further heuristics. It is recommended to also perform the default heuristics, by invoking super.eagerHeuristics(), since they are what makes the DPLL algorithm practically efficient.

      The default implementation iterates propagateUnits() until a fixpoint is reached, followed by assignPure().

      See Also:

    • commit

      protected void commit(Literal<P> literal)
      Changes this state by committing to a literal.

      The literal is added as a unit clause to the solution. The formula to be solved is simplified accordingly.

      Parameters:
      literal - the literal to commit to