Uses of Class
eu.bandm.tools.dpll.SAT.Literal

Packages that use SAT.Literal

Package	Description
eu.bandm.tools.dpll	SAT solver according to Davis-Putnam-Logemann-Loveland.

Uses of SAT.Literal in eu.bandm.tools.dpll

Methods in eu.bandm.tools.dpll that return SAT.Literal

Modifier and Type	Method	Description
protected SAT.Literal<? extends P>	SAT.choose(SAT.Form<P> form)	Choose a literal to resolve from a formula.
abstract SAT.Literal<? extends P>	SAT.Clause.getUnit()	Extract unit literal.
SAT.Literal<P>	SAT.Literal.negate()	Return the negation of this literal.

Methods in eu.bandm.tools.dpll that return types with arguments of type SAT.Literal

Modifier and Type	Method	Description
abstract Iterable<SAT.Literal<? extends P>>	SAT.Form.literals()	View literals occurring in this formula.
(package private) abstract Set<SAT.Literal<? extends P>>	SAT.Form.pure()
Set<SAT.Literal<? extends P>>	SAT.solve(Collection<? extends Collection<? extends SAT.Literal<? extends P>>> cnf)	Solve a formula.

Methods in eu.bandm.tools.dpll with parameters of type SAT.Literal

Modifier and Type	Method	Description
(package private) static <P> SAT.Form<P>	SAT.Form.and(SAT.Literal<? extends P> first, SAT.Form<P> rest)
(package private) static <P> SAT.Clause<P>	SAT.Clause.or(SAT.Literal<? extends P>... lits)
(package private) static <P> SAT.Clause<P>	SAT.Clause.or(SAT.Literal<? extends P> first, SAT.Clause<P> rest)
(package private) abstract SAT.Clause<P>	SAT.Clause.propagate(SAT.Literal<? extends P> lit)
(package private) abstract SAT.Form<P>	SAT.Form.propagate(SAT.Literal<? extends P> lit)

Method parameters in eu.bandm.tools.dpll with type arguments of type SAT.Literal

Modifier and Type	Method	Description
Set<SAT.Literal<? extends P>>	SAT.solve(Collection<? extends Collection<? extends SAT.Literal<? extends P>>> cnf)	Solve a formula.