META-INF/MANIFEST.MF
META-INF/ECLIPSE_.SF
META-INF/ECLIPSE_.RSA
META-INF/
org/
org/sat4j/
org/sat4j/pb/
org/sat4j/pb/tools/
org/sat4j/pb/constraints/
org/sat4j/pb/constraints/pb/
org/sat4j/pb/reader/
org/sat4j/pb/orders/
org/sat4j/pb/core/
build.properties
overview.html
org/sat4j/pb/PBSolverDecorator.classPBSolverDecorator.java
package org.sat4j.pb
public org.sat4j.pb.PBSolverDecorator extends org.sat4j.tools.SolverDecorator implements org.sat4j.pb.IPBSolver {
private static final long serialVersionUID
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
}
org/sat4j/pb/SolverFactory.classSolverFactory.java
package org.sat4j.pb
public final org.sat4j.pb.SolverFactory extends org.sat4j.core.ASolverFactory {
private static final long serialVersionUID
private static org.sat4j.pb.SolverFactory instance
private void ()
private static synchronized void createInstance ()
public static org.sat4j.pb.SolverFactory instance ()
public static org.sat4j.pb.core.PBSolverResolution newPBResAllPB ()
public static org.sat4j.pb.core.PBSolverCP newPBCPAllPB ()
public static org.sat4j.pb.IPBSolver newOPBStringSolver ()
public static org.sat4j.pb.core.PBSolverCP newPBCPMixedConstraints ()
public static org.sat4j.pb.core.PBSolverCP newPBCPMixedConstraintsObjective ()
public static org.sat4j.pb.core.PBSolverCP newCompetPBCPMixedConstraintsObjective ()
public static org.sat4j.pb.core.PBSolverCP newCompetPBCPMixedConstraintsMinObjective ()
public static org.sat4j.pb.core.PBSolverCP newCompetPBCPMixedConstraintsLongMaxObjective ()
public static org.sat4j.pb.core.PBSolverCP newCompetPBCPMixedConstraintsLongMinObjective ()
public static org.sat4j.pb.core.PBSolverCP newPBCPMixedConstraintsObjectiveLearnJustClauses ()
org.sat4j.minisat.learning.ClauseOnlyLearning learning
org.sat4j.pb.core.PBSolverCP solver
public static org.sat4j.pb.core.PBSolverCP newCompetPBCPMixedConstraintsObjectiveLearnJustClauses ()
org.sat4j.minisat.learning.ClauseOnlyLearning learning
org.sat4j.pb.core.PBSolverCP solver
private static org.sat4j.pb.core.PBSolverCP newPBKiller (org.sat4j.minisat.core.IPhaseSelectionStrategy)
org.sat4j.minisat.core.IPhaseSelectionStrategy phase
org.sat4j.minisat.learning.ClauseOnlyLearning learning
org.sat4j.pb.core.PBSolverCP solver
public static org.sat4j.pb.core.PBSolverCP newPBKillerRSAT ()
public static org.sat4j.pb.core.PBSolverCP newPBKillerClassic ()
public static org.sat4j.pb.core.PBSolverCP newPBKillerFixed ()
private static org.sat4j.pb.core.PBSolverCP newCompetPBKiller (org.sat4j.minisat.core.IPhaseSelectionStrategy)
org.sat4j.minisat.core.IPhaseSelectionStrategy phase
org.sat4j.minisat.learning.ClauseOnlyLearning learning
org.sat4j.pb.core.PBSolverCP solver
public static org.sat4j.pb.core.PBSolverCP newCompetPBKillerRSAT ()
public static org.sat4j.pb.core.PBSolverCP newCompetPBKillerClassic ()
public static org.sat4j.pb.core.PBSolverCP newCompetPBKillerFixed ()
public static org.sat4j.pb.core.PBSolverCP newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause ()
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverCP solver
public static org.sat4j.pb.core.PBSolverCP newPBCPMixedConstraintsObjectiveNoLearning ()
org.sat4j.minisat.learning.NoLearningButHeuristics learning
org.sat4j.pb.core.PBSolverCP solver
public static org.sat4j.pb.core.PBSolverResolution newPBResMixedConstraintsObjective ()
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newCompetPBResWLMixedConstraintsObjectiveExpSimp ()
public static org.sat4j.pb.core.PBSolverResolution newCompetPBResHTMixedConstraintsObjectiveExpSimp ()
public static org.sat4j.pb.core.PBSolverResolution newCompetPBResLongHTMixedConstraintsObjectiveExpSimp ()
public static org.sat4j.pb.core.PBSolverResolution newCompetPBResLongWLMixedConstraintsObjectiveExpSimp ()
public static org.sat4j.pb.core.PBSolverResolution newCompetMinPBResLongWLMixedConstraintsObjectiveExpSimp ()
public static org.sat4j.pb.core.PBSolverResolution newCompetPBResMixedConstraintsObjectiveExpSimp (org.sat4j.pb.core.PBDataStructureFactory)
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newPBResHTMixedConstraintsObjective ()
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.constraints.AbstractPBDataStructureFactory ds
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newCompetPBResMinHTMixedConstraintsObjective ()
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newPBResMinHTMixedConstraintsObjective ()
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.constraints.AbstractPBDataStructureFactory ds
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newCompetPBResMixedConstraintsObjectiveExpSimp ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newPBResHTMixedConstraintsObjectiveExpSimp ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newCompetPBResMinHTMixedConstraintsObjectiveExpSimp ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverClause newPBCPMixedConstraintsReduceToClause ()
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverClause solver
public static org.sat4j.pb.core.PBSolverCautious newPBCPMixedConstraintsCautious (int)
int bound
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverCautious solver
public static org.sat4j.pb.core.PBSolverCautious newPBCPMixedConstraintsCautious ()
public static org.sat4j.pb.core.PBSolverResCP newPBCPMixedConstraintsResCP (long)
long bound
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverResCP solver
public static org.sat4j.pb.core.PBSolverResCP newPBCPMixedConstraintsResCP ()
public static org.sat4j.pb.core.PBSolverWithImpliedClause newPBCPMixedConstrainsImplied ()
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverWithImpliedClause solver
public static org.sat4j.pb.core.PBSolverCP newMiniOPBClauseAtLeastConstrMax ()
public static org.sat4j.pb.core.PBSolverResolution newPBResAllPBWL ()
public static org.sat4j.pb.core.PBSolverCP newPBCPAllPBWL ()
public static org.sat4j.pb.core.PBSolverResolution newPBResAllPBWLPueblo ()
private static org.sat4j.pb.core.PBSolverResolution newPBRes (org.sat4j.pb.core.PBDataStructureFactory)
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverCP newPBCPAllPBWLPueblo ()
public static org.sat4j.pb.core.PBSolverCP newMiniOPBClauseCardMinPueblo ()
public static org.sat4j.pb.core.PBSolverCP newMiniOPBClauseCardMin ()
public static org.sat4j.pb.core.PBSolverCP newMiniOPBClauseAtLeastMinPueblo ()
private static org.sat4j.pb.core.PBSolverCP newPBCP (org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder)
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverCP solver
private static org.sat4j.pb.core.PBSolverCP newPBCP (org.sat4j.pb.core.PBDataStructureFactory)
org.sat4j.pb.core.PBDataStructureFactory dsf
public static org.sat4j.pb.IPBSolver newCuttingPlanes ()
public static org.sat4j.pb.IPBSolver newCuttingPlanesAggressiveCleanup ()
org.sat4j.pb.core.PBSolverCP solver
public static org.sat4j.pb.IPBSolver newResolution ()
public static org.sat4j.pb.IPBSolver newBoth ()
public static org.sat4j.pb.IPBSolver newSATUNSAT ()
public static org.sat4j.pb.core.PBSolverResolution newSAT ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newUNSAT ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newResolutionGlucose ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newResolutionGlucose21 ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newResolutionGlucoseSimpleSimp ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolverResolution newResolutionGlucoseExpSimp ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.IPBSolver newSimpleSimplification ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.IPBSolver newResolutionSimpleRestarts ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.IPBSolver newResolutionMaxMemory ()
org.sat4j.pb.core.PBSolverResolution solver
public static org.sat4j.pb.core.PBSolver newDefault ()
public static org.sat4j.pb.IPBSolver newDefaultNonNormalized ()
org.sat4j.pb.core.PBSolver solver
org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure ds
public org.sat4j.pb.core.PBSolver defaultSolver ()
public static org.sat4j.pb.IPBSolver newDefaultOptimizer ()
public static org.sat4j.pb.IPBSolver newLight ()
public org.sat4j.pb.IPBSolver lightSolver ()
public static org.sat4j.pb.IPBSolver newEclipseP2 ()
org.sat4j.minisat.learning.MiniSATLearning learning
org.sat4j.pb.core.PBSolverResolution solver
public volatile org.sat4j.specs.ISolver lightSolver ()
public volatile org.sat4j.specs.ISolver defaultSolver ()
}
org/sat4j/pb/PseudoIteratorDecorator.classPseudoIteratorDecorator.java
package org.sat4j.pb
public org.sat4j.pb.PseudoIteratorDecorator extends org.sat4j.pb.PseudoOptDecorator {
private static final long serialVersionUID
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public void discardCurrentSolution () throws org.sat4j.specs.ContradictionException
int[] last
org.sat4j.specs.IVecInt clause
int q
}
org/sat4j/pb/tools/LexicoHelper.classLexicoHelper.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.LexicoHelper extends org.sat4j.pb.tools.AbstractLexicoHelper {
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public void (org.sat4j.pb.IPBSolver, boolean, boolean)
org.sat4j.pb.IPBSolver solver
boolean explanationEnabled
boolean canonicalOptFunctionEnabled
public void (org.sat4j.pb.IPBSolver, boolean)
org.sat4j.pb.IPBSolver solver
boolean explanationEnabled
}
org/sat4j/pb/tools/WeightedObject.classWeightedObject.java
package org.sat4j.pb.tools
public final org.sat4j.pb.tools.WeightedObject extends java.lang.Object implements java.lang.Comparable {
public final Object thing
private java.math.BigInteger weight
private void (java.lang.Object, java.math.BigInteger)
Object thing
java.math.BigInteger weight
public java.math.BigInteger getWeight ()
public void increaseWeight (java.math.BigInteger)
java.math.BigInteger delta
public int compareTo (org.sat4j.pb.tools.WeightedObject)
org.sat4j.pb.tools.WeightedObject arg0
public static org.sat4j.pb.tools.WeightedObject newWO (java.lang.Object, int)
Object e
int w
public static org.sat4j.pb.tools.WeightedObject newWO (java.lang.Object, long)
Object e
long w
public static org.sat4j.pb.tools.WeightedObject newWO (java.lang.Object, java.math.BigInteger)
Object e
java.math.BigInteger w
public int hashCode ()
int result
public boolean equals (java.lang.Object)
Object obj
org.sat4j.pb.tools.WeightedObject other
public volatile int compareTo (java.lang.Object)
}
org/sat4j/pb/tools/SteppedTimeoutLexicoHelper.classSteppedTimeoutLexicoHelper.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.SteppedTimeoutLexicoHelper extends org.sat4j.pb.tools.AbstractLexicoHelper {
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public void (org.sat4j.pb.IPBSolver, boolean, boolean)
org.sat4j.pb.IPBSolver solver
boolean explanationEnabled
boolean canonicalOptFunctionEnabled
public void (org.sat4j.pb.IPBSolver, boolean)
org.sat4j.pb.IPBSolver solver
boolean explanationEnabled
}
org/sat4j/pb/tools/ManyCorePB.classManyCorePB.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.ManyCorePB extends org.sat4j.tools.ManyCore implements org.sat4j.pb.IPBSolver {
private static final long serialVersionUID
public transient void (org.sat4j.core.ASolverFactory, java.lang.String[])
org.sat4j.core.ASolverFactory factory
String[] solverNames
public transient void (org.sat4j.pb.IPBSolver[])
org.sat4j.pb.IPBSolver[] iSolver
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
org.sat4j.core.ConstrGroup group
int i
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
int i
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
org.sat4j.core.ConstrGroup group
int i
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
org.sat4j.core.ConstrGroup group
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
org.sat4j.core.ConstrGroup group
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
org.sat4j.core.ConstrGroup group
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
org.sat4j.core.ConstrGroup group
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
org.sat4j.core.ConstrGroup group
int i
}
org/sat4j/pb/tools/SteppedTimeoutLexicoDecoratorPB.classSteppedTimeoutLexicoDecoratorPB.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.SteppedTimeoutLexicoDecoratorPB extends org.sat4j.pb.tools.LexicoDecoratorPB {
private static final long serialVersionUID
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public boolean admitABetterSolution (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
int i
org.sat4j.specs.TimeoutException te
org.sat4j.specs.ContradictionException ce
private void mergeCurrentandNextCriteria ()
org.sat4j.pb.ObjectiveFunction currentObj
int currentObjSize
org.sat4j.pb.ObjectiveFunction nextObj
int nextObjSize
org.sat4j.specs.IVecInt newLits
org.sat4j.specs.IVec newCoeffs
java.math.BigInteger coeffFactor
java.util.Iterator it
}
org/sat4j/pb/tools/StringNegator.classStringNegator.java
package org.sat4j.pb.tools
public final org.sat4j.pb.tools.StringNegator extends java.lang.Object implements org.sat4j.pb.tools.INegator {
public static final org.sat4j.pb.tools.INegator INSTANCE
static void ()
private void ()
public boolean isNegated (java.lang.Object)
Object thing
public java.lang.Object unNegate (java.lang.Object)
Object thing
}
org/sat4j/pb/tools/AbstractLexicoHelper.classAbstractLexicoHelper.java
package org.sat4j.pb.tools
public abstract org.sat4j.pb.tools.AbstractLexicoHelper extends org.sat4j.pb.tools.DependencyHelper implements org.sat4j.tools.SolutionFoundListener {
private final org.sat4j.pb.tools.LexicoDecoratorPB lexico
private boolean hasASolution
public void (org.sat4j.pb.tools.LexicoDecoratorPB)
org.sat4j.pb.tools.LexicoDecoratorPB lexico
public void (org.sat4j.pb.tools.LexicoDecoratorPB, boolean)
org.sat4j.pb.tools.LexicoDecoratorPB lexico
boolean explanationEnabled
public void (org.sat4j.pb.tools.LexicoDecoratorPB, boolean, boolean)
org.sat4j.pb.tools.LexicoDecoratorPB lexico
boolean explanationEnabled
boolean canonicalOptFunctionEnabled
public void addCriterion (java.util.Collection)
java.util.Collection things
org.sat4j.specs.IVecInt literals
Object thing
public void addWeightedCriterion (java.util.Collection)
java.util.Collection things
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
org.sat4j.pb.tools.WeightedObject wo
public boolean hasASolution () throws org.sat4j.specs.TimeoutException
org.sat4j.specs.TimeoutException e
public boolean hasASolution (org.sat4j.specs.IVec) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVec assumps
org.sat4j.specs.TimeoutException e
public boolean hasASolution (java.util.Collection) throws org.sat4j.specs.TimeoutException
java.util.Collection assumps
org.sat4j.specs.TimeoutException e
public boolean isOptimal ()
public void onSolutionFound (int[])
int[] solution
public void onSolutionFound (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt solution
public void onUnsatTermination ()
}
org/sat4j/pb/tools/ImplicationNamer.classImplicationNamer.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.ImplicationNamer extends java.lang.Object {
private final org.sat4j.pb.tools.DependencyHelper helper
private org.sat4j.specs.IVec toName
public void (org.sat4j.pb.tools.DependencyHelper, org.sat4j.specs.IVec)
org.sat4j.pb.tools.DependencyHelper helper
org.sat4j.specs.IVec toName
public void named (java.lang.Object)
Object name
java.util.Iterator it
}
org/sat4j/pb/tools/INegator.classINegator.java
package org.sat4j.pb.tools
public abstract org.sat4j.pb.tools.INegator extends java.lang.Object {
public abstract boolean isNegated (java.lang.Object)
public abstract java.lang.Object unNegate (java.lang.Object)
}
org/sat4j/pb/tools/DependencyHelper$2.classDependencyHelper.java
package org.sat4j.pb.tools
org.sat4j.pb.tools.DependencyHelper$2 extends java.lang.Object implements org.sat4j.pb.tools.INegator {
void ()
public boolean isNegated (java.lang.Object)
Object thing
public java.lang.Object unNegate (java.lang.Object)
Object thing
}
org/sat4j/pb/tools/LexicoDecoratorPB.classLexicoDecoratorPB.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.LexicoDecoratorPB extends org.sat4j.tools.LexicoDecorator implements org.sat4j.pb.IPBSolver {
private static final long serialVersionUID
protected final java.util.List objs
private java.math.BigInteger bigCurrentValue
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public boolean admitABetterSolution (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
public void addCriterion (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt literals
public void addCriterion (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
protected java.lang.Number evaluate ()
protected java.lang.Number evaluate (int)
int criterion
protected void fixCriterionValue () throws org.sat4j.specs.ContradictionException
protected org.sat4j.specs.IConstr discardSolutionsForOptimizing () throws org.sat4j.specs.ContradictionException
public int numberOfCriteria ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
}
org/sat4j/pb/tools/package-info.classpackage-info.java
package org.sat4j.pb.tools
abstract org.sat4j.pb.tools.package-info extends java.lang.Object {
}
org/sat4j/pb/tools/DependencyHelper$1.classDependencyHelper.java
package org.sat4j.pb.tools
org.sat4j.pb.tools.DependencyHelper$1 extends java.lang.Object implements org.sat4j.pb.tools.INegator {
void ()
public boolean isNegated (java.lang.Object)
Object thing
public java.lang.Object unNegate (java.lang.Object)
Object thing
}
org/sat4j/pb/tools/DependencyHelper.classDependencyHelper.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.DependencyHelper extends java.lang.Object {
public static final org.sat4j.pb.tools.INegator NO_NEGATION
public static final org.sat4j.pb.tools.INegator BASIC_NEGATION
private static final long serialVersionUID
private final java.util.Map mapToDimacs
private final java.util.Map mapToDomain
final java.util.Map descs
private final org.sat4j.pb.tools.XplainPB xplain
private final org.sat4j.tools.GateTranslator gator
final org.sat4j.pb.IPBSolver solver
private org.sat4j.pb.tools.INegator negator
private org.sat4j.pb.ObjectiveFunction objFunction
private org.sat4j.specs.IVecInt objLiterals
private org.sat4j.specs.IVec objCoefs
private final boolean explanationEnabled
private final boolean canonicalOptFunction
static void ()
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public void (org.sat4j.pb.IPBSolver, boolean)
org.sat4j.pb.IPBSolver solver
boolean explanationEnabled
public void (org.sat4j.pb.IPBSolver, boolean, boolean)
org.sat4j.pb.IPBSolver solver
boolean explanationEnabled
boolean canonicalOptFunctionEnabled
public void setNegator (org.sat4j.pb.tools.INegator)
org.sat4j.pb.tools.INegator negator
protected int getIntValue (java.lang.Object)
Object thing
protected int getIntValue (java.lang.Object, boolean)
Object thing
boolean create
Object myThing
Object myThing
boolean negated
Integer intValue
public org.sat4j.specs.IVec getSolution ()
int[] model
org.sat4j.specs.IVec toInstall
int i
public java.util.Collection getASolution ()
int[] model
java.util.Collection toInstall
int i
public java.math.BigInteger getSolutionCost ()
public boolean getBooleanValueFor (java.lang.Object)
Object t
int dimacsValue
public boolean hasASolution () throws org.sat4j.specs.TimeoutException
public boolean hasASolution (org.sat4j.specs.IVec) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVec assumps
org.sat4j.specs.IVecInt assumptions
java.util.Iterator it
public boolean hasASolution (java.util.Collection) throws org.sat4j.specs.TimeoutException
java.util.Collection assumps
org.sat4j.specs.IVecInt assumptions
Object t
public java.util.Set why () throws org.sat4j.specs.TimeoutException
java.util.Collection explanation
java.util.Set ezexplain
org.sat4j.specs.IConstr constr
Object desc
public java.util.Set why (java.lang.Object) throws org.sat4j.specs.TimeoutException
Object thing
org.sat4j.specs.IVecInt assumps
public java.util.Set whyNot (java.lang.Object) throws org.sat4j.specs.TimeoutException
Object thing
org.sat4j.specs.IVecInt assumps
private java.util.Set why (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
public void setTrue (java.lang.Object, java.lang.Object) throws org.sat4j.specs.ContradictionException
Object thing
Object name
org.sat4j.specs.IConstr constr
public void setFalse (java.lang.Object, java.lang.Object) throws org.sat4j.specs.ContradictionException
Object thing
Object name
org.sat4j.specs.IConstr constr
public transient org.sat4j.pb.tools.ImplicationRHS implication (java.lang.Object[])
Object[] lhs
org.sat4j.specs.IVecInt clause
Object t
public transient org.sat4j.pb.tools.DisjunctionRHS disjunction (java.lang.Object[])
Object[] lhs
org.sat4j.specs.IVecInt literals
Object t
public transient void atLeast (java.lang.Object, int, java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object name
int i
Object[] things
org.sat4j.specs.IVecInt literals
Object t
public transient org.sat4j.pb.tools.ImplicationNamer atMost (int, java.lang.Object[]) throws org.sat4j.specs.ContradictionException
int i
Object[] things
org.sat4j.specs.IVec toName
org.sat4j.specs.IVecInt literals
Object t
public transient void atMost (java.lang.Object, int, java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object name
int i
Object[] things
org.sat4j.specs.IVecInt literals
Object t
public transient void clause (java.lang.Object, java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object name
Object[] things
org.sat4j.specs.IVecInt literals
Object t
org.sat4j.specs.IConstr constr
public transient void iff (java.lang.Object, java.lang.Object, java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object name
Object thing
Object[] otherThings
org.sat4j.specs.IVecInt literals
Object t
org.sat4j.specs.IConstr[] constrs
org.sat4j.specs.IConstr constr
public transient void and (java.lang.Object, java.lang.Object, java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object name
Object thing
Object[] otherThings
org.sat4j.specs.IVecInt literals
Object t
org.sat4j.specs.IConstr[] constrs
org.sat4j.specs.IConstr constr
public transient void or (java.lang.Object, java.lang.Object, java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object name
Object thing
Object[] otherThings
org.sat4j.specs.IVecInt literals
Object t
org.sat4j.specs.IConstr[] constrs
org.sat4j.specs.IConstr constr
public transient void halfOr (java.lang.Object, java.lang.Object, java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object name
Object thing
Object[] otherThings
org.sat4j.specs.IVecInt literals
Object t
org.sat4j.specs.IConstr[] constrs
org.sat4j.specs.IConstr constr
public void ifThenElse (java.lang.Object, java.lang.Object, java.lang.Object, java.lang.Object, java.lang.Object) throws org.sat4j.specs.ContradictionException
Object name
Object thing
Object conditionThing
Object thenThing
Object elseThing
org.sat4j.specs.IConstr[] constrs
org.sat4j.specs.IConstr constr
public transient void setObjectiveFunction (org.sat4j.pb.tools.WeightedObject[])
org.sat4j.pb.tools.WeightedObject[] wobj
org.sat4j.pb.tools.WeightedObject wo
private void addProperly (java.lang.Object, java.math.BigInteger)
Object thing
java.math.BigInteger weight
int lit
int index
private void createObjectivetiveFunctionIfNeeded (int)
int n
public void addToObjectiveFunction (java.lang.Object, int)
Object thing
int weight
public void addToObjectiveFunction (java.lang.Object, java.math.BigInteger)
Object thing
java.math.BigInteger weight
public transient void atLeast (java.lang.Object, java.math.BigInteger, org.sat4j.pb.tools.WeightedObject[]) throws org.sat4j.specs.ContradictionException
Object name
java.math.BigInteger degree
org.sat4j.pb.tools.WeightedObject[] wobj
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
org.sat4j.pb.tools.WeightedObject wo
public transient void atMost (java.lang.Object, java.math.BigInteger, org.sat4j.pb.tools.WeightedObject[]) throws org.sat4j.specs.ContradictionException
Object name
java.math.BigInteger degree
org.sat4j.pb.tools.WeightedObject[] wobj
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
org.sat4j.pb.tools.WeightedObject wo
public transient void atMost (java.lang.Object, int, org.sat4j.pb.tools.WeightedObject[]) throws org.sat4j.specs.ContradictionException
Object name
int degree
org.sat4j.pb.tools.WeightedObject[] wobj
public void stopSolver ()
public void stopExplanation ()
public void discard (org.sat4j.specs.IVec) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVec things
org.sat4j.specs.IVecInt literals
java.util.Iterator it
public void discardSolutionsWithObjectiveValueGreaterThan (long) throws org.sat4j.specs.ContradictionException
long value
org.sat4j.pb.ObjectiveFunction obj
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
public java.lang.String getObjectiveFunction ()
org.sat4j.pb.ObjectiveFunction obj
StringBuffer stb
int i
public int getNumberOfVariables ()
public int getNumberOfConstraints ()
public java.util.Map getMappingToDomain ()
public java.lang.Object not (java.lang.Object)
Object thing
public org.sat4j.pb.IPBSolver getSolver ()
public void reset ()
public void impliedBy (java.util.Collection, java.util.Collection, java.util.Collection) throws org.sat4j.specs.TimeoutException
java.util.Collection assumptions
java.util.Collection satisfied
java.util.Collection falsified
org.sat4j.specs.IVecInt assump
Object thing
org.sat4j.specs.IVecInt implied
int p
org.sat4j.specs.IteratorInt it
}
org/sat4j/pb/tools/PBAdapter.classPBAdapter.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.PBAdapter extends org.sat4j.tools.SolverDecorator implements org.sat4j.pb.IPBSolver {
private static final long serialVersionUID
public void (org.sat4j.specs.ISolver)
org.sat4j.specs.ISolver solver
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
}
org/sat4j/pb/tools/DisjunctionRHS.classDisjunctionRHS.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.DisjunctionRHS extends java.lang.Object {
private final org.sat4j.specs.IVecInt literals
private final org.sat4j.pb.tools.DependencyHelper helper
private final org.sat4j.specs.IVec toName
public void (org.sat4j.pb.tools.DependencyHelper, org.sat4j.specs.IVecInt)
org.sat4j.pb.tools.DependencyHelper helper
org.sat4j.specs.IVecInt literals
public transient org.sat4j.pb.tools.ImplicationNamer implies (java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object[] things
org.sat4j.specs.IVecInt clause
Object t
int p
org.sat4j.specs.IConstr constr
org.sat4j.specs.IteratorInt it
}
org/sat4j/pb/tools/DependencyHelper$Negation.classDependencyHelper.java
package org.sat4j.pb.tools
final org.sat4j.pb.tools.DependencyHelper$Negation extends java.lang.Object {
private final Object thing
void (java.lang.Object)
Object thing
java.lang.Object getThing ()
public java.lang.String toString ()
}
org/sat4j/pb/tools/ClausalConstraintsDecorator.classClausalConstraintsDecorator.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.ClausalConstraintsDecorator extends org.sat4j.tools.ClausalCardinalitiesDecorator implements org.sat4j.pb.IPBSolver {
private static final long serialVersionUID
private final org.sat4j.pb.IPBSolver solver
public void (org.sat4j.pb.IPBSolver, org.sat4j.tools.encoding.EncodingStrategyAdapter)
org.sat4j.pb.IPBSolver solver
org.sat4j.tools.encoding.EncodingStrategyAdapter encodingAd
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
public static boolean isCardinality (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt coeffs
boolean result
int i
public static boolean isCardinality (org.sat4j.specs.IVec)
org.sat4j.specs.IVec coeffs
boolean result
int i
}
org/sat4j/pb/tools/ImplicationRHS.classImplicationRHS.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.ImplicationRHS extends java.lang.Object {
private final org.sat4j.specs.IVecInt clause
private final org.sat4j.pb.tools.DependencyHelper helper
private final org.sat4j.specs.IVec toName
public void (org.sat4j.pb.tools.DependencyHelper, org.sat4j.specs.IVecInt)
org.sat4j.pb.tools.DependencyHelper helper
org.sat4j.specs.IVecInt clause
public org.sat4j.pb.tools.ImplicationAnd implies (java.lang.Object) throws org.sat4j.specs.ContradictionException
Object thing
org.sat4j.pb.tools.ImplicationAnd and
public transient org.sat4j.pb.tools.ImplicationNamer implies (java.lang.Object[]) throws org.sat4j.specs.ContradictionException
Object[] things
Object t
public org.sat4j.pb.tools.ImplicationAnd impliesNot (java.lang.Object) throws org.sat4j.specs.ContradictionException
Object thing
org.sat4j.pb.tools.ImplicationAnd and
}
org/sat4j/pb/tools/ConflictTracing.classConflictTracing.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.ConflictTracing extends org.sat4j.tools.SearchListenerAdapter {
private static final long serialVersionUID
private final String filename
private java.io.PrintStream out
private long index
public void (java.lang.String)
String filename
private void updateWriter ()
public void learn (org.sat4j.specs.IConstr)
org.sat4j.specs.IConstr c
org.sat4j.pb.constraints.pb.PBConstr myConstr
}
org/sat4j/pb/tools/SearchOptimizerListener.classSearchOptimizerListener.java
package org.sat4j.pb.tools
public final org.sat4j.pb.tools.SearchOptimizerListener extends org.sat4j.tools.SearchListenerAdapter {
private static final long serialVersionUID
private org.sat4j.pb.IPBSolverService solverService
private org.sat4j.pb.ObjectiveFunction obj
private final org.sat4j.tools.SolutionFoundListener sfl
private java.math.BigInteger currentValue
private org.sat4j.specs.IConstr prevConstr
public void (org.sat4j.tools.SolutionFoundListener)
org.sat4j.tools.SolutionFoundListener sfl
public void init (org.sat4j.pb.IPBSolverService)
org.sat4j.pb.IPBSolverService solverService
public void solutionFound (int[], org.sat4j.specs.RandomAccessModel)
int[] model
org.sat4j.specs.RandomAccessModel lazyModel
public void end (org.sat4j.specs.Lbool)
org.sat4j.specs.Lbool result
public java.lang.String toString ()
public volatile void init (org.sat4j.specs.ISolverService)
}
org/sat4j/pb/tools/ImplicationAnd.classImplicationAnd.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.ImplicationAnd extends java.lang.Object {
private final org.sat4j.pb.tools.DependencyHelper helper
private final org.sat4j.specs.IVecInt clause
private final org.sat4j.specs.IVec toName
public void (org.sat4j.pb.tools.DependencyHelper, org.sat4j.specs.IVecInt)
org.sat4j.pb.tools.DependencyHelper helper
org.sat4j.specs.IVecInt clause
public org.sat4j.pb.tools.ImplicationAnd and (java.lang.Object) throws org.sat4j.specs.ContradictionException
Object thing
org.sat4j.specs.IVecInt tmpClause
org.sat4j.specs.IConstr constr
public org.sat4j.pb.tools.ImplicationAnd andNot (java.lang.Object) throws org.sat4j.specs.ContradictionException
Object thing
org.sat4j.specs.IVecInt tmpClause
org.sat4j.specs.IConstr constr
public void named (java.lang.Object)
Object name
java.util.Iterator it
}
org/sat4j/pb/tools/XplainPB.classXplainPB.java
package org.sat4j.pb.tools
public org.sat4j.pb.tools.XplainPB extends org.sat4j.tools.xplain.Xplain implements org.sat4j.pb.IPBSolver {
private static final long serialVersionUID
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
org.sat4j.specs.IVecInt coeffs
int newvar
org.sat4j.specs.IConstr constr
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
org.sat4j.specs.IVecInt coeffs
int newvar
org.sat4j.specs.IConstr constr
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int n
int newvar
org.sat4j.specs.IVecInt coeffs
org.sat4j.specs.IConstr constr1
org.sat4j.specs.IConstr constr2
org.sat4j.core.ConstrGroup group
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
int newvar
java.math.BigInteger sum
java.util.Iterator ite
org.sat4j.specs.IConstr constr
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
}
org/sat4j/pb/LPStringSolver.classLPStringSolver.java
package org.sat4j.pb
public org.sat4j.pb.LPStringSolver extends org.sat4j.tools.DimacsStringSolver implements org.sat4j.pb.IPBSolver {
private static final String FAKE_I_CONSTR_MSG
private static final long serialVersionUID
private int indxConstrObj
private int nbOfConstraints
private org.sat4j.pb.ObjectiveFunction obj
private boolean inserted
private static final org.sat4j.specs.IConstr FAKE_CONSTR
static final boolean $assertionsDisabled
static void ()
public void ()
public void (int)
int initSize
public boolean isSatisfiable (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
org.sat4j.specs.IteratorInt it
int p
public boolean isSatisfiable (org.sat4j.specs.IVecInt, boolean) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
boolean global
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
StringBuffer out
int negationweight
int p
boolean first
org.sat4j.specs.IteratorInt iterator
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
StringBuffer out
int negationweight
int p
boolean first
org.sat4j.specs.IteratorInt iterator
public org.sat4j.specs.IConstr addClause (org.sat4j.specs.IVecInt) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
StringBuffer out
int lit
boolean first
int negationweight
org.sat4j.specs.IteratorInt iterator
public java.lang.String getExplanation ()
public void setListOfVariablesForExplanation (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt listOfVariables
public void objectiveFunctionToLP (org.sat4j.pb.ObjectiveFunction, java.lang.StringBuffer)
org.sat4j.pb.ObjectiveFunction obj
StringBuffer buffer
org.sat4j.specs.IVecInt variables
org.sat4j.specs.IVec coeffs
int n
java.math.BigInteger coeff
int i
public java.lang.String toString ()
StringBuffer out
StringBuffer tmp
int i
public java.lang.String toString (java.lang.String)
String prefix
public int newVar (int)
int howmany
StringBuffer out
public void setExpectedNumberOfClauses (int)
int nb
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public int nConstraints ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
StringBuffer out
int n
int coeff
int i
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
StringBuffer out
int n
java.math.BigInteger coeff
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
StringBuffer out
int n
int coeff
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
StringBuffer out
int n
java.math.BigInteger coeff
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
StringBuffer out
int n
int coeff
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
StringBuffer out
int n
java.math.BigInteger coeff
int i
}
org/sat4j/pb/constraints/CompetResolutionPBLongMixedWLClauseCardConstrDataStructure.classCompetResolutionPBLongMixedWLClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/AtLeastCardPBConstructor.classAtLeastCardPBConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.AtLeastCardPBConstructor extends java.lang.Object implements org.sat4j.pb.constraints.ICardConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructCard (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt theLits
int degree
public org.sat4j.minisat.core.Constr constructLearntCard (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
org.sat4j.specs.IVecInt resLits
org.sat4j.specs.IVec resCoefs
}
org/sat4j/pb/constraints/UnitBinaryHTClausePBConstructor.classUnitBinaryHTClausePBConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.UnitBinaryHTClausePBConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IClauseConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructClause (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt v
public org.sat4j.minisat.core.Constr constructLearntClause (org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt literals
}
org/sat4j/pb/constraints/UnitBinaryWLClauseConstructor.classUnitBinaryWLClauseConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.UnitBinaryWLClauseConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IClauseConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructClause (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt v
public org.sat4j.minisat.core.Constr constructLearntClause (org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt literals
}
org/sat4j/pb/constraints/IPBConstructor.classIPBConstructor.java
package org.sat4j.pb.constraints
public abstract org.sat4j.pb.constraints.IPBConstructor extends java.lang.Object {
public abstract org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
public abstract org.sat4j.minisat.core.Constr constructPB (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
}
org/sat4j/pb/constraints/pb/MinWatchPbLongCP.classMinWatchPbLongCP.java
package org.sat4j.pb.constraints.pb
public org.sat4j.pb.constraints.pb.MinWatchPbLongCP extends org.sat4j.pb.constraints.pb.WatchPbLongCP {
private static final long serialVersionUID
protected long watchCumul
protected boolean[] watched
protected int[] watching
protected int watchingCount
static final boolean $assertionsDisabled
static void ()
protected void (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
protected void (org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
protected void computeWatches () throws org.sat4j.specs.ContradictionException
int i
private void watchMoreForLearntConstraint ()
int free
int maxlevel
int maxi
int level
int i
protected void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
int ind
public static org.sat4j.pb.constraints.pb.MinWatchPbLongCP normalizedMinWatchPbNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
org.sat4j.pb.constraints.pb.MinWatchPbLongCP outclause
protected int nbOfWatched ()
int retour
int ind
int i
public boolean propagate (org.sat4j.specs.UnitPropagationListener, int)
org.sat4j.specs.UnitPropagationListener s
int p
int pIndiceWatching
int pIndice
long maxCoef
long upWatchCumul
long limit
int i
public void remove (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener upl
int i
public void undo (int)
int p
int pIndice
public static org.sat4j.pb.constraints.pb.WatchPbLongCP normalizedWatchPbNew (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
protected long maximalCoefficient (int)
int pIndice
long maxCoef
int i
protected long updateWatched (long, int)
long mc
int pIndice
long maxCoef
long upWatchCumul
long degreePlusMaxCoef
int ind
}
org/sat4j/pb/constraints/pb/Pseudos.classPseudos.java
package org.sat4j.pb.constraints.pb
public abstract org.sat4j.pb.constraints.pb.Pseudos extends java.lang.Object {
static final boolean $assertionsDisabled
static void ()
public void ()
public static org.sat4j.pb.constraints.pb.IDataStructurePB niceCheckedParameters (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger, org.sat4j.minisat.core.ILits)
org.sat4j.specs.IVecInt ps
org.sat4j.specs.IVec bigCoefs
boolean moreThan
java.math.BigInteger bigDeg
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] bc
java.math.BigInteger bigDegree
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
public static java.math.BigInteger niceCheckedParametersForCompetition (int[], java.math.BigInteger[], boolean, java.math.BigInteger)
int[] lits
java.math.BigInteger[] bc
boolean moreThan
java.math.BigInteger bigDeg
java.math.BigInteger bigDegree
int i
int i
int i
public static org.sat4j.pb.constraints.pb.IDataStructurePB niceParameters (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger, org.sat4j.minisat.core.ILits) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt ps
org.sat4j.specs.IVec bigCoefs
boolean moreThan
java.math.BigInteger bigDeg
org.sat4j.minisat.core.ILits voc
public static java.math.BigInteger niceParametersForCompetition (int[], java.math.BigInteger[], boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
int[] ps
java.math.BigInteger[] bigCoefs
boolean moreThan
java.math.BigInteger bigDeg
public static org.sat4j.specs.IVec toVecBigInt (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt vec
org.sat4j.specs.IVec bigVec
int i
public static java.math.BigInteger toBigInt (int)
int i
public static org.sat4j.pb.ObjectiveFunction normalizeObjective (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction initial
org.sat4j.specs.IVec initCoeffs
org.sat4j.specs.IVecInt initLits
java.util.Map reduced
int lit
int i
java.math.BigInteger oldCoef
org.sat4j.specs.IVecInt newLits
org.sat4j.specs.IVec newCoefs
java.util.Map$Entry entry
}
org/sat4j/pb/constraints/pb/PuebloMinWatchPb.classPuebloMinWatchPb.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.PuebloMinWatchPb extends org.sat4j.pb.constraints.pb.MinWatchPb {
private static final long serialVersionUID
static final boolean $assertionsDisabled
static void ()
private void (org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
private void (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
public static org.sat4j.pb.constraints.pb.PuebloMinWatchPb normalizedMinWatchPbNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
java.math.BigInteger c
org.sat4j.pb.constraints.pb.PuebloMinWatchPb outclause
public static org.sat4j.pb.constraints.pb.WatchPb normalizedWatchPbNew (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
protected java.math.BigInteger maximalCoefficient (int)
int pIndice
protected java.math.BigInteger updateWatched (java.math.BigInteger, int)
java.math.BigInteger mc
int pIndice
java.math.BigInteger maxCoef
java.math.BigInteger upWatchCumul
java.math.BigInteger borneSup
int ind
}
org/sat4j/pb/constraints/pb/ConflictMap.classConflictMap.java
package org.sat4j.pb.constraints.pb
public org.sat4j.pb.constraints.pb.ConflictMap extends org.sat4j.pb.constraints.pb.MapPb implements org.sat4j.pb.constraints.pb.IConflict {
private final org.sat4j.minisat.core.ILits voc
protected boolean hasBeenReduced
protected long numberOfReductions
protected java.math.BigInteger currentSlack
protected int currentLevel
protected org.sat4j.core.VecInt[] byLevel
protected java.math.BigInteger coefMult
protected java.math.BigInteger coefMultCons
private java.math.BigInteger possReducedCoefs
static final boolean $assertionsDisabled
static void ()
public static org.sat4j.pb.constraints.pb.IConflict createConflict (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr cpb
int level
void (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr cpb
int level
private void initStructures ()
int ilit
int litLevel
int index
java.math.BigInteger tmp
int i
private static int levelToIndex (int)
int level
private static int indexToLevel (int)
int indLevel
public java.math.BigInteger resolve (org.sat4j.pb.constraints.pb.PBConstr, int, org.sat4j.minisat.core.VarActivityListener)
org.sat4j.pb.constraints.pb.PBConstr cpb
int litImplied
org.sat4j.minisat.core.VarActivityListener val
int nLitImplied
int litLevel
int lit
java.math.BigInteger[] coefsCons
java.math.BigInteger degreeCons
int ind
org.sat4j.pb.constraints.pb.IWatchPb wpb
int i
protected java.math.BigInteger reduceUntilConflict (int, int, java.math.BigInteger[], org.sat4j.pb.constraints.pb.IWatchPb)
int litImplied
int ind
java.math.BigInteger[] reducedCoefs
org.sat4j.pb.constraints.pb.IWatchPb wpb
java.math.BigInteger slackResolve
java.math.BigInteger slackThis
java.math.BigInteger slackIndex
java.math.BigInteger slackConflict
java.math.BigInteger ppcm
java.math.BigInteger reducedDegree
java.math.BigInteger previousCoefLitImplied
java.math.BigInteger tmp
java.math.BigInteger coefLitImplied
private java.math.BigInteger possConstraint (org.sat4j.pb.constraints.pb.IWatchPb, java.math.BigInteger[])
org.sat4j.pb.constraints.pb.IWatchPb wpb
java.math.BigInteger[] theCoefs
java.math.BigInteger poss
int i
public java.math.BigInteger slackConflict ()
java.math.BigInteger poss
java.math.BigInteger tmp
int i
public boolean oldIsAssertive (int)
int dl
java.math.BigInteger tmp
int lit
java.math.BigInteger slack
int i
private java.math.BigInteger computeSlack (int)
int dl
java.math.BigInteger slack
int lit
java.math.BigInteger tmp
int i
public boolean isAssertive (int)
int dl
java.math.BigInteger slack
private boolean isImplyingLiteral (java.math.BigInteger)
java.math.BigInteger slack
int unassigned
int lit
int lit
org.sat4j.specs.IteratorInt iterator
java.math.BigInteger tmp
int level
org.sat4j.specs.IteratorInt iterator
private boolean isImplyingLiteralOrdered (int, java.math.BigInteger)
int dl
java.math.BigInteger slack
int ilit
int litLevel
int i
protected static java.math.BigInteger ppcm (java.math.BigInteger, java.math.BigInteger)
java.math.BigInteger a
java.math.BigInteger b
public java.math.BigInteger reduceInConstraint (org.sat4j.pb.constraints.pb.IWatchPb, java.math.BigInteger[], int, java.math.BigInteger)
org.sat4j.pb.constraints.pb.IWatchPb wpb
java.math.BigInteger[] coefsBis
int indLitImplied
java.math.BigInteger degreeBis
int lit
int size
int ind
int ind
java.math.BigInteger degUpdate
private java.math.BigInteger saturation (java.math.BigInteger[], java.math.BigInteger, org.sat4j.pb.constraints.pb.IWatchPb)
java.math.BigInteger[] coefs
java.math.BigInteger degree
org.sat4j.pb.constraints.pb.IWatchPb wpb
java.math.BigInteger degreeResult
boolean isMinimumEqualsToDegree
int comparison
int i
int i
private static boolean positiveCoefs (java.math.BigInteger[])
java.math.BigInteger[] coefsCons
java.math.BigInteger coefsCon
public int getBacktrackLevel (int)
int maxLevel
org.sat4j.core.VecInt lits
int level
int indStop
int indStart
java.math.BigInteger slack
int previous
int indLevel
int lit
org.sat4j.specs.IteratorInt iterator
public int oldGetBacktrackLevel (int)
int maxLevel
int litLevel
int litLevel
int borneMax
int borneMin
int i
int retour
int i
public void updateSlack (int)
int level
int dl
int lit
org.sat4j.specs.IteratorInt iterator
void increaseCoef (int, java.math.BigInteger)
int lit
java.math.BigInteger incCoef
void decreaseCoef (int, java.math.BigInteger)
int lit
java.math.BigInteger decCoef
void setCoef (int, java.math.BigInteger)
int lit
java.math.BigInteger newValue
int litLevel
int indLitLevel
void changeCoef (int, java.math.BigInteger)
int indLit
java.math.BigInteger newValue
int lit
int litLevel
int indLitLevel
void removeCoef (int)
int lit
int litLevel
int indLitLevel
private int getLevelByLevel (int)
int lit
int i
public boolean slackIsCorrect (int)
int dl
public java.lang.String toString ()
int lit
StringBuffer stb
int i
public boolean hasBeenReduced ()
public long getNumberOfReductions ()
}
org/sat4j/pb/constraints/pb/UnitClausePB.classUnitClausePB.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.UnitClausePB extends org.sat4j.minisat.constraints.cnf.UnitClause implements org.sat4j.pb.constraints.pb.PBConstr {
private final org.sat4j.minisat.core.ILits voc
private static final long serialVersionUID
public void (int, org.sat4j.minisat.core.ILits)
int value
org.sat4j.minisat.core.ILits voc
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
public java.math.BigInteger getCoef (int)
int p
public java.math.BigInteger[] getCoefs ()
public java.math.BigInteger getDegree ()
public int[] getLits ()
public org.sat4j.minisat.core.ILits getVocabulary ()
}
org/sat4j/pb/constraints/pb/MinWatchPb.classMinWatchPb.java
package org.sat4j.pb.constraints.pb
public org.sat4j.pb.constraints.pb.MinWatchPb extends org.sat4j.pb.constraints.pb.WatchPb {
private static final long serialVersionUID
protected java.math.BigInteger watchCumul
protected boolean[] watched
protected int[] watching
protected int watchingCount
static final boolean $assertionsDisabled
static void ()
protected void (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
protected void (org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
protected void computeWatches () throws org.sat4j.specs.ContradictionException
int i
private void watchMoreForLearntConstraint ()
int free
int maxlevel
int maxi
int level
int i
protected void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
int ind
public static org.sat4j.pb.constraints.pb.MinWatchPb normalizedMinWatchPbNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
org.sat4j.pb.constraints.pb.MinWatchPb outclause
protected int nbOfWatched ()
int retour
int ind
int i
public boolean propagate (org.sat4j.specs.UnitPropagationListener, int)
org.sat4j.specs.UnitPropagationListener s
int p
int pIndiceWatching
int pIndice
java.math.BigInteger maxCoef
java.math.BigInteger upWatchCumul
java.math.BigInteger limit
int i
public void remove (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener upl
int i
public void undo (int)
int p
int pIndice
public static org.sat4j.pb.constraints.pb.WatchPb normalizedWatchPbNew (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
protected java.math.BigInteger maximalCoefficient (int)
int pIndice
java.math.BigInteger maxCoef
int i
protected java.math.BigInteger updateWatched (java.math.BigInteger, int)
java.math.BigInteger mc
int pIndice
java.math.BigInteger maxCoef
java.math.BigInteger upWatchCumul
java.math.BigInteger degreePlusMaxCoef
int ind
}
org/sat4j/pb/constraints/pb/ConflictMapCardinality.classConflictMapCardinality.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.ConflictMapCardinality extends org.sat4j.pb.constraints.pb.ConflictMap {
public void (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr cpb
int level
}
org/sat4j/pb/constraints/pb/OriginalHTClausePB.classOriginalHTClausePB.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.OriginalHTClausePB extends org.sat4j.minisat.constraints.cnf.OriginalHTClause implements org.sat4j.pb.constraints.pb.PBConstr {
private static final long serialVersionUID
public void (org.sat4j.specs.IVecInt, org.sat4j.minisat.core.ILits)
org.sat4j.specs.IVecInt ps
org.sat4j.minisat.core.ILits voc
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
public java.math.BigInteger getCoef (int)
int literal
public java.math.BigInteger[] getCoefs ()
java.math.BigInteger[] tmp
int i
public java.math.BigInteger getDegree ()
public static org.sat4j.pb.constraints.pb.OriginalHTClausePB brandNewClause (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt literals
org.sat4j.pb.constraints.pb.OriginalHTClausePB c
public static volatile org.sat4j.minisat.constraints.cnf.OriginalHTClause brandNewClause (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
}
org/sat4j/pb/constraints/pb/UnitClausesPB.classUnitClausesPB.java
package org.sat4j.pb.constraints.pb
public org.sat4j.pb.constraints.pb.UnitClausesPB extends org.sat4j.minisat.constraints.cnf.UnitClauses implements org.sat4j.pb.constraints.pb.PBConstr {
public void (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt values
public java.math.BigInteger getCoef (int)
int literal
public java.math.BigInteger getDegree ()
public org.sat4j.minisat.core.ILits getVocabulary ()
public int[] getLits ()
public java.math.BigInteger[] getCoefs ()
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
}
org/sat4j/pb/constraints/pb/MaxWatchPb.classMaxWatchPb.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.MaxWatchPb extends org.sat4j.pb.constraints.pb.WatchPb {
private static final long serialVersionUID
public static final int LIMIT_FOR_MAP
private java.math.BigInteger watchCumul
private final java.util.Map litToCoeffs
static final boolean $assertionsDisabled
static void ()
private void (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
int i
private void (org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
int i
protected void computeWatches () throws org.sat4j.specs.ContradictionException
int i
protected void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
int ind
public boolean propagate (org.sat4j.specs.UnitPropagationListener, int)
org.sat4j.specs.UnitPropagationListener s
int p
java.math.BigInteger coefP
java.math.BigInteger coefP
int indiceP
java.math.BigInteger newcumul
int ind
java.math.BigInteger limit
public void remove (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener upl
int i
public void undo (int)
int p
java.math.BigInteger coefP
java.math.BigInteger coefP
int indiceP
public static org.sat4j.pb.constraints.pb.MaxWatchPb normalizedMaxWatchPbNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
org.sat4j.pb.constraints.pb.MaxWatchPb outclause
public static org.sat4j.pb.constraints.pb.WatchPb normalizedWatchPbNew (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
}
org/sat4j/pb/constraints/pb/InternalMapPBStructure.classInternalMapPBStructure.java
package org.sat4j.pb.constraints.pb
public org.sat4j.pb.constraints.pb.InternalMapPBStructure extends java.lang.Object {
private final org.sat4j.specs.IVecInt lits
private final org.sat4j.specs.IVec coefs
private org.sat4j.specs.IVecInt allLits
static final boolean $assertionsDisabled
static void ()
void (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec)
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coefs
void (int)
int size
void (org.sat4j.pb.constraints.pb.PBConstr)
org.sat4j.pb.constraints.pb.PBConstr cpb
int lit
int i
java.math.BigInteger get (int)
int lit
int getFromAllLits (int)
int lit
int getLit (int)
int indLit
java.math.BigInteger getCoef (int)
int indLit
boolean containsKey (int)
int lit
int size ()
void put (int, java.math.BigInteger)
int lit
java.math.BigInteger newValue
int indLit
void changeCoef (int, java.math.BigInteger)
int indLit
java.math.BigInteger newValue
void remove (int)
int lit
int indLit
int tmp
void copyCoefs (org.sat4j.specs.IVec)
org.sat4j.specs.IVec dest
void copyCoefs (java.math.BigInteger[])
java.math.BigInteger[] dest
void copyLits (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt dest
void copyLits (int[])
int[] dest
}
org/sat4j/pb/constraints/pb/IConflict.classIConflict.java
package org.sat4j.pb.constraints.pb
public abstract org.sat4j.pb.constraints.pb.IConflict extends java.lang.Object implements org.sat4j.pb.constraints.pb.IDataStructurePB {
public abstract java.math.BigInteger resolve (org.sat4j.pb.constraints.pb.PBConstr, int, org.sat4j.minisat.core.VarActivityListener)
public abstract java.math.BigInteger slackConflict ()
public abstract boolean isAssertive (int)
public abstract java.math.BigInteger reduceInConstraint (org.sat4j.pb.constraints.pb.IWatchPb, java.math.BigInteger[], int, java.math.BigInteger)
public abstract int getBacktrackLevel (int)
public abstract void updateSlack (int)
public abstract boolean slackIsCorrect (int)
}
org/sat4j/pb/constraints/pb/MaxWatchPbLongCP.classMaxWatchPbLongCP.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.MaxWatchPbLongCP extends org.sat4j.pb.constraints.pb.WatchPbLongCP {
private static final long serialVersionUID
private long watchCumul
private final java.util.Map litToCoeffs
static final boolean $assertionsDisabled
static void ()
private void (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
int i
private void (org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
int i
protected void computeWatches () throws org.sat4j.specs.ContradictionException
int i
protected void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
int ind
public boolean propagate (org.sat4j.specs.UnitPropagationListener, int)
org.sat4j.specs.UnitPropagationListener s
int p
long coefP
long coefP
int indiceP
long newcumul
int ind
long limit
public void remove (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener upl
int i
public void undo (int)
int p
long coefP
long coefP
long coefP
int indiceP
Long coefL
public static org.sat4j.pb.constraints.pb.MaxWatchPbLongCP normalizedMaxWatchPbNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
org.sat4j.pb.constraints.pb.MaxWatchPbLongCP outclause
public static org.sat4j.pb.constraints.pb.WatchPbLongCP normalizedWatchPbNew (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
}
org/sat4j/pb/constraints/pb/WatchPbLongCP.classWatchPbLongCP.java
package org.sat4j.pb.constraints.pb
public abstract org.sat4j.pb.constraints.pb.WatchPbLongCP extends java.lang.Object implements org.sat4j.pb.constraints.pb.IWatchPb org.sat4j.minisat.core.Propagatable org.sat4j.minisat.core.Undoable java.io.Serializable {
private static final long serialVersionUID
private static final int LIMIT_SELECTION_SORT
protected double activity
protected java.math.BigInteger[] bigCoefs
protected java.math.BigInteger bigDegree
protected long[] coefs
protected long sumcoefs
protected long degree
protected int[] lits
protected boolean learnt
protected org.sat4j.minisat.core.ILits voc
static final boolean $assertionsDisabled
static void ()
void ()
void (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
int size
long c
void (int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
public static long[] toLong (java.math.BigInteger[])
java.math.BigInteger[] bigValues
long[] res
int i
public boolean isAssertive (int)
int dl
long slack
int i
int i
public void calcReason (int, org.sat4j.specs.IVecInt)
int p
org.sat4j.specs.IVecInt outReason
long sumfalsified
int[] mlits
int i
int q
protected abstract void computeWatches () throws org.sat4j.specs.ContradictionException
protected abstract void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
public int get (int)
int i
public double getActivity ()
public void incActivity (double)
double claInc
public void setActivity (double)
double d
public long slackConstraint ()
public long slackConstraint (long[], long)
long[] theCoefs
long theDegree
public long computeLeftSide (long[])
long[] theCoefs
long poss
int i
public java.math.BigInteger computeLeftSide (java.math.BigInteger[])
java.math.BigInteger[] theCoefs
java.math.BigInteger poss
int i
public long computeLeftSide ()
protected boolean isSatisfiable ()
public boolean learnt ()
public boolean locked ()
int p
protected static java.math.BigInteger ppcm (java.math.BigInteger, java.math.BigInteger)
java.math.BigInteger a
java.math.BigInteger b
public void rescaleBy (double)
double d
void selectionSort (int, int)
int from
int to
int i
int j
int bestIndex
long tmp
java.math.BigInteger bigTmp
int tmp2
public void setLearnt ()
public boolean simplify ()
long cumul
int i
public final int size ()
protected final void sort ()
protected final void sort (int, int)
int from
int to
int width
int indPivot
long pivot
int litPivot
long tmp
java.math.BigInteger bigTmp
int i
int j
int tmp2
public java.lang.String toString ()
StringBuffer stb
int i
public void assertConstraint (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
long tmp
int i
boolean ret
public void assertConstraintIfNeeded (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
public void register ()
public int[] getLits ()
int[] litsBis
public org.sat4j.minisat.core.ILits getVocabulary ()
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
long cptCoefs
int index
org.sat4j.specs.IVecInt literals
int j
public boolean coefficientsEqualToOne ()
public boolean equals (java.lang.Object)
Object pb
org.sat4j.pb.constraints.pb.WatchPbLongCP wpb
int lit
boolean ok
int ilit
int ilit2
public int hashCode ()
long sum
int p
public void forwardActivity (double)
double claInc
public long[] getLongCoefs ()
long[] coefsBis
public java.math.BigInteger slackConstraint (java.math.BigInteger[], java.math.BigInteger)
java.math.BigInteger[] theCoefs
java.math.BigInteger theDegree
public java.math.BigInteger getCoef (int)
int i
public java.math.BigInteger[] getCoefs ()
java.math.BigInteger[] coefsBis
public java.math.BigInteger getDegree ()
public boolean canBePropagatedMultipleTimes ()
public org.sat4j.minisat.core.Constr toConstraint ()
public void calcReasonOnTheFly (int, org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt)
int p
org.sat4j.specs.IVecInt trail
org.sat4j.specs.IVecInt outReason
}
org/sat4j/pb/constraints/pb/WatchPbLong$1.classWatchPbLong.java
package org.sat4j.pb.constraints.pb
org.sat4j.pb.constraints.pb.WatchPbLong$1 extends java.lang.Object implements java.util.Comparator {
final org.sat4j.pb.constraints.pb.WatchPbLong this$0
void (org.sat4j.pb.constraints.pb.WatchPbLong)
public int compare (java.lang.Integer, java.lang.Integer)
Integer o1
Integer o2
public volatile int compare (java.lang.Object, java.lang.Object)
}
org/sat4j/pb/constraints/pb/WatchPb.classWatchPb.java
package org.sat4j.pb.constraints.pb
public abstract org.sat4j.pb.constraints.pb.WatchPb extends java.lang.Object implements org.sat4j.pb.constraints.pb.IWatchPb org.sat4j.minisat.core.Propagatable org.sat4j.minisat.core.Undoable java.io.Serializable {
private static final long serialVersionUID
private static final int LIMIT_SELECTION_SORT
protected double activity
protected java.math.BigInteger[] coefs
protected java.math.BigInteger sumcoefs
protected java.math.BigInteger degree
protected int[] lits
protected boolean learnt
protected org.sat4j.minisat.core.ILits voc
static final boolean $assertionsDisabled
static void ()
void ()
void (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
int size
java.math.BigInteger c
void (int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
public boolean isAssertive (int)
int dl
java.math.BigInteger slack
int i
int i
public void calcReason (int, org.sat4j.specs.IVecInt)
int p
org.sat4j.specs.IVecInt outReason
java.math.BigInteger sumfalsified
int[] mlits
int i
int q
protected abstract void computeWatches () throws org.sat4j.specs.ContradictionException
protected abstract void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
public int get (int)
int i
public java.math.BigInteger getCoef (int)
int i
public double getActivity ()
public void incActivity (double)
double claInc
public void setActivity (double)
double d
public java.math.BigInteger slackConstraint ()
public java.math.BigInteger slackConstraint (java.math.BigInteger[], java.math.BigInteger)
java.math.BigInteger[] theCoefs
java.math.BigInteger theDegree
public java.math.BigInteger computeLeftSide (java.math.BigInteger[])
java.math.BigInteger[] theCoefs
java.math.BigInteger poss
int i
public java.math.BigInteger computeLeftSide ()
protected boolean isSatisfiable ()
public boolean learnt ()
public boolean locked ()
int p
protected static java.math.BigInteger ppcm (java.math.BigInteger, java.math.BigInteger)
java.math.BigInteger a
java.math.BigInteger b
public void rescaleBy (double)
double d
void selectionSort (int, int)
int from
int to
int i
int j
int bestIndex
java.math.BigInteger tmp
int tmp2
public void setLearnt ()
public boolean simplify ()
java.math.BigInteger cumul
int i
public final int size ()
protected final void sort ()
java.math.BigInteger buffInt
int i
protected final void sort (int, int)
int from
int to
int width
int indPivot
java.math.BigInteger pivot
int litPivot
java.math.BigInteger tmp
int i
int j
int tmp2
public java.lang.String toString ()
StringBuffer stb
int i
public void assertConstraint (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
java.math.BigInteger tmp
int i
boolean ret
public void assertConstraintIfNeeded (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
public java.math.BigInteger getDegree ()
public void register ()
public java.math.BigInteger[] getCoefs ()
java.math.BigInteger[] coefsBis
public int[] getLits ()
int[] litsBis
public org.sat4j.minisat.core.ILits getVocabulary ()
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
java.math.BigInteger cptCoefs
int index
org.sat4j.specs.IVecInt literals
int j
public boolean coefficientsEqualToOne ()
public boolean equals (java.lang.Object)
Object pb
org.sat4j.pb.constraints.pb.WatchPb wpb
int lit
boolean ok
int ilit
int ilit2
public int hashCode ()
long sum
int p
public void forwardActivity (double)
double claInc
public boolean canBePropagatedMultipleTimes ()
public org.sat4j.minisat.core.Constr toConstraint ()
public void calcReasonOnTheFly (int, org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt)
int p
org.sat4j.specs.IVecInt trail
org.sat4j.specs.IVecInt outReason
java.math.BigInteger sumfalsified
org.sat4j.specs.IVecInt vlits
int index
org.sat4j.specs.IteratorInt it
int q
}
org/sat4j/pb/constraints/pb/MapPb.classMapPb.java
package org.sat4j.pb.constraints.pb
public org.sat4j.pb.constraints.pb.MapPb extends java.lang.Object implements org.sat4j.pb.constraints.pb.IDataStructurePB {
protected org.sat4j.pb.constraints.pb.InternalMapPBStructure weightedLits
protected java.math.BigInteger degree
protected int assertiveLiteral
static final boolean $assertionsDisabled
static void ()
void (org.sat4j.pb.constraints.pb.PBConstr)
org.sat4j.pb.constraints.pb.PBConstr cpb
void (int)
int size
public void (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
public boolean isCardinality ()
int i
public boolean isLongSufficient ()
java.math.BigInteger som
int i
public int getAssertiveLiteral ()
public java.math.BigInteger saturation ()
java.math.BigInteger minimum
int ind
int ind
public java.math.BigInteger cuttingPlane (org.sat4j.pb.constraints.pb.PBConstr, java.math.BigInteger, java.math.BigInteger[], org.sat4j.minisat.core.VarActivityListener)
org.sat4j.pb.constraints.pb.PBConstr cpb
java.math.BigInteger deg
java.math.BigInteger[] reducedCoefs
org.sat4j.minisat.core.VarActivityListener val
public java.math.BigInteger cuttingPlane (org.sat4j.pb.constraints.pb.PBConstr, java.math.BigInteger, java.math.BigInteger[], java.math.BigInteger, org.sat4j.minisat.core.VarActivityListener)
org.sat4j.pb.constraints.pb.PBConstr cpb
java.math.BigInteger degreeCons
java.math.BigInteger[] reducedCoefs
java.math.BigInteger coefMult
org.sat4j.minisat.core.VarActivityListener val
int i
int i
public java.math.BigInteger cuttingPlane (int[], java.math.BigInteger[], java.math.BigInteger)
int[] lits
java.math.BigInteger[] reducedCoefs
java.math.BigInteger deg
public java.math.BigInteger cuttingPlane (int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
int[] lits
java.math.BigInteger[] reducedCoefs
java.math.BigInteger degreeCons
java.math.BigInteger coefMult
int i
private void cuttingPlaneStep (int, java.math.BigInteger)
int lit
java.math.BigInteger coef
int nlit
java.math.BigInteger tmp
public void buildConstraintFromConflict (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec)
org.sat4j.specs.IVecInt resLits
org.sat4j.specs.IVec resCoefs
public void buildConstraintFromMapPb (int[], java.math.BigInteger[])
int[] resLits
java.math.BigInteger[] resCoefs
public java.math.BigInteger getDegree ()
public int size ()
public java.lang.String toString ()
StringBuffer stb
int ind
private java.math.BigInteger multiplyCoefficient (java.math.BigInteger, java.math.BigInteger)
java.math.BigInteger coef
java.math.BigInteger mult
void increaseCoef (int, java.math.BigInteger)
int lit
java.math.BigInteger incCoef
void decreaseCoef (int, java.math.BigInteger)
int lit
java.math.BigInteger decCoef
void setCoef (int, java.math.BigInteger)
int lit
java.math.BigInteger newValue
void changeCoef (int, java.math.BigInteger)
int indLit
java.math.BigInteger newValue
void removeCoef (int)
int lit
}
org/sat4j/pb/constraints/pb/ConflictMapClause.classConflictMapClause.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.ConflictMapClause extends org.sat4j.pb.constraints.pb.ConflictMap {
public void (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr cpb
int level
public static org.sat4j.pb.constraints.pb.IConflict createConflict (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr cpb
int level
protected java.math.BigInteger reduceUntilConflict (int, int, java.math.BigInteger[], org.sat4j.pb.constraints.pb.IWatchPb)
int litImplied
int ind
java.math.BigInteger[] reducedCoefs
org.sat4j.pb.constraints.pb.IWatchPb wpb
int i
}
org/sat4j/pb/constraints/pb/IDataStructurePB.classIDataStructurePB.java
package org.sat4j.pb.constraints.pb
public abstract org.sat4j.pb.constraints.pb.IDataStructurePB extends java.lang.Object {
public abstract java.math.BigInteger saturation ()
public abstract java.math.BigInteger cuttingPlane (org.sat4j.pb.constraints.pb.PBConstr, java.math.BigInteger, java.math.BigInteger[], org.sat4j.minisat.core.VarActivityListener)
public abstract java.math.BigInteger cuttingPlane (org.sat4j.pb.constraints.pb.PBConstr, java.math.BigInteger, java.math.BigInteger[], java.math.BigInteger, org.sat4j.minisat.core.VarActivityListener)
public abstract java.math.BigInteger cuttingPlane (int[], java.math.BigInteger[], java.math.BigInteger)
public abstract java.math.BigInteger cuttingPlane (int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
public abstract void buildConstraintFromConflict (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec)
public abstract void buildConstraintFromMapPb (int[], java.math.BigInteger[])
public abstract java.math.BigInteger getDegree ()
public abstract int size ()
public abstract boolean isCardinality ()
public abstract int getAssertiveLiteral ()
public abstract boolean isLongSufficient ()
}
org/sat4j/pb/constraints/pb/PBConstr.classPBConstr.java
package org.sat4j.pb.constraints.pb
public abstract org.sat4j.pb.constraints.pb.PBConstr extends java.lang.Object implements org.sat4j.minisat.core.Constr {
public abstract java.math.BigInteger getCoef (int)
public abstract java.math.BigInteger getDegree ()
public abstract org.sat4j.minisat.core.ILits getVocabulary ()
public abstract int[] getLits ()
public abstract java.math.BigInteger[] getCoefs ()
public abstract org.sat4j.specs.IVecInt computeAnImpliedClause ()
}
org/sat4j/pb/constraints/pb/package-info.classpackage-info.java
package org.sat4j.pb.constraints.pb
abstract org.sat4j.pb.constraints.pb.package-info extends java.lang.Object {
}
org/sat4j/pb/constraints/pb/LearntHTClausePB.classLearntHTClausePB.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.LearntHTClausePB extends org.sat4j.minisat.constraints.cnf.LearntHTClause implements org.sat4j.pb.constraints.pb.PBConstr {
private static final long serialVersionUID
public void (org.sat4j.specs.IVecInt, org.sat4j.minisat.core.ILits)
org.sat4j.specs.IVecInt ps
org.sat4j.minisat.core.ILits voc
public void assertConstraint (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
int i
int temp
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
public java.math.BigInteger getCoef (int)
int literal
public java.math.BigInteger[] getCoefs ()
java.math.BigInteger[] tmp
int i
public java.math.BigInteger getDegree ()
}
org/sat4j/pb/constraints/pb/IWatchPb.classIWatchPb.java
package org.sat4j.pb.constraints.pb
public abstract org.sat4j.pb.constraints.pb.IWatchPb extends java.lang.Object implements org.sat4j.pb.constraints.pb.PBConstr {
public abstract java.math.BigInteger slackConstraint (java.math.BigInteger[], java.math.BigInteger)
}
org/sat4j/pb/constraints/pb/AtLeastPB.classAtLeastPB.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.AtLeastPB extends org.sat4j.minisat.constraints.card.AtLeast implements org.sat4j.pb.constraints.pb.PBConstr {
private static final long serialVersionUID
private final java.math.BigInteger degree
private boolean learnt
static final boolean $assertionsDisabled
static void ()
private void (org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int)
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt ps
int degree
public static org.sat4j.pb.constraints.pb.PBConstr atLeastNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt ps
int n
int degree
public static org.sat4j.pb.constraints.pb.AtLeastPB atLeastNew (org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int)
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt ps
int n
org.sat4j.pb.constraints.pb.AtLeastPB atleast
public java.math.BigInteger getCoef (int)
int literal
public java.math.BigInteger getDegree ()
public org.sat4j.minisat.core.ILits getVocabulary ()
public int[] getLits ()
int[] tmp
public java.math.BigInteger[] getCoefs ()
java.math.BigInteger[] tmp
int i
public boolean learnt ()
public void setLearnt ()
public void assertConstraint (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
int i
boolean ret
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
public static volatile org.sat4j.minisat.core.Constr atLeastNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
}
org/sat4j/pb/constraints/pb/OriginalBinaryClausePB.classOriginalBinaryClausePB.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.OriginalBinaryClausePB extends org.sat4j.minisat.constraints.cnf.OriginalBinaryClause implements org.sat4j.pb.constraints.pb.PBConstr {
private static final long serialVersionUID
public void (org.sat4j.specs.IVecInt, org.sat4j.minisat.core.ILits)
org.sat4j.specs.IVecInt ps
org.sat4j.minisat.core.ILits voc
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
public java.math.BigInteger getCoef (int)
int literal
public java.math.BigInteger[] getCoefs ()
java.math.BigInteger[] tmp
int i
public java.math.BigInteger getDegree ()
public static org.sat4j.pb.constraints.pb.OriginalBinaryClausePB brandNewClause (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt literals
org.sat4j.pb.constraints.pb.OriginalBinaryClausePB c
public static volatile org.sat4j.minisat.constraints.cnf.OriginalBinaryClause brandNewClause (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
}
org/sat4j/pb/constraints/pb/MinWatchCardPB.classMinWatchCardPB.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.MinWatchCardPB extends org.sat4j.minisat.constraints.card.MinWatchCard implements org.sat4j.pb.constraints.pb.PBConstr {
private static final long serialVersionUID
private final java.math.BigInteger bigDegree
private boolean learnt
static final boolean $assertionsDisabled
static void ()
public void (org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, boolean, int)
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt ps
boolean moreThan
int degree
public void (org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int)
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt ps
int degree
public java.math.BigInteger getCoef (int)
int literal
public java.math.BigInteger getDegree ()
public java.math.BigInteger[] getCoefs ()
java.math.BigInteger[] tmp
int i
public static org.sat4j.pb.constraints.pb.PBConstr normalizedMinWatchCardPBNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt ps
int degree
public static org.sat4j.pb.constraints.pb.PBConstr minWatchCardPBNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, boolean, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt ps
boolean moreThan
int degree
private static org.sat4j.pb.constraints.pb.PBConstr minWatchCardPBNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, boolean, int, boolean) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt ps
boolean moreThan
int degree
boolean normalized
int mydegree
int i
org.sat4j.pb.constraints.pb.MinWatchCardPB retour
public boolean learnt ()
public void setLearnt ()
public void register ()
public void assertConstraint (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
int i
boolean ret
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
}
org/sat4j/pb/constraints/pb/LearntBinaryClausePB.classLearntBinaryClausePB.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.LearntBinaryClausePB extends org.sat4j.minisat.constraints.cnf.LearntBinaryClause implements org.sat4j.pb.constraints.pb.PBConstr {
private static final long serialVersionUID
public void (org.sat4j.specs.IVecInt, org.sat4j.minisat.core.ILits)
org.sat4j.specs.IVecInt ps
org.sat4j.minisat.core.ILits voc
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
public java.math.BigInteger getCoef (int)
int literal
public java.math.BigInteger[] getCoefs ()
java.math.BigInteger[] tmp
int i
public java.math.BigInteger getDegree ()
}
org/sat4j/pb/constraints/pb/WatchPbLong.classWatchPbLong.java
package org.sat4j.pb.constraints.pb
public abstract org.sat4j.pb.constraints.pb.WatchPbLong extends java.lang.Object implements org.sat4j.minisat.core.Propagatable org.sat4j.minisat.core.Constr org.sat4j.minisat.core.Undoable java.io.Serializable {
private static final long serialVersionUID
private static final int LIMIT_SELECTION_SORT
protected double activity
protected long[] coefs
protected long sumcoefs
protected long degree
protected int[] lits
protected boolean learnt
protected org.sat4j.minisat.core.ILits voc
private final java.util.Comparator levelBased
static final boolean $assertionsDisabled
static void ()
void ()
void (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
int size
java.math.BigInteger[] bigCoefs
long c
void (int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
public static long[] toLong (java.math.BigInteger[])
java.math.BigInteger[] bigValues
long[] res
int i
public boolean isAssertive (int)
int dl
long slack
int i
int i
public void calcReason (int, org.sat4j.specs.IVecInt)
int p
org.sat4j.specs.IVecInt outReason
long sumfalsified
long tous
int[] mlits
boolean ok
int i
int q
protected abstract void computeWatches () throws org.sat4j.specs.ContradictionException
protected abstract void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
public int get (int)
int i
public double getActivity ()
public void incActivity (double)
double claInc
public void setActivity (double)
double d
public long slackConstraint ()
public long slackConstraint (long[], long)
long[] theCoefs
long theDegree
public long computeLeftSide (long[])
long[] theCoefs
long poss
int i
public long computeLeftSide ()
protected boolean isSatisfiable ()
public boolean learnt ()
public boolean locked ()
int p
protected static java.math.BigInteger ppcm (java.math.BigInteger, java.math.BigInteger)
java.math.BigInteger a
java.math.BigInteger b
public void rescaleBy (double)
double d
void selectionSort (int, int)
int from
int to
int i
int j
int bestIndex
long tmp
int tmp2
public void setLearnt ()
public boolean simplify ()
long cumul
int i
public final int size ()
protected final void sort ()
long buffInt
int i
protected final void sort (int, int)
int from
int to
int width
int indPivot
long pivot
int litPivot
long tmp
int i
int j
int tmp2
public java.lang.String toString ()
StringBuffer stb
int i
public void assertConstraint (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
long tmp
int i
boolean ret
public void assertConstraintIfNeeded (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener s
public void register ()
public int[] getLits ()
int[] litsBis
public org.sat4j.minisat.core.ILits getVocabulary ()
public org.sat4j.specs.IVecInt computeAnImpliedClause ()
long cptCoefs
int index
org.sat4j.specs.IVecInt literals
int j
public boolean coefficientsEqualToOne ()
public boolean equals (java.lang.Object)
Object pb
org.sat4j.pb.constraints.pb.WatchPbLong wpb
int lit
boolean ok
int ilit
int ilit2
public int hashCode ()
long sum
int p
public void forwardActivity (double)
double claInc
public void remove (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener upl
public boolean propagate (org.sat4j.specs.UnitPropagationListener, int)
org.sat4j.specs.UnitPropagationListener s
int p
public void undo (int)
int p
public boolean canBePropagatedMultipleTimes ()
public org.sat4j.minisat.core.Constr toConstraint ()
public void calcReasonOnTheFly (int, org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt)
int p
org.sat4j.specs.IVecInt trail
org.sat4j.specs.IVecInt outReason
long sumfalsified
java.util.List sortedList
int q
org.sat4j.specs.IVecInt vlits
int index
int q
}
org/sat4j/pb/constraints/pb/MinWatchPbLong.classMinWatchPbLong.java
package org.sat4j.pb.constraints.pb
public org.sat4j.pb.constraints.pb.MinWatchPbLong extends org.sat4j.pb.constraints.pb.WatchPbLong {
private static final long serialVersionUID
protected long watchCumul
protected boolean[] watched
protected int[] watching
protected int watchingCount
static final boolean $assertionsDisabled
static void ()
protected void (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
protected void (org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
protected void computeWatches () throws org.sat4j.specs.ContradictionException
int i
private void watchMoreForLearntConstraint ()
int free
int maxlevel
int maxi
int level
int i
protected void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
int ind
public static org.sat4j.pb.constraints.pb.MinWatchPbLong normalizedMinWatchPbNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
org.sat4j.pb.constraints.pb.MinWatchPbLong outclause
protected int nbOfWatched ()
int retour
int ind
int i
public boolean propagate (org.sat4j.specs.UnitPropagationListener, int)
org.sat4j.specs.UnitPropagationListener s
int p
int pIndiceWatching
int pIndice
long maxCoef
long upWatchCumul
long limit
int i
public void remove (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener upl
int i
public void undo (int)
int p
int pIndice
public static org.sat4j.pb.constraints.pb.WatchPbLong normalizedWatchPbNew (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
protected long maximalCoefficient (int)
int pIndice
long maxCoef
int i
protected long updateWatched (long, int)
long mc
int pIndice
long maxCoef
long upWatchCumul
long degreePlusMaxCoef
int ind
}
org/sat4j/pb/constraints/pb/ConflictMapSwitchToClause.classConflictMapSwitchToClause.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.ConflictMapSwitchToClause extends org.sat4j.pb.constraints.pb.ConflictMap {
public static int UpperBound
public void (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr cpb
int level
public static org.sat4j.pb.constraints.pb.IConflict createConflict (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr cpb
int level
protected java.math.BigInteger reduceUntilConflict (int, int, java.math.BigInteger[], org.sat4j.pb.constraints.pb.IWatchPb)
int litImplied
int ind
java.math.BigInteger[] reducedCoefs
org.sat4j.pb.constraints.pb.IWatchPb wpb
java.math.BigInteger degreeCons
int i
java.math.BigInteger bigCoef
private java.math.BigInteger reduceToClause (int, org.sat4j.pb.constraints.pb.IWatchPb, java.math.BigInteger[])
int ind
org.sat4j.pb.constraints.pb.IWatchPb wpb
java.math.BigInteger[] reducedCoefs
int i
}
org/sat4j/pb/constraints/pb/MaxWatchPbLong.classMaxWatchPbLong.java
package org.sat4j.pb.constraints.pb
public final org.sat4j.pb.constraints.pb.MaxWatchPbLong extends org.sat4j.pb.constraints.pb.WatchPbLong {
private static final long serialVersionUID
private long watchCumul
private final java.util.Map litToCoeffs
static final boolean $assertionsDisabled
static void ()
private void (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
int i
private void (org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger)
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
int i
protected void computeWatches () throws org.sat4j.specs.ContradictionException
int i
protected void computePropagation (org.sat4j.specs.UnitPropagationListener) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
int ind
public boolean propagate (org.sat4j.specs.UnitPropagationListener, int)
org.sat4j.specs.UnitPropagationListener s
int p
long coefP
long coefP
int indiceP
long newcumul
int ind
long limit
public void remove (org.sat4j.specs.UnitPropagationListener)
org.sat4j.specs.UnitPropagationListener upl
int i
public void undo (int)
int p
long coefP
long coefP
long coefP
int indiceP
Long coefL
public static org.sat4j.pb.constraints.pb.MaxWatchPbLong normalizedMaxWatchPbNew (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener s
org.sat4j.minisat.core.ILits voc
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
org.sat4j.pb.constraints.pb.MaxWatchPbLong outclause
public static org.sat4j.pb.constraints.pb.WatchPbLong normalizedWatchPbNew (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB mpb
}
org/sat4j/pb/constraints/MinWatchPBConstructor.classMinWatchPBConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.MinWatchPBConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IPBConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
public org.sat4j.minisat.core.Constr constructPB (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
int[] theLits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
}
org/sat4j/pb/constraints/ICardConstructor.classICardConstructor.java
package org.sat4j.pb.constraints
public abstract org.sat4j.pb.constraints.ICardConstructor extends java.lang.Object {
public abstract org.sat4j.minisat.core.Constr constructCard (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.minisat.core.Constr constructLearntCard (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
}
org/sat4j/pb/constraints/MaxLongWatchPBConstructor.classMaxLongWatchPBConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.MaxLongWatchPBConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IPBConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
public org.sat4j.minisat.core.Constr constructPB (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
int[] theLits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
}
org/sat4j/pb/constraints/AbstractPBClauseCardConstrDataStructure.classAbstractPBClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public abstract org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBDataStructureFactory {
private static final long serialVersionUID
static final java.math.BigInteger MAX_INT_VALUE
private final org.sat4j.pb.constraints.IPBConstructor ipbc
private final org.sat4j.pb.constraints.ICardConstructor icardc
private final org.sat4j.pb.constraints.IClauseConstructor iclausec
static final boolean $assertionsDisabled
static void ()
void (org.sat4j.pb.constraints.IClauseConstructor, org.sat4j.pb.constraints.ICardConstructor, org.sat4j.pb.constraints.IPBConstructor)
org.sat4j.pb.constraints.IClauseConstructor iclausec
org.sat4j.pb.constraints.ICardConstructor icardc
org.sat4j.pb.constraints.IPBConstructor ipbc
public org.sat4j.minisat.core.Constr createClause (org.sat4j.specs.IVecInt) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt v
public org.sat4j.minisat.core.Constr createUnregisteredClause (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt literals
protected org.sat4j.minisat.core.Constr constraintFactory (int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
int[] literals
java.math.BigInteger[] coefs
java.math.BigInteger degree
org.sat4j.specs.IVecInt v
protected org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec resCoefs
int indLit
int tmp
private org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger, boolean)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
boolean moreThan
int[] lits
java.math.BigInteger[] bc
protected org.sat4j.minisat.core.Constr learntAtLeastConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected org.sat4j.minisat.core.Constr learntAtMostConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
static boolean coefficientsEqualToOne (java.math.BigInteger[])
java.math.BigInteger[] coefs
int i
protected org.sat4j.minisat.core.Constr constructClause (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt v
protected org.sat4j.minisat.core.Constr constructCard (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt theLits
int degree
protected org.sat4j.minisat.core.Constr constructPB (int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
int[] theLits
java.math.BigInteger[] coefs
java.math.BigInteger degree
protected org.sat4j.minisat.core.Constr constructLearntClause (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt literals
protected org.sat4j.minisat.core.Constr constructLearntCard (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
protected org.sat4j.minisat.core.Constr constructLearntCard (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
protected org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
public static final java.math.BigInteger sumOfCoefficients (java.math.BigInteger[])
java.math.BigInteger[] coefs
java.math.BigInteger sumCoefs
java.math.BigInteger c
}
org/sat4j/pb/constraints/PBMaxClauseAtLeastConstrDataStructure.classPBMaxClauseAtLeastConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PBMaxClauseAtLeastConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/MinCardPBConstructor.classMinCardPBConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.MinCardPBConstructor extends java.lang.Object implements org.sat4j.pb.constraints.ICardConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructCard (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt theLits
int degree
public org.sat4j.minisat.core.Constr constructLearntCard (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
org.sat4j.specs.IVecInt resLits
org.sat4j.specs.IVec resCoefs
}
org/sat4j/pb/constraints/AbstractPBDataStructureFactory$INormalizer.classAbstractPBDataStructureFactory.java
package org.sat4j.pb.constraints
abstract org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer extends java.lang.Object {
public abstract org.sat4j.pb.constraints.PBContainer nice (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger, org.sat4j.minisat.core.ILits) throws org.sat4j.specs.ContradictionException
}
org/sat4j/pb/constraints/AtLeastCardConstructor.classAtLeastCardConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.AtLeastCardConstructor extends java.lang.Object implements org.sat4j.pb.constraints.ICardConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructCard (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt theLits
int degree
public org.sat4j.minisat.core.Constr constructLearntCard (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
org.sat4j.specs.IVecInt resLits
org.sat4j.specs.IVec resCoefs
}
org/sat4j/pb/constraints/MinCardConstructor.classMinCardConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.MinCardConstructor extends java.lang.Object implements org.sat4j.pb.constraints.ICardConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructCard (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt theLits
int degree
public org.sat4j.minisat.core.Constr constructLearntCard (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
org.sat4j.specs.IVecInt resLits
org.sat4j.specs.IVec resCoefs
}
org/sat4j/pb/constraints/PBLongMaxClauseCardConstrDataStructure.classPBLongMaxClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PBLongMaxClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/PBMaxDataStructure.classPBMaxDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PBMaxDataStructure extends org.sat4j.pb.constraints.AbstractPBDataStructureFactory {
private static final long serialVersionUID
public void ()
protected org.sat4j.minisat.core.Constr constraintFactory (int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
int[] literals
java.math.BigInteger[] coefs
java.math.BigInteger degree
protected org.sat4j.pb.constraints.pb.WatchPb learntConstraintFactory (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
private org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger, boolean)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
boolean moreThan
int[] lits
java.math.BigInteger[] bc
protected org.sat4j.minisat.core.Constr learntAtLeastConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected org.sat4j.minisat.core.Constr learntAtMostConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected volatile org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.pb.constraints.pb.IDataStructurePB)
}
org/sat4j/pb/constraints/PBLongMinClauseCardConstrDataStructure.classPBLongMinClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PBLongMinClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/PuebloPBMinClauseAtLeastConstrDataStructure.classPuebloPBMinClauseAtLeastConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PuebloPBMinClauseAtLeastConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/PuebloMinWatchPBConstructor.classPuebloMinWatchPBConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PuebloMinWatchPBConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IPBConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
public org.sat4j.minisat.core.Constr constructPB (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
int[] theLits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
}
org/sat4j/pb/constraints/CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure.classCompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/PBMaxClauseCardConstrDataStructure.classPBMaxClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/AbstractPBDataStructureFactory.classAbstractPBDataStructureFactory.java
package org.sat4j.pb.constraints
public abstract org.sat4j.pb.constraints.AbstractPBDataStructureFactory extends org.sat4j.minisat.constraints.AbstractDataStructureFactory implements org.sat4j.pb.core.PBDataStructureFactory {
public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer FOR_COMPETITION
public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer NO_COMPETITION
private org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer norm
private static final long serialVersionUID
static void ()
public void ()
protected org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer getNormalizer ()
public void setNormalizer (java.lang.String)
String simp
java.lang.reflect.Field f
Exception e
public void setNormalizer (org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer)
org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer normalizer
public org.sat4j.minisat.core.Constr createClause (org.sat4j.specs.IVecInt) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt v
public org.sat4j.minisat.core.Constr createUnregisteredClause (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt literals
public org.sat4j.minisat.core.Constr createCardinalityConstraint (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
public org.sat4j.minisat.core.Constr createPseudoBooleanConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
boolean moreThan
java.math.BigInteger degree
org.sat4j.pb.constraints.PBContainer res
public org.sat4j.minisat.core.Constr createAtMostPBConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
public org.sat4j.minisat.core.Constr createAtLeastPBConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
public org.sat4j.minisat.core.Constr createUnregisteredPseudoBooleanConstraint (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
public org.sat4j.minisat.core.Constr createUnregisteredAtLeastConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
public org.sat4j.minisat.core.Constr createUnregisteredAtMostConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected abstract org.sat4j.minisat.core.Constr constraintFactory (int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
protected abstract org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.pb.constraints.pb.IDataStructurePB)
protected abstract org.sat4j.minisat.core.Constr learntAtLeastConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
protected abstract org.sat4j.minisat.core.Constr learntAtMostConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
protected org.sat4j.minisat.core.ILits createLits ()
public org.sat4j.minisat.core.Constr createUnregisteredCardinalityConstraint (org.sat4j.specs.IVecInt, int)
org.sat4j.specs.IVecInt literals
int degree
}
org/sat4j/pb/constraints/PuebloPBMinClauseCardConstrDataStructure.classPuebloPBMinClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
public org.sat4j.minisat.core.Constr createClause (org.sat4j.specs.IVecInt) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt v
}
org/sat4j/pb/constraints/package-info.classpackage-info.java
package org.sat4j.pb.constraints
abstract org.sat4j.pb.constraints.package-info extends java.lang.Object {
}
org/sat4j/pb/constraints/AbstractPBDataStructureFactory$2.classAbstractPBDataStructureFactory.java
package org.sat4j.pb.constraints
org.sat4j.pb.constraints.AbstractPBDataStructureFactory$2 extends java.lang.Object implements org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer {
void ()
public org.sat4j.pb.constraints.PBContainer nice (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger, org.sat4j.minisat.core.ILits) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
boolean moreThan
java.math.BigInteger degree
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB res
int size
int[] theLits
java.math.BigInteger[] theCoefs
java.math.BigInteger theDegree
}
org/sat4j/pb/constraints/MaxWatchPBConstructor.classMaxWatchPBConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.MaxWatchPBConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IPBConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
public org.sat4j.minisat.core.Constr constructPB (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
int[] theLits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
}
org/sat4j/pb/constraints/MinLongWatchPBCPConstructor.classMinLongWatchPBCPConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.MinLongWatchPBCPConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IPBConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
public org.sat4j.minisat.core.Constr constructPB (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
int[] theLits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
}
org/sat4j/pb/constraints/CompetMinHTmixedClauseCardConstrDataStructureFactory.classCompetMinHTmixedClauseCardConstrDataStructureFactory.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/PBContainer.classPBContainer.java
package org.sat4j.pb.constraints
final org.sat4j.pb.constraints.PBContainer extends java.lang.Object {
final int[] lits
final java.math.BigInteger[] coefs
final java.math.BigInteger degree
void (int[], java.math.BigInteger[], java.math.BigInteger)
int[] lits
java.math.BigInteger[] coefs
java.math.BigInteger degree
}
org/sat4j/pb/constraints/MinLongWatchPBConstructor.classMinLongWatchPBConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.MinLongWatchPBConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IPBConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
public org.sat4j.minisat.core.Constr constructPB (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
int[] theLits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
}
org/sat4j/pb/constraints/UnitBinaryHTClauseConstructor.classUnitBinaryHTClauseConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.UnitBinaryHTClauseConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IClauseConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructClause (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt v
public org.sat4j.minisat.core.Constr constructLearntClause (org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt literals
}
org/sat4j/pb/constraints/CompetResolutionPBMixedHTClauseCardConstrDataStructure.classCompetResolutionPBMixedHTClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/PBMinClauseCardConstrDataStructure.classPBMinClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PBMinClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/IClauseConstructor.classIClauseConstructor.java
package org.sat4j.pb.constraints
public abstract org.sat4j.pb.constraints.IClauseConstructor extends java.lang.Object {
public abstract org.sat4j.minisat.core.Constr constructClause (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
public abstract org.sat4j.minisat.core.Constr constructLearntClause (org.sat4j.minisat.core.ILits, org.sat4j.specs.IVecInt)
}
org/sat4j/pb/constraints/CompetResolutionPBMixedWLClauseCardConstrDataStructure.classCompetResolutionPBMixedWLClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/PBMinDataStructure.classPBMinDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PBMinDataStructure extends org.sat4j.pb.constraints.AbstractPBDataStructureFactory {
private static final long serialVersionUID
public void ()
protected org.sat4j.pb.constraints.pb.PBConstr constraintFactory (int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
int[] literals
java.math.BigInteger[] coefs
java.math.BigInteger degree
protected org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
private org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger, boolean)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
boolean moreThan
int[] lits
java.math.BigInteger[] bc
protected org.sat4j.minisat.core.Constr learntAtLeastConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected org.sat4j.minisat.core.Constr learntAtMostConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected volatile org.sat4j.minisat.core.Constr constraintFactory (int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
}
org/sat4j/pb/constraints/CompetResolutionPBLongMixedHTClauseCardConstrDataStructure.classCompetResolutionPBLongMixedHTClauseCardConstrDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.CompetResolutionPBLongMixedHTClauseCardConstrDataStructure extends org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure {
private static final long serialVersionUID
public void ()
}
org/sat4j/pb/constraints/MaxLongWatchPBCPConstructor.classMaxLongWatchPBCPConstructor.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.MaxLongWatchPBCPConstructor extends java.lang.Object implements org.sat4j.pb.constraints.IPBConstructor {
public void ()
public org.sat4j.minisat.core.Constr constructLearntPB (org.sat4j.minisat.core.ILits, org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.minisat.core.ILits voc
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
public org.sat4j.minisat.core.Constr constructPB (org.sat4j.specs.UnitPropagationListener, org.sat4j.minisat.core.ILits, int[], java.math.BigInteger[], java.math.BigInteger, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.UnitPropagationListener solver
org.sat4j.minisat.core.ILits voc
int[] theLits
java.math.BigInteger[] coefs
java.math.BigInteger degree
java.math.BigInteger sumCoefs
}
org/sat4j/pb/constraints/PuebloPBMinDataStructure.classPuebloPBMinDataStructure.java
package org.sat4j.pb.constraints
public org.sat4j.pb.constraints.PuebloPBMinDataStructure extends org.sat4j.pb.constraints.AbstractPBDataStructureFactory {
private static final long serialVersionUID
public void ()
protected org.sat4j.pb.constraints.pb.PBConstr constraintFactory (int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
int[] literals
java.math.BigInteger[] coefs
java.math.BigInteger degree
protected org.sat4j.pb.constraints.pb.PBConstr learntConstraintFactory (org.sat4j.pb.constraints.pb.IDataStructurePB)
org.sat4j.pb.constraints.pb.IDataStructurePB dspb
private org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger, boolean)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
boolean moreThan
int[] lits
java.math.BigInteger[] bc
protected org.sat4j.minisat.core.Constr learntAtLeastConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected org.sat4j.minisat.core.Constr learntAtMostConstraintFactory (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
protected volatile org.sat4j.minisat.core.Constr constraintFactory (int[], java.math.BigInteger[], java.math.BigInteger) throws org.sat4j.specs.ContradictionException
protected volatile org.sat4j.minisat.core.Constr learntConstraintFactory (org.sat4j.pb.constraints.pb.IDataStructurePB)
}
org/sat4j/pb/constraints/AbstractPBDataStructureFactory$1.classAbstractPBDataStructureFactory.java
package org.sat4j.pb.constraints
org.sat4j.pb.constraints.AbstractPBDataStructureFactory$1 extends java.lang.Object implements org.sat4j.pb.constraints.AbstractPBDataStructureFactory$INormalizer {
void ()
public org.sat4j.pb.constraints.PBContainer nice (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger, org.sat4j.minisat.core.ILits) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
boolean moreThan
java.math.BigInteger degree
org.sat4j.minisat.core.ILits voc
org.sat4j.specs.IVecInt cliterals
org.sat4j.specs.IVec ccoefs
int i
int[] theLits
java.math.BigInteger[] normCoefs
java.math.BigInteger degRes
}
org/sat4j/pb/reader/OPBReader2006.classOPBReader2006.java
package org.sat4j.pb.reader
public org.sat4j.pb.reader.OPBReader2006 extends org.sat4j.pb.reader.OPBReader2005 {
private static final long serialVersionUID
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
protected void readTerm (java.lang.StringBuffer, java.lang.StringBuffer) throws java.io.IOException org.sat4j.reader.ParseFormatException
StringBuffer coeff
StringBuffer var
}
org/sat4j/pb/reader/OPBEclipseReader2007.classOPBEclipseReader2007.java
package org.sat4j.pb.reader
public org.sat4j.pb.reader.OPBEclipseReader2007 extends org.sat4j.pb.reader.OPBReader2007 {
private static final long serialVersionUID
private final org.sat4j.specs.IVecInt varExplain
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
protected void beginListOfVariables ()
protected void endListOfVariables ()
protected void readVariablesExplanation () throws java.io.IOException org.sat4j.reader.ParseFormatException
char c
StringBuffer var
public org.sat4j.specs.IVecInt getListOfVariables ()
org.sat4j.specs.IVecInt tmp
}
org/sat4j/pb/reader/package-info.classpackage-info.java
package org.sat4j.pb.reader
abstract org.sat4j.pb.reader.package-info extends java.lang.Object {
}
org/sat4j/pb/reader/PBInstanceReader.classPBInstanceReader.java
package org.sat4j.pb.reader
public org.sat4j.pb.reader.PBInstanceReader extends org.sat4j.reader.InstanceReader {
private org.sat4j.pb.reader.OPBReader2012 opb
private final org.sat4j.pb.IPBSolver solver
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
private org.sat4j.reader.Reader getDefaultOPBReader ()
public boolean hasObjectiveFunction ()
protected org.sat4j.reader.Reader handleFileName (java.lang.String, java.lang.String)
String fname
String prefix
}
org/sat4j/pb/reader/OPBReader2010.classOPBReader2010.java
package org.sat4j.pb.reader
public org.sat4j.pb.reader.OPBReader2010 extends org.sat4j.pb.reader.OPBReader2007 {
public static final java.math.BigInteger SAT4J_MAX_BIG_INTEGER
private boolean isWbo
private java.math.BigInteger softLimit
private static final long serialVersionUID
private boolean softConstraint
static void ()
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
protected void readMetaData () throws java.io.IOException org.sat4j.reader.ParseFormatException
char c
String s
String rest
String[] splitted
protected void readObjective () throws java.io.IOException org.sat4j.reader.ParseFormatException
private void readSoftLine () throws java.io.IOException org.sat4j.reader.ParseFormatException
String s
protected void beginConstraint ()
char c
String s
java.math.BigInteger coeff
int varId
Exception e
protected void endConstraint () throws org.sat4j.specs.ContradictionException
int varId
java.math.BigInteger constrWeight
java.util.Iterator it
public org.sat4j.specs.IProblem parseInstance (java.io.Reader) throws org.sat4j.reader.ParseFormatException org.sat4j.specs.ContradictionException
java.io.Reader input
}
org/sat4j/pb/reader/OPBReader2005.classOPBReader2005.java
package org.sat4j.pb.reader
public org.sat4j.pb.reader.OPBReader2005 extends org.sat4j.reader.Reader implements java.io.Serializable {
private static final long serialVersionUID
protected final org.sat4j.pb.IPBSolver solver
protected final org.sat4j.specs.IVecInt lits
protected final org.sat4j.specs.IVec coeffs
protected java.math.BigInteger d
protected String operator
private final org.sat4j.specs.IVecInt objectiveVars
private final org.sat4j.specs.IVec objectiveCoeffs
protected boolean hasObjFunc
protected boolean hasVariablesExplanation
protected int nbVars
protected int nbConstr
protected int nbConstraintsRead
transient java.io.BufferedReader in
char savedChar
boolean charAvailable
boolean eofReached
private boolean eolReached
static final boolean $assertionsDisabled
static void ()
protected void metaData (int, int)
int nbvar
int nbconstr
protected void beginObjective ()
protected void endObjective ()
int i
protected void beginConstraint ()
protected void endConstraint () throws org.sat4j.specs.ContradictionException
private void constraintTerm (java.math.BigInteger, java.lang.String) throws org.sat4j.reader.ParseFormatException
java.math.BigInteger coeff
String var
protected int translateVarToId (java.lang.String) throws org.sat4j.reader.ParseFormatException
String var
int id
protected void constraintRelOp (java.lang.String)
String relop
protected void constraintRightTerm (java.math.BigInteger)
java.math.BigInteger val
protected char get () throws java.io.IOException
int c
public org.sat4j.specs.IVecInt getVars ()
public org.sat4j.specs.IVec getCoeffs ()
protected void putback (char)
char c
protected boolean eof ()
protected boolean eol ()
protected void skipSpaces () throws java.io.IOException
char c
public java.lang.String readWord () throws java.io.IOException
StringBuffer s
char c
char c
public void readInteger (java.lang.StringBuffer) throws java.io.IOException
StringBuffer s
char c
protected boolean readIdentifier (java.lang.StringBuffer) throws java.io.IOException org.sat4j.reader.ParseFormatException
StringBuffer s
char c
protected boolean isGoodFirstCharacter (char)
char c
protected boolean isGoodFollowingCharacter (char)
char c
protected void checkId (java.lang.StringBuffer) throws org.sat4j.reader.ParseFormatException
StringBuffer s
int varID
private java.lang.String readRelOp () throws java.io.IOException
char c
char following
protected void readMetaData () throws java.io.IOException org.sat4j.reader.ParseFormatException
char c
String s
private void skipComments () throws java.io.IOException
char c
protected void readTerm (java.lang.StringBuffer, java.lang.StringBuffer) throws java.io.IOException org.sat4j.reader.ParseFormatException
StringBuffer coeff
StringBuffer var
char c
protected void readVariablesExplanation () throws java.io.IOException org.sat4j.reader.ParseFormatException
protected void readObjective () throws java.io.IOException org.sat4j.reader.ParseFormatException
char c
StringBuffer var
StringBuffer coeff
protected void readConstraint () throws java.io.IOException org.sat4j.reader.ParseFormatException org.sat4j.specs.ContradictionException
StringBuffer var
StringBuffer coeff
char c
char c
String relop
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public void parse () throws java.io.IOException org.sat4j.reader.ParseFormatException org.sat4j.specs.ContradictionException
char c
public org.sat4j.specs.IProblem parseInstance (java.io.Reader) throws org.sat4j.reader.ParseFormatException org.sat4j.specs.ContradictionException
java.io.Reader input
org.sat4j.specs.IProblem problem
protected org.sat4j.specs.IProblem parseInstance (java.io.LineNumberReader) throws org.sat4j.reader.ParseFormatException org.sat4j.specs.ContradictionException
java.io.LineNumberReader input
org.sat4j.specs.ContradictionException ce
org.sat4j.reader.ParseFormatException pfe
Exception e
public java.lang.String decode (int[])
int[] model
StringBuffer stb
int i
public void decode (int[], java.io.PrintWriter)
int[] model
java.io.PrintWriter out
int i
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IVecInt getListOfVariables ()
public org.sat4j.specs.IProblem parseInstance (java.io.InputStream) throws org.sat4j.reader.ParseFormatException org.sat4j.specs.ContradictionException java.io.IOException
java.io.InputStream in
}
org/sat4j/pb/reader/JSONPBReader.classJSONPBReader.java
package org.sat4j.pb.reader
public org.sat4j.pb.reader.JSONPBReader extends org.sat4j.reader.JSONReader {
public static final String WLITERAL
public static final String WCLAUSE
public static final String PB
public static final String OBJECTIVE_FUNCTION
public static final java.util.regex.Pattern PSEUDO_PATTERN
public static final java.util.regex.Pattern WCLAUSE_PATTERN
public static final java.util.regex.Pattern WLITERAL_PATTERN
public static final java.util.regex.Pattern OBJECTIVE_FUNCTION_PATTERN
static final boolean $assertionsDisabled
static void ()
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
protected void handleNotHandled (java.lang.String) throws org.sat4j.reader.ParseFormatException org.sat4j.specs.ContradictionException
String constraint
private void handleObj (java.lang.String)
String constraint
java.util.regex.Matcher matcher
String weightedLiterals
org.sat4j.specs.IVecInt literals
String[] pieces
boolean negate
org.sat4j.specs.IVec coefs
java.math.BigInteger coef
private void handlePB (java.lang.String) throws org.sat4j.specs.ContradictionException
String constraint
java.util.regex.Matcher matcher
String weightedLiterals
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coefs
String[] pieces
String comp
int degree
protected java.lang.String constraintRegexp ()
}
org/sat4j/pb/reader/OPBReader2007.classOPBReader2007.java
package org.sat4j.pb.reader
public org.sat4j.pb.reader.OPBReader2007 extends org.sat4j.pb.reader.OPBReader2006 {
private static final long serialVersionUID
protected int nbNewSymbols
private final java.util.Map varToProduct
private final java.util.Map binaryProductToVar
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
protected boolean isGoodFirstCharacter (char)
char c
protected void checkId (java.lang.StringBuffer) throws org.sat4j.reader.ParseFormatException
StringBuffer s
int cpt
int varID
protected void readTerm (java.lang.StringBuffer, java.lang.StringBuffer) throws java.io.IOException org.sat4j.reader.ParseFormatException
StringBuffer coeff
StringBuffer var
org.sat4j.specs.IVec tmpLit
StringBuffer tmpVar
org.sat4j.specs.ContradictionException e
protected void literalInAProduct (java.lang.String, org.sat4j.specs.IVecInt) throws org.sat4j.reader.ParseFormatException
String var
org.sat4j.specs.IVecInt lits
int beginning
int id
int lid
protected void negateLiteralInAProduct (java.lang.String, org.sat4j.specs.IVecInt)
String var
org.sat4j.specs.IVecInt lits
int beginning
int id
int lid
protected void readMetaData () throws java.io.IOException org.sat4j.reader.ParseFormatException
char c
String s
String rest
String[] splitted
protected int translateVarToId (java.lang.String) throws org.sat4j.reader.ParseFormatException
String var
int beginning
int id
private java.lang.String linearizeProduct (org.sat4j.specs.IVec) throws org.sat4j.specs.ContradictionException org.sat4j.reader.ParseFormatException
org.sat4j.specs.IVec tmpLit
String newVar
java.util.Map map1
org.sat4j.specs.IVecInt newLits
java.util.Iterator iterator
org.sat4j.specs.IVec newCoefs
java.util.Iterator iterator
private java.lang.String getProductVariable (org.sat4j.specs.IVec)
org.sat4j.specs.IVec lits
java.util.Map map
java.util.Map$Entry c
public java.lang.String decode (int[])
int[] model
StringBuffer stb
int p
int element
public void decode (int[], java.io.PrintWriter)
int[] model
java.io.PrintWriter out
int p
int element
}
org/sat4j/pb/reader/OPBReader2012.classOPBReader2012.java
package org.sat4j.pb.reader
public org.sat4j.pb.reader.OPBReader2012 extends org.sat4j.pb.reader.OPBReader2010 {
private org.sat4j.pb.tools.LexicoDecoratorPB lexico
private static final long serialVersionUID
static final boolean $assertionsDisabled
static void ()
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
protected void readMetaData () throws java.io.IOException org.sat4j.reader.ParseFormatException
char c
String s
protected void readObjective () throws java.io.IOException org.sat4j.reader.ParseFormatException
public org.sat4j.specs.IProblem parseInstance (java.io.Reader) throws org.sat4j.reader.ParseFormatException org.sat4j.specs.ContradictionException
java.io.Reader input
org.sat4j.specs.IProblem problem
}
org/sat4j/pb/LanceurPseudo2005.classLanceurPseudo2005.java
package org.sat4j.pb
public org.sat4j.pb.LanceurPseudo2005 extends org.sat4j.AbstractLauncher implements org.sat4j.specs.ILogAble {
org.sat4j.core.ASolverFactory factory
private static final long serialVersionUID
protected org.sat4j.pb.ObjectiveFunction obfct
static final boolean $assertionsDisabled
static void ()
public void ()
void (org.sat4j.core.ASolverFactory)
org.sat4j.core.ASolverFactory factory
public static void main (java.lang.String[])
String[] args
org.sat4j.AbstractLauncher lanceur
protected org.sat4j.reader.Reader createReader (org.sat4j.specs.ISolver, java.lang.String)
org.sat4j.specs.ISolver theSolver
String problemname
protected org.sat4j.specs.ISolver configureSolver (java.lang.String[])
String[] args
org.sat4j.pb.IPBSolver theSolver
org.sat4j.pb.IPBSolver theSolver
String solverName
boolean lower
public void usage ()
protected java.lang.String getInstanceName (java.lang.String[])
String[] args
protected org.sat4j.specs.IProblem readProblem (java.lang.String) throws org.sat4j.reader.ParseFormatException java.io.IOException org.sat4j.specs.ContradictionException
String problemname
org.sat4j.specs.IProblem problem
org.sat4j.pb.ObjectiveFunction obj
}
org/sat4j/pb/LanceurPseudo2007Eclipse.classLanceurPseudo2007Eclipse.java
package org.sat4j.pb
public org.sat4j.pb.LanceurPseudo2007Eclipse extends org.sat4j.pb.LanceurPseudo2007 {
org.sat4j.pb.tools.XplainPB quickxplain
private static final long serialVersionUID
protected org.sat4j.specs.ISolver configureSolver (java.lang.String[])
String[] args
org.sat4j.pb.IPBSolver theSolver
org.sat4j.pb.IPBSolver theSolver
public void ()
protected org.sat4j.reader.Reader createReader (org.sat4j.specs.ISolver, java.lang.String)
org.sat4j.specs.ISolver theSolver
String problemname
public static void main (java.lang.String[])
String[] args
org.sat4j.AbstractLauncher lanceur
protected void displayResult ()
org.sat4j.ExitCode exitCode
java.util.Collection explanation
}
org/sat4j/pb/UserFriendlyPBStringSolver$1.classUserFriendlyPBStringSolver.java
package org.sat4j.pb
org.sat4j.pb.UserFriendlyPBStringSolver$1 extends java.lang.Object implements org.sat4j.specs.IConstr {
void ()
public int size ()
public boolean learnt ()
public double getActivity ()
public int get (int)
int i
public boolean canBePropagatedMultipleTimes ()
}
org/sat4j/pb/ConstraintRelaxingPseudoOptDecorator.classConstraintRelaxingPseudoOptDecorator.java
package org.sat4j.pb
public org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator extends org.sat4j.pb.PBSolverDecorator implements org.sat4j.specs.IOptimizationProblem {
private static final long serialVersionUID
private org.sat4j.specs.IConstr previousPBConstr
private org.sat4j.specs.IConstr addedConstr
private Number objectiveValue
private boolean optimumFound
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public boolean isSatisfiable () throws org.sat4j.specs.TimeoutException
public boolean isSatisfiable (boolean) throws org.sat4j.specs.TimeoutException
boolean global
public boolean isSatisfiable (org.sat4j.specs.IVecInt, boolean) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
boolean global
boolean result
public boolean isSatisfiable (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
public boolean admitABetterSolution () throws org.sat4j.specs.TimeoutException
public boolean admitABetterSolution (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
boolean isSatisfiable
int maxValue
public boolean hasNoObjectiveFunction ()
public boolean nonOptimalMeansSatisfiable ()
public java.lang.Number calculateObjective ()
public java.lang.Number getObjectiveValue ()
public void forceObjectiveValueTo (java.lang.Number) throws org.sat4j.specs.ContradictionException
Number forcedValue
public void discard ()
public void discardCurrentSolution ()
public boolean isOptimal ()
public java.lang.String toString (java.lang.String)
String prefix
public void setTimeoutForFindingBetterSolution (int)
int seconds
}
org/sat4j/pb/OPBStringSolver$1.classOPBStringSolver.java
package org.sat4j.pb
org.sat4j.pb.OPBStringSolver$1 extends java.lang.Object implements org.sat4j.specs.IConstr {
void ()
public int size ()
public boolean learnt ()
public double getActivity ()
public int get (int)
int i
public boolean canBePropagatedMultipleTimes ()
}
org/sat4j/pb/PseudoBitsAdderDecorator.classPseudoBitsAdderDecorator.java
package org.sat4j.pb
public org.sat4j.pb.PseudoBitsAdderDecorator extends org.sat4j.tools.SolverDecorator implements org.sat4j.pb.IPBSolver {
private static final long serialVersionUID
private org.sat4j.pb.ObjectiveFunction objfct
private final org.sat4j.tools.GateTranslator gator
private final org.sat4j.pb.IPBSolver solver
static final boolean $assertionsDisabled
static void ()
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction objf
public boolean isSatisfiable () throws org.sat4j.specs.TimeoutException
public boolean isSatisfiable (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
org.sat4j.specs.IVecInt bitsLiterals
org.sat4j.specs.IVecInt fixedLiterals
org.sat4j.specs.IVecInt nAssumpts
boolean result
int litIndex
int j
Number value
public static void main (java.lang.String[])
String[] args
org.sat4j.pb.PseudoBitsAdderDecorator decorator
org.sat4j.pb.reader.OPBReader2007 reader
long begin
org.sat4j.specs.IProblem problem
java.io.FileNotFoundException e
org.sat4j.reader.ParseFormatException e
java.io.IOException e
long end
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
}
org/sat4j/pb/orders/RandomWalkDecoratorObjective.classRandomWalkDecoratorObjective.java
package org.sat4j.pb.orders
public org.sat4j.pb.orders.RandomWalkDecoratorObjective extends org.sat4j.minisat.orders.RandomWalkDecorator implements org.sat4j.pb.orders.IOrderObjective {
private static final long serialVersionUID
private final org.sat4j.pb.orders.IOrderObjective objorder
public void (org.sat4j.pb.orders.VarOrderHeapObjective, double)
org.sat4j.pb.orders.VarOrderHeapObjective order
double p
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
}
org/sat4j/pb/orders/IOrderObjective.classIOrderObjective.java
package org.sat4j.pb.orders
public abstract org.sat4j.pb.orders.IOrderObjective extends java.lang.Object implements org.sat4j.minisat.core.IOrder {
public abstract void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
}
org/sat4j/pb/orders/package-info.classpackage-info.java
package org.sat4j.pb.orders
abstract org.sat4j.pb.orders.package-info extends java.lang.Object {
}
org/sat4j/pb/orders/VarOrderHeapObjective.classVarOrderHeapObjective.java
package org.sat4j.pb.orders
public org.sat4j.pb.orders.VarOrderHeapObjective extends org.sat4j.minisat.orders.VarOrderHeap implements org.sat4j.pb.orders.IOrderObjective {
private static final long serialVersionUID
private org.sat4j.pb.ObjectiveFunction obj
public void ()
public void (org.sat4j.minisat.core.IPhaseSelectionStrategy)
org.sat4j.minisat.core.IPhaseSelectionStrategy strategy
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public void init ()
org.sat4j.specs.IVecInt vars
org.sat4j.specs.IVec coefs
int i
int dimacsLiteral
int p
java.math.BigInteger c
int var
public java.lang.String toString ()
}
org/sat4j/pb/OPBStringSolver.classOPBStringSolver.java
package org.sat4j.pb
public org.sat4j.pb.OPBStringSolver extends org.sat4j.tools.DimacsStringSolver implements org.sat4j.pb.IPBSolver {
private static final String FAKE_I_CONSTR_MSG
private static final long serialVersionUID
private int indxConstrObj
private int nbOfConstraints
private org.sat4j.pb.ObjectiveFunction obj
private boolean inserted
private static final org.sat4j.specs.IConstr FAKE_CONSTR
static final boolean $assertionsDisabled
static void ()
public void ()
public void (int)
int initSize
public boolean isSatisfiable (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
org.sat4j.specs.IteratorInt it
int p
public boolean isSatisfiable (org.sat4j.specs.IVecInt, boolean) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
boolean global
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
StringBuffer out
int negationweight
int p
org.sat4j.specs.IteratorInt iterator
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
StringBuffer out
int negationweight
int p
org.sat4j.specs.IteratorInt iterator
public org.sat4j.specs.IConstr addClause (org.sat4j.specs.IVecInt) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
StringBuffer out
int negationweight
int lit
org.sat4j.specs.IteratorInt iterator
public java.lang.String getExplanation ()
public void setListOfVariablesForExplanation (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt listOfVariables
public java.lang.String toString ()
StringBuffer out
StringBuffer tmp
public java.lang.String toString (java.lang.String)
String prefix
public int newVar (int)
int howmany
StringBuffer out
public void setExpectedNumberOfClauses (int)
int nb
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public int nConstraints ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
StringBuffer out
int i
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
StringBuffer out
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
StringBuffer out
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
StringBuffer out
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int weight
StringBuffer out
int negationweight
int p
org.sat4j.specs.IteratorInt iterator
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
StringBuffer out
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
StringBuffer out
int i
}
org/sat4j/pb/LPStringSolver$1.classLPStringSolver.java
package org.sat4j.pb
org.sat4j.pb.LPStringSolver$1 extends java.lang.Object implements org.sat4j.specs.IConstr {
void ()
public int size ()
public boolean learnt ()
public double getActivity ()
public int get (int)
int i
public boolean canBePropagatedMultipleTimes ()
}
org/sat4j/pb/package-info.classpackage-info.java
package org.sat4j.pb
abstract org.sat4j.pb.package-info extends java.lang.Object {
}
org/sat4j/pb/OptToPBSATAdapter.classOptToPBSATAdapter.java
package org.sat4j.pb
public org.sat4j.pb.OptToPBSATAdapter extends org.sat4j.pb.PBSolverDecorator {
private static final long serialVersionUID
org.sat4j.specs.IOptimizationProblem problem
private final org.sat4j.specs.IVecInt assumps
private long begin
private org.sat4j.tools.SolutionFoundListener sfl
public void (org.sat4j.specs.IOptimizationProblem)
org.sat4j.specs.IOptimizationProblem problem
public void (org.sat4j.specs.IOptimizationProblem, org.sat4j.tools.SolutionFoundListener)
org.sat4j.specs.IOptimizationProblem problem
org.sat4j.tools.SolutionFoundListener sfl
public boolean isSatisfiable () throws org.sat4j.specs.TimeoutException
public boolean isSatisfiable (boolean) throws org.sat4j.specs.TimeoutException
boolean global
public boolean isSatisfiable (org.sat4j.specs.IVecInt, boolean) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt myAssumps
boolean global
public boolean isSatisfiable (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt myAssumps
boolean satisfiable
org.sat4j.specs.TimeoutException e
public int[] model ()
public int[] model (java.io.PrintWriter)
java.io.PrintWriter out
public boolean model (int)
int var
public java.lang.String toString (java.lang.String)
String prefix
public boolean isOptimal ()
public java.lang.Number getCurrentObjectiveValue ()
public void setTimeoutForFindingBetterSolution (int)
int seconds
public void setSolutionFoundListener (org.sat4j.tools.SolutionFoundListener)
org.sat4j.tools.SolutionFoundListener sfl
}
org/sat4j/pb/ObjectiveFunction.classObjectiveFunction.java
package org.sat4j.pb
public org.sat4j.pb.ObjectiveFunction extends java.lang.Object implements java.io.Serializable {
private static final long serialVersionUID
private final org.sat4j.specs.IVec coeffs
private final org.sat4j.specs.IVecInt vars
private java.math.BigInteger correction
public void (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec)
org.sat4j.specs.IVecInt vars
org.sat4j.specs.IVec coeffs
public java.math.BigInteger calculateDegree (org.sat4j.specs.RandomAccessModel)
org.sat4j.specs.RandomAccessModel lazyModel
java.math.BigInteger tempDegree
int i
java.math.BigInteger coeff
public java.math.BigInteger calculateDegreeImplicant (org.sat4j.specs.ISolver)
org.sat4j.specs.ISolver solver
java.math.BigInteger tempDegree
int i
java.math.BigInteger coeff
private boolean varInModel (int, org.sat4j.specs.RandomAccessModel)
int var
org.sat4j.specs.RandomAccessModel lazyModel
public org.sat4j.specs.IVec getCoeffs ()
public org.sat4j.specs.IVecInt getVars ()
public void setCorrection (java.math.BigInteger)
java.math.BigInteger correction
public java.math.BigInteger getCorrection ()
public java.lang.String toString ()
StringBuffer stb
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coefs
java.math.BigInteger coef
int lit
int i
public java.math.BigInteger minValue ()
java.math.BigInteger tempDegree
int i
java.math.BigInteger coeff
public int hashCode ()
public boolean equals (java.lang.Object)
Object obj
org.sat4j.pb.ObjectiveFunction of
}
org/sat4j/pb/UserFriendlyPBStringSolver.classUserFriendlyPBStringSolver.java
package org.sat4j.pb
public org.sat4j.pb.UserFriendlyPBStringSolver extends org.sat4j.tools.DimacsStringSolver implements org.sat4j.pb.IPBSolver {
private static final String FAKE_I_CONSTR_MSG
private static final long serialVersionUID
private int indxConstrObj
private int nbOfConstraints
private org.sat4j.pb.ObjectiveFunction obj
private boolean inserted
private static final org.sat4j.specs.IConstr FAKE_CONSTR
private java.util.Map mapping
static final boolean $assertionsDisabled
static void ()
public void ()
public void (int)
int initSize
public void setMapping (java.util.Map)
java.util.Map mapping
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
StringBuffer out
int i
int i
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
StringBuffer out
org.sat4j.specs.IteratorInt iterator
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
StringBuffer out
org.sat4j.specs.IteratorInt iterator
public org.sat4j.specs.IConstr addClause (org.sat4j.specs.IVecInt) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
StringBuffer out
int lit
boolean beginning
org.sat4j.specs.IteratorInt iterator
public java.lang.String getExplanation ()
public void setListOfVariablesForExplanation (org.sat4j.specs.IVecInt)
org.sat4j.specs.IVecInt listOfVariables
public java.lang.String toString ()
StringBuffer out
StringBuffer tmp
private java.lang.Object decode (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj2
StringBuffer stb
org.sat4j.specs.IVecInt vars
org.sat4j.specs.IVec coeffs
int lit
int i
public java.lang.String toString (java.lang.String)
String prefix
public int newVar (int)
int howmany
StringBuffer out
public void setExpectedNumberOfClauses (int)
int nb
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
StringBuffer out
int i
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
StringBuffer out
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
StringBuffer out
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
StringBuffer out
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
StringBuffer out
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
StringBuffer out
int i
}
org/sat4j/pb/IPBSolverService.classIPBSolverService.java
package org.sat4j.pb
public abstract org.sat4j.pb.IPBSolverService extends java.lang.Object implements org.sat4j.specs.ISolverService {
public abstract org.sat4j.specs.IConstr addAtMostOnTheFly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
public abstract org.sat4j.specs.IConstr addAtMostOnTheFly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int)
public abstract org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
}
org/sat4j/pb/PseudoOptDecorator.classPseudoOptDecorator.java
package org.sat4j.pb
public org.sat4j.pb.PseudoOptDecorator extends org.sat4j.pb.PBSolverDecorator implements org.sat4j.specs.IOptimizationProblem {
private static final long serialVersionUID
private java.math.BigInteger objectiveValue
private int[] prevmodel
private int[] prevmodelwithadditionalvars
private boolean[] prevfullmodel
private org.sat4j.specs.IConstr previousPBConstr
private boolean isSolutionOptimal
private final boolean nonOptimalMeansSatisfiable
private final boolean useAnImplicantForEvaluation
private int solverTimeout
private int optimizationTimeout
static final boolean $assertionsDisabled
static void ()
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver solver
public void (org.sat4j.pb.IPBSolver, boolean)
org.sat4j.pb.IPBSolver solver
boolean nonOptimalMeansSatisfiable
public void (org.sat4j.pb.IPBSolver, boolean, boolean)
org.sat4j.pb.IPBSolver solver
boolean nonOptimalMeansSatisfiable
boolean useAnImplicantForEvaluation
public boolean isSatisfiable () throws org.sat4j.specs.TimeoutException
public boolean isSatisfiable (boolean) throws org.sat4j.specs.TimeoutException
boolean global
public boolean isSatisfiable (org.sat4j.specs.IVecInt, boolean) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
boolean global
boolean result
int i
public boolean isSatisfiable (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction objf
public boolean admitABetterSolution () throws org.sat4j.specs.TimeoutException
public boolean admitABetterSolution (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
boolean result
int i
org.sat4j.specs.TimeoutException te
private int[] modelWithAdaptedNonPrimeLiterals ()
int[] completeModel
int var
int i
org.sat4j.pb.ObjectiveFunction obj
int i
int d
java.math.BigInteger coeff
public boolean hasNoObjectiveFunction ()
public boolean nonOptimalMeansSatisfiable ()
public java.lang.Number calculateObjective ()
public void discardCurrentSolution () throws org.sat4j.specs.ContradictionException
public void reset ()
public int[] model ()
public boolean model (int)
int var
public java.lang.String toString (java.lang.String)
String prefix
public java.lang.Number getObjectiveValue ()
public void discard () throws org.sat4j.specs.ContradictionException
public void forceObjectiveValueTo (java.lang.Number) throws org.sat4j.specs.ContradictionException
Number forcedValue
public boolean isOptimal ()
public int[] modelWithInternalVariables ()
public void setTimeoutForFindingBetterSolution (int)
int seconds
public void setTimeout (int)
int t
}
org/sat4j/pb/core/PBSolverWithImpliedClause.classPBSolverWithImpliedClause.java
package org.sat4j.pb.core
public org.sat4j.pb.core.PBSolverWithImpliedClause extends org.sat4j.pb.core.PBSolverCP {
private static final long serialVersionUID
static final boolean $assertionsDisabled
static void ()
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger degree
org.sat4j.specs.IVecInt vlits
org.sat4j.pb.constraints.pb.PBConstr result
org.sat4j.specs.IVecInt clits
public java.lang.String toString (java.lang.String)
String prefix
}
org/sat4j/pb/core/IPBCDCLSolver.classIPBCDCLSolver.java
package org.sat4j.pb.core
public abstract org.sat4j.pb.core.IPBCDCLSolver extends java.lang.Object implements org.sat4j.pb.IPBSolver org.sat4j.minisat.core.ICDCL {
}
org/sat4j/pb/core/PBSolverStats.classPBSolverStats.java
package org.sat4j.pb.core
public org.sat4j.pb.core.PBSolverStats extends org.sat4j.minisat.core.SolverStats {
private static final long serialVersionUID
public long numberOfReductions
public long numberOfLearnedConstraintsReduced
public long numberOfResolution
public long numberOfCP
public void ()
public void reset ()
public void printStat (java.io.PrintWriter, java.lang.String)
java.io.PrintWriter out
String prefix
}
org/sat4j/pb/core/PBSolver.classPBSolver.java
package org.sat4j.pb.core
public abstract org.sat4j.pb.core.PBSolver extends org.sat4j.minisat.core.Solver implements org.sat4j.pb.core.IPBCDCLSolver org.sat4j.pb.IPBSolverService {
private org.sat4j.pb.ObjectiveFunction objf
private static final long serialVersionUID
protected org.sat4j.pb.core.PBSolverStats stats
public final org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy objectiveFunctionBased
static final boolean $assertionsDisabled
static void ()
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder, org.sat4j.minisat.core.RestartStrategy)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
org.sat4j.minisat.core.RestartStrategy restarter
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.SearchParams, org.sat4j.minisat.core.IOrder, org.sat4j.minisat.core.RestartStrategy)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.SearchParams params
org.sat4j.minisat.core.IOrder order
org.sat4j.minisat.core.RestartStrategy restarter
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger degree
org.sat4j.specs.IVecInt vlits
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
org.sat4j.minisat.core.IOrder order
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
org.sat4j.specs.IVec bcoeffs
int i
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
org.sat4j.specs.IVecInt vlits
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
org.sat4j.specs.IVec bcoeffs
int i
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
org.sat4j.specs.IVecInt vlits
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
org.sat4j.specs.IVec bcoeffs
int i
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
org.sat4j.specs.IVecInt vlits
org.sat4j.core.ConstrGroup group
public org.sat4j.specs.IConstr addAtMostOnTheFly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coefs
java.math.BigInteger degree
org.sat4j.specs.IVecInt vlits
org.sat4j.specs.IVecInt outReason
java.util.Set subset
org.sat4j.specs.IteratorInt it
public org.sat4j.specs.IConstr addAtMostOnTheFly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int)
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coefs
int degree
org.sat4j.specs.IVec coeffsCpy
org.sat4j.specs.IteratorInt iterator
static org.sat4j.specs.IVec access$0 (org.sat4j.pb.core.PBSolver)
static org.sat4j.pb.ObjectiveFunction access$1 (org.sat4j.pb.core.PBSolver)
}
org/sat4j/pb/core/ObjectiveReducerPBSolverDecorator.classObjectiveReducerPBSolverDecorator.java
package org.sat4j.pb.core
public org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator extends java.lang.Object implements org.sat4j.pb.IPBSolver {
private static final long serialVersionUID
private final org.sat4j.pb.IPBSolver decorated
private final java.util.List atMostOneCstrs
public void (org.sat4j.pb.IPBSolver)
org.sat4j.pb.IPBSolver decorated
public int[] model ()
public int newVar ()
public org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt lits
org.sat4j.specs.IVec coeffs
boolean moreThan
java.math.BigInteger d
public boolean model (int)
int var
public int nextFreeVarId (boolean)
boolean reserve
public int[] primeImplicant ()
public boolean primeImplicant (int)
int p
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
org.sat4j.specs.IteratorInt it
public boolean isSatisfiable () throws org.sat4j.specs.TimeoutException
public boolean isSatisfiable (org.sat4j.specs.IVecInt, boolean) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
boolean globalTimeout
public void registerLiteral (int)
int p
public void setExpectedNumberOfClauses (int)
int nb
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
java.util.Iterator it
public boolean isSatisfiable (boolean) throws org.sat4j.specs.TimeoutException
boolean globalTimeout
public org.sat4j.specs.IConstr addClause (org.sat4j.specs.IVecInt) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
public boolean isSatisfiable (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int degree
public int[] findModel () throws org.sat4j.specs.TimeoutException
public org.sat4j.specs.IConstr addBlockingClause (org.sat4j.specs.IVecInt) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
public boolean removeConstr (org.sat4j.specs.IConstr)
org.sat4j.specs.IConstr c
public int[] findModel (org.sat4j.specs.IVecInt) throws org.sat4j.specs.TimeoutException
org.sat4j.specs.IVecInt assumps
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger degree
public boolean removeSubsumedConstr (org.sat4j.specs.IConstr)
org.sat4j.specs.IConstr c
public int nConstraints ()
public int newVar (int)
int howmany
public void addAllClauses (org.sat4j.specs.IVec) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVec clauses
java.util.Iterator it
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVecInt coeffs
int weight
public int nVars ()
public void printInfos (java.io.PrintWriter, java.lang.String)
java.io.PrintWriter out
String prefix
public org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
org.sat4j.specs.IVec coeffs
java.math.BigInteger weight
public void printInfos (java.io.PrintWriter)
java.io.PrintWriter out
public org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int degree
public void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
org.sat4j.pb.ObjectiveFunction obj
org.sat4j.specs.IVecInt newVars
org.sat4j.specs.IVec newCoeffs
java.util.Set oldVarsToIgnore
org.sat4j.specs.IVecInt oldObjVars
org.sat4j.specs.IVec oldObjCoeffs
int nbReduc
int i
private int processAtMostOneCstrs (org.sat4j.pb.ObjectiveFunction, org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.util.Set)
org.sat4j.pb.ObjectiveFunction obj
org.sat4j.specs.IVecInt newVars
org.sat4j.specs.IVec newCoeffs
java.util.Set oldVarsToIgnore
int nbReduc
org.sat4j.specs.IVecInt oldObjVars
org.sat4j.specs.IVec oldObjCoeffs
org.sat4j.specs.IVecInt lits
boolean allLitsIn
org.sat4j.specs.IteratorInt it
int next
int indexOf
int newObjVar
org.sat4j.specs.IteratorInt it
int nextInt
org.sat4j.specs.ContradictionException e
public org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
public org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
org.sat4j.specs.IVecInt literals
int n
public void setTimeout (int)
int t
public void setTimeoutOnConflicts (int)
int count
public void setTimeoutMs (long)
long t
public int getTimeout ()
public long getTimeoutMs ()
public void expireTimeout ()
public void reset ()
public void printStat (java.io.PrintStream, java.lang.String)
java.io.PrintStream out
String prefix
public void printStat (java.io.PrintWriter, java.lang.String)
java.io.PrintWriter out
String prefix
public void printStat (java.io.PrintWriter)
java.io.PrintWriter out
public java.util.Map getStat ()
public java.lang.String toString (java.lang.String)
String prefix
public void clearLearntClauses ()
public void setDBSimplificationAllowed (boolean)
boolean status
public boolean isDBSimplificationAllowed ()
public void setSearchListener (org.sat4j.specs.SearchListener)
org.sat4j.specs.SearchListener sl
public org.sat4j.specs.SearchListener getSearchListener ()
public boolean isVerbose ()
public void setVerbose (boolean)
boolean value
public void setLogPrefix (java.lang.String)
String prefix
public java.lang.String getLogPrefix ()
public org.sat4j.specs.IVecInt unsatExplanation ()
public int[] modelWithInternalVariables ()
public int realNumberOfVariables ()
public boolean isSolverKeptHot ()
public void setKeepSolverHot (boolean)
boolean keepHot
public org.sat4j.specs.ISolver getSolvingEngine ()
public void setUnitClauseProvider (org.sat4j.specs.UnitClauseProvider)
org.sat4j.specs.UnitClauseProvider ucp
}
org/sat4j/pb/core/PBSolverResCP.classPBSolverResCP.java
package org.sat4j.pb.core
public org.sat4j.pb.core.PBSolverResCP extends org.sat4j.pb.core.PBSolverCP {
private static final long serialVersionUID
public static final long MAXCONFLICTS
private long bound
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder, long)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
long bound
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.SearchParams, org.sat4j.minisat.core.IOrder, org.sat4j.minisat.core.RestartStrategy)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.SearchParams params
org.sat4j.minisat.core.IOrder order
org.sat4j.minisat.core.RestartStrategy restarter
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.SearchParams, org.sat4j.minisat.core.IOrder)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.SearchParams params
org.sat4j.minisat.core.IOrder order
boolean someCriteria ()
}
org/sat4j/pb/core/PBSolverResolution.classPBSolverResolution.java
package org.sat4j.pb.core
public org.sat4j.pb.core.PBSolverResolution extends org.sat4j.pb.core.PBSolver {
private static final long serialVersionUID
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.SearchParams, org.sat4j.minisat.core.IOrder, org.sat4j.minisat.core.RestartStrategy)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.SearchParams params
org.sat4j.minisat.core.IOrder order
org.sat4j.minisat.core.RestartStrategy restarter
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder, org.sat4j.minisat.core.RestartStrategy)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
org.sat4j.minisat.core.RestartStrategy restarter
}
org/sat4j/pb/core/PBDataStructureFactory.classPBDataStructureFactory.java
package org.sat4j.pb.core
public abstract org.sat4j.pb.core.PBDataStructureFactory extends java.lang.Object implements org.sat4j.minisat.core.DataStructureFactory {
public abstract org.sat4j.minisat.core.Constr createPseudoBooleanConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.minisat.core.Constr createAtMostPBConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.minisat.core.Constr createAtLeastPBConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.minisat.core.Constr createUnregisteredPseudoBooleanConstraint (org.sat4j.pb.constraints.pb.IDataStructurePB)
public abstract org.sat4j.minisat.core.Constr createUnregisteredAtMostConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
public abstract org.sat4j.minisat.core.Constr createUnregisteredAtLeastConstraint (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger)
}
org/sat4j/pb/core/package-info.classpackage-info.java
package org.sat4j.pb.core
abstract org.sat4j.pb.core.package-info extends java.lang.Object {
}
org/sat4j/pb/core/PBSolverClause.classPBSolverClause.java
package org.sat4j.pb.core
public org.sat4j.pb.core.PBSolverClause extends org.sat4j.pb.core.PBSolverCP {
private static final long serialVersionUID
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
org.sat4j.pb.constraints.pb.IConflict chooseConflict (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr myconfl
int level
public java.lang.String toString (java.lang.String)
String prefix
}
org/sat4j/pb/core/PBSolver$1.classPBSolver.java
package org.sat4j.pb.core
org.sat4j.pb.core.PBSolver$1 extends java.lang.Object implements org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy {
private static final long serialVersionUID
private boolean[] inObjectiveFunction
private final org.sat4j.minisat.core.ConflictTimer clauseManagement
final org.sat4j.pb.core.PBSolver this$0
void (org.sat4j.pb.core.PBSolver)
public void reduce (org.sat4j.specs.IVec)
org.sat4j.specs.IVec learnedConstrs
int i
int j
org.sat4j.minisat.core.Constr c
public org.sat4j.minisat.core.ConflictTimer getTimer ()
public java.lang.String toString ()
public void init ()
org.sat4j.specs.IteratorInt it
public void onClauseLearning (org.sat4j.minisat.core.Constr)
org.sat4j.minisat.core.Constr constr
boolean fullObj
int i
public void onConflictAnalysis (org.sat4j.minisat.core.Constr)
org.sat4j.minisat.core.Constr reason
public void onPropagation (org.sat4j.minisat.core.Constr)
org.sat4j.minisat.core.Constr from
static org.sat4j.pb.core.PBSolver access$0 (org.sat4j.pb.core.PBSolver$1)
}
org/sat4j/pb/core/PBSolver$1$1.classPBSolver.java
package org.sat4j.pb.core
org.sat4j.pb.core.PBSolver$1$1 extends org.sat4j.minisat.core.ConflictTimerAdapter {
private static final long serialVersionUID
private int nbconflict
private static final int MAX_CLAUSE
private static final int INC_CLAUSE
private int nextbound
final org.sat4j.pb.core.PBSolver$1 this$1
void (org.sat4j.pb.core.PBSolver$1, int)
int $anonymous0
public void run ()
public void reset ()
}
org/sat4j/pb/core/PBSolverCP.classPBSolverCP.java
package org.sat4j.pb.core
public org.sat4j.pb.core.PBSolverCP extends org.sat4j.pb.core.PBSolver {
private static final long serialVersionUID
private final org.sat4j.specs.IVec conflictVariables
private final org.sat4j.specs.IVec conflictConstraints
static final boolean $assertionsDisabled
static void ()
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.SearchParams, org.sat4j.minisat.core.IOrder, org.sat4j.minisat.core.RestartStrategy)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.SearchParams params
org.sat4j.minisat.core.IOrder order
org.sat4j.minisat.core.RestartStrategy restarter
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.SearchParams, org.sat4j.minisat.core.IOrder)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.SearchParams params
org.sat4j.minisat.core.IOrder order
public void analyze (org.sat4j.minisat.core.Constr, org.sat4j.minisat.core.Pair) throws org.sat4j.specs.TimeoutException
org.sat4j.minisat.core.Constr myconfl
org.sat4j.minisat.core.Pair results
public void analyzeCP (org.sat4j.minisat.core.Constr, org.sat4j.minisat.core.Pair) throws org.sat4j.specs.TimeoutException
org.sat4j.minisat.core.Constr myconfl
org.sat4j.minisat.core.Pair results
int litImplied
int currentLevel
org.sat4j.pb.constraints.pb.IConflict confl
org.sat4j.pb.constraints.pb.PBConstr constraint
org.sat4j.pb.constraints.pb.PBConstr resConstr
org.sat4j.pb.constraints.pb.IConflict chooseConflict (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr myconfl
int level
public java.lang.String toString (java.lang.String)
String prefix
void initExplanation ()
boolean someCriteria ()
protected void updateNumberOfReductions (org.sat4j.pb.constraints.pb.IConflict)
org.sat4j.pb.constraints.pb.IConflict confl
protected void updateNumberOfReducedLearnedConstraints (org.sat4j.pb.constraints.pb.IConflict)
org.sat4j.pb.constraints.pb.IConflict confl
}
org/sat4j/pb/core/PBSolverCautious.classPBSolverCautious.java
package org.sat4j.pb.core
public org.sat4j.pb.core.PBSolverCautious extends org.sat4j.pb.core.PBSolverCP {
private static final long serialVersionUID
public static final int BOUND
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
public void (org.sat4j.minisat.core.LearningStrategy, org.sat4j.pb.core.PBDataStructureFactory, org.sat4j.minisat.core.IOrder, int)
org.sat4j.minisat.core.LearningStrategy learner
org.sat4j.pb.core.PBDataStructureFactory dsf
org.sat4j.minisat.core.IOrder order
int bound
org.sat4j.pb.constraints.pb.IConflict chooseConflict (org.sat4j.pb.constraints.pb.PBConstr, int)
org.sat4j.pb.constraints.pb.PBConstr myconfl
int level
public java.lang.String toString (java.lang.String)
String prefix
protected void updateNumberOfReductions (org.sat4j.pb.constraints.pb.IConflict)
org.sat4j.pb.constraints.pb.IConflict confl
protected void updateNumberOfReducedLearnedConstraints (org.sat4j.pb.constraints.pb.IConflict)
org.sat4j.pb.constraints.pb.IConflict confl
}
org/sat4j/pb/LanceurPseudo2007.classLanceurPseudo2007.java
package org.sat4j.pb
public org.sat4j.pb.LanceurPseudo2007 extends org.sat4j.pb.LanceurPseudo2005 {
private static final long serialVersionUID
public void ()
public void (org.sat4j.core.ASolverFactory)
org.sat4j.core.ASolverFactory factory
protected org.sat4j.reader.Reader createReader (org.sat4j.specs.ISolver, java.lang.String)
org.sat4j.specs.ISolver theSolver
String problemname
public static void main (java.lang.String[])
String[] args
org.sat4j.AbstractLauncher lanceur
}
org/sat4j/pb/IPBSolver.classIPBSolver.java
package org.sat4j.pb
public abstract org.sat4j.pb.IPBSolver extends java.lang.Object implements org.sat4j.specs.ISolver {
public abstract org.sat4j.specs.IConstr addPseudoBoolean (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, boolean, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.specs.IConstr addAtMost (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.specs.IConstr addAtLeast (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVecInt, int) throws org.sat4j.specs.ContradictionException
public abstract org.sat4j.specs.IConstr addExactly (org.sat4j.specs.IVecInt, org.sat4j.specs.IVec, java.math.BigInteger) throws org.sat4j.specs.ContradictionException
public abstract void setObjectiveFunction (org.sat4j.pb.ObjectiveFunction)
public abstract org.sat4j.pb.ObjectiveFunction getObjectiveFunction ()
}
plugin.properties
about.html