eu.bandm.tools.util

Class SAT<P>

java.lang.Object

eu.bandm.tools.util.SAT<P>

Type Parameters:

P - base class of propositional variables.

public class SAT<P>
extends Object

Solver for propositional formulas in conjunctive normal form. Based on the DPLL algorithm.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	SAT.Clause<P> Disjunction of literals.
protected static class	SAT.Form<P> Conjunction of clauses.
static class	SAT.Literal<P> Optionally negated propositional variable.

Constructor Summary

Constructors

Constructor and Description
SAT() Create a new solver.

Method Summary

Modifier and Type	Method and Description
protected SAT.Literal<? extends P>	choose(SAT.Form<P> form) Choose a literal to resolve from a formula.
Set<SAT.Literal<? extends P>>	solve(Collection<? extends Collection<? extends SAT.Literal<? extends P>>> cnf) Solve a formula.
protected SAT.Form<P>	solve(SAT.Form<P> form) Solve a formula.

Methods inherited from class java.lang.Object

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

Constructor Detail

SAT

public SAT()

Create a new solver.

Method Detail

choose

protected SAT.Literal<? extends P> choose(SAT.Form<P> form)

Choose a literal to resolve from a formula. 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().

Parameters:

form - the current formula, a nonempty collection of nonempty clauses.

Returns:

a literal occurring in form.

solve

protected SAT.Form<P> solve(SAT.Form<P> form)

Solve a formula. Subclasses may override this method for global pre- or post-processing.

Parameters:

form - a formula to solve.

Returns:

a satisfiable disjunction-free formula that implies form; or a false formula if form is unsatisfiable.

solve

public Set<SAT.Literal<? extends P>> solve(Collection<? extends Collection<? extends SAT.Literal<? extends P>>> cnf)

Solve a formula.

Parameters:

cnf - a formula to solve, given as a collection of clauses (collections of literals).

Returns:

a consistent set of literals that jointly imply form; or a false formula if form is unsatisfiable.