Package eu.bandm.tools.dpll

Class SATSolver<P>

java.lang.Object
eu.bandm.tools.dpll.SATSolver<P>
Type Parameters:
P - the type of propositional variables
public class SATSolver<P> extends Object
Solver for propositional formulas in conjunctive normal form. Based on the DPLL (Davis–Putnam–Logemann–Loveland) algorithm.

The solving procedure is highly customizable: Objects of customized subclasses of SATSolver.State can be injected by overriding the factory methods initialState(Formula) and SATSolver.State.with(Literal).

The data structures that represent the formulas to be solved are immutable. They are safe for sharing in distinct parts of a formula, for concurrent use in several independent solving tasks, and in subtask parallelization.

  • Constructor Details

    • SATSolver

      public SATSolver()
      Creates a new solver.

  • Method Details

    • initialState

      protected SATSolver.State<P> initialState(Formula<P> form)
      Creates a new initial state for solving the given formula.

      Subclasses may override this method to create instances of custom subclasses.

      The default implementation invokes new State(Formula).

      Parameters:
      form - the formula to solve
      Returns:
      a state that pairs the given formula with an empty solution candidate

    • solve

      public Formula<P> solve(Formula<P> form)
      Solves a formula. Subclasses may override this method for global pre- or post-processing.
      Parameters:
      form - the formula to solve
      Returns:
      a satisfiable disjunction-free formula that entails form; or a false formula if form is unsatisfiable.
      See Also:

    • findSolution

      public Optional<Set<Literal<P>>> findSolution(Formula<P> form)
      Solves a formula.
      Parameters:
      form - the formula to solve
      Returns:
      a consistent set of literals that jointly satisfy form; or Optional.empty() if form is unsatisfiable.
      See Also: