Package owl.logic.propositional.sat

Class Solver

java.lang.Object

owl.logic.propositional.sat.Solver

public final class Solver
extends Object

Interface for SAT-solver for propositional formulas.

Method Summary

Modifier and Type	Method	Description
static IncrementalSolver	incrementalSolver()
static IncrementalSolver	incrementalSolver(owl.logic.propositional.sat.Solver.Engine engine)
static <V> List<Set<V>>	maximalModels(PropositionalFormula<V> formula, Set<V> upperBound)
static <V> List<Set<V>>	maximalModels(PropositionalFormula<V> formula, Set<V> upperBound, owl.logic.propositional.sat.Solver.Engine engine)
static Optional<BitSet>	model(com.google.common.primitives.ImmutableIntArray clauses)	Determine if the the given conjunctiveNormalForm is satisfiable and if this is the case return a satisfying assignment.
static Optional<BitSet>	model(com.google.common.primitives.ImmutableIntArray clauses, owl.logic.propositional.sat.Solver.Engine engine)
static <V> Optional<Set<V>>	model(PropositionalFormula<V> formula)
static <V> Optional<Set<V>>	model(PropositionalFormula<V> preFormula, owl.logic.propositional.sat.Solver.Engine engine)

Methods inherited from class java.lang.Object

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

Method Detail

incrementalSolver

public static IncrementalSolver incrementalSolver()

incrementalSolver

public static IncrementalSolver incrementalSolver(owl.logic.propositional.sat.Solver.Engine engine)

model

public static Optional<BitSet> model(com.google.common.primitives.ImmutableIntArray clauses)

Determine if the the given conjunctiveNormalForm is satisfiable and if this is the case return a satisfying assignment. Note that variables are shifted by 1. Thus bs.get(0) retrieves the assigend value to variable 1 in the given conjunctiveNormalForm.

Parameters:

clauses - in conjunctive normal form.

Returns:

Optional.empty() if the given conjunctiveNormalForm is not satisfiable. Otherwise a satisfying assignment.

model

public static Optional<BitSet> model(com.google.common.primitives.ImmutableIntArray clauses,
                                     owl.logic.propositional.sat.Solver.Engine engine)

model

public static <V> Optional<Set<V>> model(PropositionalFormula<V> formula)

model

public static <V> Optional<Set<V>> model(PropositionalFormula<V> preFormula,
                                         owl.logic.propositional.sat.Solver.Engine engine)

maximalModels

public static <V> List<Set<V>> maximalModels(PropositionalFormula<V> formula,
                                             Set<V> upperBound)

maximalModels

public static <V> List<Set<V>> maximalModels(PropositionalFormula<V> formula,
                                             Set<V> upperBound,
                                             owl.logic.propositional.sat.Solver.Engine engine)