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

Packages that use Literal

Package	Description
eu.bandm.tools.dpll	Model and solver for propositional logic in conjunctive normal form.

Uses of Literal in eu.bandm.tools.dpll

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

Modifier and Type	Method	Description
protected Literal<P>	SATSolver.State.choose()	Chooses a literal to resolve.
abstract @Opt Literal<P>	Clause.getUnit()	Extract the unit literal if appropriate.
Literal<P>	Literal.negate()	Return the negation of this literal.
static <P> Literal<P>	Literal.negative(P variable)	Creates a new negative instance.
static <P> Literal<P>	Literal.positive(P variable)	Creates a new positive instance.

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

Modifier and Type	Method	Description
Optional<Set<Literal<P>>>	SATSolver.findSolution(Formula<P> form)	Solves a formula.
abstract Iterable<Literal<P>>	Formula.literals()	View literals occurring in this formula.
(package private) abstract Set<Literal<P>>	Formula.pure()	Returns the set of all literals occuring purely in this formula.
static <P> Set<Literal<P>>	Literal.pure(Iterable<Literal<P>> literals)	Finds the propositional variables occurring purely in some literals.

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

Modifier and Type	Method	Description
protected void	SATSolver.State.commit(Literal<P> literal)	Changes this state by committing to a literal.
abstract Clause<P>	Clause.given(Literal<P> literal)	Returns a simplified clause that is equivalent to this clause assuming the given literal.
abstract Formula<P>	Formula.given(Literal<P> literal)	Returns a formula that abstracts from the given literal in this formula.
static <P> Clause<P>	Clause.of(Literal<P>... literals)	Returns a clause containing the given literals.
static <P> Clause<P>	Clause.unit(Literal<P> literal)	Returns a unitary clause containing the given literal.
Formula<P>	Formula.with(Literal<P> first)	Returns a formula that prepends a unit clause to this formula.
protected SATSolver.State<P>	SATSolver.State.with(Literal<P> literal)	Creates a copy of this state with a given unit clause added to the formula.

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

Modifier and Type	Method	Description
static <P> boolean	Literal.isConsistent(Collection<Literal<P>> literals)	Checks whether the given literals are consistent.
boolean	Clause.isSatisfiedBy(Set<Literal<P>> solution)	Checks whether this proposition is satisfied by a given solution.
boolean	Formula.isSatisfiedBy(Set<Literal<P>> solution)	Checks whether this proposition is satisfied by a given solution.
boolean	Literal.isSatisfiedBy(Set<Literal<P>> solution)	Checks whether this proposition is satisfied by a given solution.
boolean	Proposition.isSatisfiedBy(Set<Literal<P>> solution)	Checks whether this proposition is satisfied by a given solution.
static <P> Clause<P>	Clause.of(List<Literal<P>> literals)	Returns a clause containing the given literals.
static <P> Set<Literal<P>>	Literal.pure(Iterable<Literal<P>> literals)	Finds the propositional variables occurring purely in some literals.