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

Packages that use AssertingClauseGenerator

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).
org.sat4j.pb.core

Uses of AssertingClauseGenerator in org.sat4j.minisat.core

Fields in org.sat4j.minisat.core declared as AssertingClauseGenerator

protected AssertingClauseGenerator

Solver.analyzer

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

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

Solver(AssertingClauseGenerator acg, LearningStrategy<D> learner, D dsf, SearchParams params, IOrder 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.

Uses of AssertingClauseGenerator in org.sat4j.pb.core

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

PBSolver(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter)

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

PBSolverCautious(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverCautious(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, int bound)

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

PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)

PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)

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

PBSolverResCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverResCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, long bound)

PBSolverResCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)

PBSolverResCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)

PBSolverResolution(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter)

PBSolverResolution(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)

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