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 learner, DataStructureFactory dsf, IOrder order)

PBSolverCard(AssertingClauseGenerator acg, LearningStrategy learner, DataStructureFactory dsf, IOrder order)

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

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

Uses of AssertingClauseGenerator in org.sat4j.minisat.core

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

Solver(AssertingClauseGenerator acg, LearningStrategy learner, DataStructureFactory dsf, IOrder order)
creates a Solver without LearningListener.

Solver(AssertingClauseGenerator acg, LearningStrategy learner, DataStructureFactory dsf, SearchParams params, IOrder order)

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.