Package | Description |
---|---|
org.sat4j.minisat.constraints |
Implementations of various constraints for MiniSAT.
|
org.sat4j.minisat.constraints.card |
Implementations of cardinality constraints.
|
org.sat4j.minisat.constraints.cnf |
Implementations of clausal constraints.
|
org.sat4j.minisat.core |
Implementation of the MiniSAT solver skeleton.
|
org.sat4j.pb.constraints |
Implementation of data structures for pseudo boolean constraints.
|
org.sat4j.pb.constraints.pb |
Implementations of pseudo boolean constraints.
|
org.sat4j.pb.core |
Implementations of pseudo boolean solvers
|
org.sat4j.specs |
Those classes are intended for users dealing with SAT solvers as black boxes.
|
org.sat4j.tools |
Tools to be used on top of an
ISolver . |
Modifier and Type | Field and Description |
---|---|
protected UnitPropagationListener |
AbstractDataStructureFactory.solver |
Modifier and Type | Method and Description |
---|---|
void |
AbstractDataStructureFactory.setUnitPropagationListener(UnitPropagationListener s) |
Modifier and Type | Method and Description |
---|---|
void |
MaxWatchCard.assertConstraint(UnitPropagationListener s) |
void |
AtLeast.assertConstraint(UnitPropagationListener s) |
void |
MinWatchCard.assertConstraint(UnitPropagationListener s) |
void |
MaxWatchCard.assertConstraintIfNeeded(UnitPropagationListener s) |
void |
AtLeast.assertConstraintIfNeeded(UnitPropagationListener s) |
void |
MinWatchCard.assertConstraintIfNeeded(UnitPropagationListener s) |
static Constr |
AtLeast.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n) |
protected MinWatchCard |
MinWatchCard.computePropagation(UnitPropagationListener s) |
static Constr |
MaxWatchCard.maxWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr?
|
static Constr |
MinWatchCard.minWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Constructs a cardinality constraint with a minimal set of watched
literals Permet la cr?
|
protected static int |
AtLeast.niceParameters(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int deg) |
boolean |
MaxWatchCard.propagate(UnitPropagationListener s,
int p)
Propagation de la valeur de v?
|
boolean |
AtLeast.propagate(UnitPropagationListener s,
int p) |
boolean |
MinWatchCard.propagate(UnitPropagationListener s,
int p)
propagates the value of a falsified literal
|
void |
MaxWatchCard.remove(UnitPropagationListener upl) |
void |
AtLeast.remove(UnitPropagationListener upl) |
void |
MinWatchCard.remove(UnitPropagationListener upl)
Removes a constraint from the solver
|
Modifier and Type | Method and Description |
---|---|
void |
HTClause.assertConstraint(UnitPropagationListener s) |
void |
UnitClause.assertConstraint(UnitPropagationListener s) |
void |
UnitClauses.assertConstraint(UnitPropagationListener s) |
void |
WLClause.assertConstraint(UnitPropagationListener s) |
void |
BinaryClause.assertConstraint(UnitPropagationListener s) |
void |
HTClause.assertConstraintIfNeeded(UnitPropagationListener s) |
void |
UnitClause.assertConstraintIfNeeded(UnitPropagationListener s) |
void |
UnitClauses.assertConstraintIfNeeded(UnitPropagationListener s) |
void |
WLClause.assertConstraintIfNeeded(UnitPropagationListener s) |
void |
BinaryClause.assertConstraintIfNeeded(UnitPropagationListener s) |
static OriginalWLClause |
OriginalWLClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
static OriginalHTClause |
OriginalHTClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
static OriginalBinaryClause |
OriginalBinaryClause.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
boolean |
HTClause.propagate(UnitPropagationListener s,
int p) |
boolean |
UnitClause.propagate(UnitPropagationListener s,
int p) |
boolean |
UnitClauses.propagate(UnitPropagationListener s,
int p) |
boolean |
WLClause.propagate(UnitPropagationListener s,
int p) |
boolean |
BinaryClause.propagate(UnitPropagationListener s,
int p) |
void |
HTClause.remove(UnitPropagationListener upl) |
void |
UnitClause.remove(UnitPropagationListener upl) |
void |
UnitClauses.remove(UnitPropagationListener upl) |
void |
WLClause.remove(UnitPropagationListener upl) |
void |
BinaryClause.remove(UnitPropagationListener upl) |
static IVecInt |
Clauses.sanityCheck(IVecInt ps,
ILits voc,
UnitPropagationListener s)
Perform some sanity check before constructing a clause a) if a literal is
assigned true, return null (the clause is satisfied) b) if a literal is
assigned false, remove it c) if a clause contains a literal and its
opposite (tautology) return null d) remove duplicate literals e) if the
clause is empty, return null f) if the clause if unit, transmit it to the
object responsible for unit propagation
|
Modifier and Type | Interface and Description |
---|---|
interface |
ICDCL<D extends DataStructureFactory>
Abstraction for Conflict Driven Clause Learning Solver.
|
Modifier and Type | Class and Description |
---|---|
class |
Solver<D extends DataStructureFactory>
The backbone of the library providing the modular implementation of a MiniSAT
(Chaff) like solver.
|
Modifier and Type | Method and Description |
---|---|
void |
Constr.assertConstraint(UnitPropagationListener s)
Method called when the constraint is to be asserted.
|
void |
Constr.assertConstraintIfNeeded(UnitPropagationListener s)
Method called when the constraint is added to the solver "on the fly".
|
boolean |
Propagatable.propagate(UnitPropagationListener s,
int p)
Propagate the truth value of a literal in constraints in which that
literal is falsified.
|
void |
Constr.remove(UnitPropagationListener upl)
Remove a constraint from the solver.
|
void |
DataStructureFactory.setUnitPropagationListener(UnitPropagationListener s) |
Modifier and Type | Method and Description |
---|---|
Constr |
MinCardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
ICardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
AtLeastCardPBConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
MinCardPBConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
AtLeastCardConstructor.constructCard(UnitPropagationListener solver,
ILits voc,
IVecInt theLits,
int degree) |
Constr |
UnitBinaryHTClauseConstructor.constructClause(UnitPropagationListener solver,
ILits voc,
IVecInt v) |
Constr |
UnitBinaryWLClauseConstructor.constructClause(UnitPropagationListener solver,
ILits voc,
IVecInt v) |
Constr |
UnitBinaryHTClausePBConstructor.constructClause(UnitPropagationListener solver,
ILits voc,
IVecInt v) |
Constr |
IClauseConstructor.constructClause(UnitPropagationListener solver,
ILits voc,
IVecInt v) |
Constr |
MinLongWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxLongWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MinWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
MaxLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
IPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Constr |
PuebloMinWatchPBConstructor.constructPB(UnitPropagationListener solver,
ILits voc,
int[] theLits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs) |
Modifier and Type | Method and Description |
---|---|
void |
MinWatchCardPB.assertConstraint(UnitPropagationListener s) |
void |
WatchPbLongCP.assertConstraint(UnitPropagationListener s) |
void |
AtLeastPB.assertConstraint(UnitPropagationListener s) |
void |
WatchPb.assertConstraint(UnitPropagationListener s) |
void |
WatchPbLong.assertConstraint(UnitPropagationListener s) |
void |
LearntHTClausePB.assertConstraint(UnitPropagationListener s) |
void |
WatchPbLongCP.assertConstraintIfNeeded(UnitPropagationListener s) |
void |
WatchPb.assertConstraintIfNeeded(UnitPropagationListener s) |
void |
WatchPbLong.assertConstraintIfNeeded(UnitPropagationListener s) |
static PBConstr |
AtLeastPB.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n) |
static OriginalBinaryClausePB |
OriginalBinaryClausePB.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
static OriginalHTClausePB |
OriginalHTClausePB.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data.
|
protected void |
MaxWatchPb.computePropagation(UnitPropagationListener s) |
protected void |
MinWatchPbLong.computePropagation(UnitPropagationListener s) |
protected abstract void |
WatchPbLongCP.computePropagation(UnitPropagationListener s) |
protected abstract void |
WatchPb.computePropagation(UnitPropagationListener s) |
protected void |
MaxWatchPbLongCP.computePropagation(UnitPropagationListener s) |
protected void |
MinWatchPb.computePropagation(UnitPropagationListener s) |
protected abstract void |
WatchPbLong.computePropagation(UnitPropagationListener s) |
protected void |
MinWatchPbLongCP.computePropagation(UnitPropagationListener s) |
protected void |
MaxWatchPbLong.computePropagation(UnitPropagationListener s) |
static PBConstr |
MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr?
|
static MaxWatchPb |
MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MaxWatchPbLongCP |
MaxWatchPbLongCP.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MaxWatchPbLong |
MaxWatchPbLong.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static PBConstr |
MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int degree)
Permet la cr?
|
static PuebloMinWatchPb |
PuebloMinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree) |
static MinWatchPbLong |
MinWatchPbLong.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MinWatchPb |
MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static MinWatchPbLongCP |
MinWatchPbLongCP.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
boolean |
MaxWatchPb.propagate(UnitPropagationListener s,
int p)
Propagation of a falsified literal
|
boolean |
MinWatchPbLong.propagate(UnitPropagationListener s,
int p)
Propagation of a falsified literal
|
boolean |
MaxWatchPbLongCP.propagate(UnitPropagationListener s,
int p)
Propagation of a falsified literal
|
boolean |
MinWatchPb.propagate(UnitPropagationListener s,
int p)
Propagation of a falsified literal
|
boolean |
WatchPbLong.propagate(UnitPropagationListener s,
int p) |
boolean |
MinWatchPbLongCP.propagate(UnitPropagationListener s,
int p)
Propagation of a falsified literal
|
boolean |
MaxWatchPbLong.propagate(UnitPropagationListener s,
int p)
Propagation of a falsified literal
|
void |
MaxWatchPb.remove(UnitPropagationListener upl)
Remove a constraint from the solver
|
void |
MinWatchPbLong.remove(UnitPropagationListener upl)
Remove the constraint from the solver
|
void |
MaxWatchPbLongCP.remove(UnitPropagationListener upl)
Remove a constraint from the solver
|
void |
MinWatchPb.remove(UnitPropagationListener upl)
Remove the constraint from the solver
|
void |
WatchPbLong.remove(UnitPropagationListener upl) |
void |
MinWatchPbLongCP.remove(UnitPropagationListener upl)
Remove the constraint from the solver
|
void |
MaxWatchPbLong.remove(UnitPropagationListener upl)
Remove a constraint from the solver
|
Modifier and Type | Interface and Description |
---|---|
interface |
IPBCDCLSolver<D extends PBDataStructureFactory>
Abstraction for Conflict Driven Clause Learning PBSolver.
|
Modifier and Type | Class and Description |
---|---|
class |
PBSolver |
class |
PBSolverCautious |
class |
PBSolverClause |
class |
PBSolverCP |
class |
PBSolverResCP |
class |
PBSolverResolution |
class |
PBSolverWithImpliedClause |
Modifier and Type | Method and Description |
---|---|
void |
UnitClauseProvider.provideUnitClauses(UnitPropagationListener upl) |
Modifier and Type | Method and Description |
---|---|
void |
ManyCore.provideUnitClauses(UnitPropagationListener upl) |
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.