Package eu.bandm.tools.dpll
This package contains data classes for the representation of propositional logical formulas in conjuctive normal form. All parts of formulas are realized as immutable objects that can be shared freely between parts of a formula, as well as between concurrent reasoning processes.
A complete solver for the satisfaction problem (SAT) is provided. The problem is NP-hard, and every complete algorithm must have exponential worst-case complexity. However, the provided solver is based on the Davis–Putnam–Logemann–Loveland algorithm. As such, performance is much better for many practical use cases, due to effective heuristics.
The overall design of the logical data model and the solver strongly prefers clean object-oriented structures over raw space and time efficiency. They are not intended to solve computationally massive problems, but for tight and easy integration into any Java application.
All classes in this package are parameterized with the type <P> of
propositional variables. This allows for embedding actual domain objects
into logical calculations, without any need for indirect encoding. The
embedded objects are used as abstract representatives up to equals.
Therefore the same caveats as for Map keys apply: Objects
that are used as propositional variables should be immutable, at least in any
observable sense that affects comparisons with equals. Furthermore,
their equals and hashCode methods are likely to be invoked
often during logical calculations, and should be reasonably efficient.
-
ClassDescriptionClause<P>Disjunction of literals.Formula<P>Conjunction of clauses.Literal<P>Positive or negative occurrence of propositional variable.Proposition<P>A logical proposition.SATSolver<P>Solver for propositional formulas in conjunctive normal form.A state of a DPLL-based solution process.