Uses of Interface
org.sat4j.minisat.core.AssertingClauseGenerator

Packages that use AssertingClauseGenerator

org.sat4j.minisat.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.uip	Various ways to compute an asserting clause (containing one Unique Implication Point).

Uses of AssertingClauseGenerator in org.sat4j.minisat.constraints.pb

Constructors in org.sat4j.minisat.constraints.pb with parameters of type AssertingClauseGenerator

PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, IOrder<L> order)

PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order)

PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter)

PBSolverClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)

PBSolverMerging(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)

PBSolverWithImpliedClause(AssertingClauseGenerator acg, LearningStrategy<ILits> learner, DataStructureFactory<ILits> dsf, IOrder<ILits> order)

Uses of AssertingClauseGenerator in org.sat4j.minisat.core

Constructors in org.sat4j.minisat.core with parameters of type AssertingClauseGenerator

Solver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, IOrder<L> order, RestartStrategy restarter)
creates a Solver without LearningListener.

Solver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter)

Uses of AssertingClauseGenerator in org.sat4j.minisat.uip

Classes in org.sat4j.minisat.uip that implement AssertingClauseGenerator

class	DecisionUIP Decision UIP scheme for building an asserting clause.
class	FirstUIP FirstUIP scheme introduced in Chaff.