|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use ContradictionException | |
---|---|
org.sat4j | Contains a command line launcher for the SAT solvers. |
org.sat4j.csp | Classes needed for CSP to SAT translation. |
org.sat4j.csp.constraints | Classes needed for CSP to SAT translation. |
org.sat4j.csp.encodings | |
org.sat4j.maxsat | MAXSAT and Weighted Max SAT framework. |
org.sat4j.maxsat.reader | Some utility classes to read problems from plain text files. |
org.sat4j.minisat.constraints | Implementations of various constraints for MiniSAT. |
org.sat4j.minisat.constraints.card | Implementations of cardinality contraints. |
org.sat4j.minisat.constraints.cnf | Implementations of clausal contraints. |
org.sat4j.minisat.core | Implementation of the MiniSAT solver skeleton. |
org.sat4j.multicore | |
org.sat4j.opt | Built-in optimization framework. |
org.sat4j.pb | |
org.sat4j.pb.constraints | |
org.sat4j.pb.constraints.pb | Implementations of pseudo boolean contraints. |
org.sat4j.pb.core | |
org.sat4j.pb.reader | |
org.sat4j.pb.tools | |
org.sat4j.reader | Some utility classes to read problems from plain text files. |
org.sat4j.sat | |
org.sat4j.specs | Those classes are intented for users dealing with SAT solvers as blackboxes. |
org.sat4j.tools | Tools to be used on top of an ISolver. |
org.sat4j.tools.xplain |
Uses of ContradictionException in org.sat4j |
---|
Methods in org.sat4j that throw ContradictionException | |
---|---|
protected IProblem |
AbstractLauncher.readProblem(String problemname)
Reads a problem file from the command line. |
Uses of ContradictionException in org.sat4j.csp |
---|
Methods in org.sat4j.csp that throw ContradictionException | |
---|---|
void |
Encoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
Encoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
Encoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
Var.toClause(ISolver solver)
|
void |
Constant.toClause(ISolver solver)
|
void |
Evaluable.toClause(ISolver solver)
Translates a variable over a domain into a set a clauses enforcing that exactly one value must be chosen in the domain. |
void |
Predicate.toClause(ISolver solver,
IVec<Var> vscope,
IVec<Evaluable> vars)
|
void |
Clausifiable.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
Uses of ContradictionException in org.sat4j.csp.constraints |
---|
Methods in org.sat4j.csp.constraints that throw ContradictionException | |
---|---|
void |
Nogoods.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
AllDiff.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
void |
Supports.toClause(ISolver solver,
IVec<Var> scope,
IVec<Evaluable> vars)
|
Uses of ContradictionException in org.sat4j.csp.encodings |
---|
Methods in org.sat4j.csp.encodings that throw ContradictionException | |
---|---|
void |
GeneralizedSupportEncoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
BinarySupportEncoding.onFinish(ISolver solver,
IVec<Var> scope)
|
void |
GeneralizedSupportEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
BinarySupportEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
DirectEncoding.onNogood(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
GeneralizedSupportEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
void |
BinarySupportEncoding.onSupport(ISolver solver,
IVec<Var> scope,
Map<Evaluable,Integer> tuple)
|
Uses of ContradictionException in org.sat4j.maxsat |
---|
Methods in org.sat4j.maxsat that throw ContradictionException | |
---|---|
IConstr |
WeightedMaxSatDecorator.addClause(IVecInt literals)
Add a set of literals to the solver. |
IConstr |
WeightedMaxSatDecorator.addHardClause(IVecInt literals)
Add a hard clause in the solver, i.e. a clause that must be satisfied. |
IConstr |
WeightedMaxSatDecorator.addSoftClause(BigInteger weight,
IVecInt literals)
|
IConstr |
WeightedMaxSatDecorator.addSoftClause(int weight,
IVecInt literals)
Add a soft clause to the solver. |
IConstr |
WeightedMaxSatDecorator.addSoftClause(IVecInt literals)
Add a soft clause in the solver, i.e. a clause with a weight of 1. |
void |
WeightedMaxSatDecorator.discard()
|
void |
MinCostDecorator.discard()
|
void |
WeightedMaxSatDecorator.discardCurrentSolution()
|
void |
MinCostDecorator.discardCurrentSolution()
|
void |
WeightedMaxSatDecorator.forceObjectiveValueTo(Number forcedValue)
|
void |
MinCostDecorator.forceObjectiveValueTo(Number forcedValue)
|
Uses of ContradictionException in org.sat4j.maxsat.reader |
---|
Methods in org.sat4j.maxsat.reader that throw ContradictionException | |
---|---|
protected void |
WDimacsReader.flushConstraint()
|
protected boolean |
WDimacsReader.handleLine()
|
Uses of ContradictionException in org.sat4j.minisat.constraints |
---|
Methods in org.sat4j.minisat.constraints that throw ContradictionException | |
---|---|
Constr |
AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructure.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
ClausalDataStructureWL.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureCB.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructure.createClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielHT.createClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielWL.createClause(IVecInt literals)
|
Constr |
MixedDataStructureDanielCBWL.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMin.createClause(IVecInt literals)
|
Constr |
ClausalDataStructureCBWL.createClause(IVecInt literals)
|
Constr |
CardinalityDataStructureYanMax.createClause(IVecInt literals)
|
Uses of ContradictionException in org.sat4j.minisat.constraints.card |
---|
Methods in org.sat4j.minisat.constraints.card that throw ContradictionException | |
---|---|
static Constr |
AtLeast.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
protected MinWatchCard |
MinWatchCard.computePropagation(UnitPropagationListener s)
|
static MaxWatchCard |
MaxWatchCard.maxWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr? |
static MinWatchCard |
MinWatchCard.minWatchCardNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Constructs a cardinality constraint with a minimal set of watched literals Permet la cr? |
protected static int |
AtLeast.niceParameters(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int deg)
|
Uses of ContradictionException in org.sat4j.minisat.constraints.cnf |
---|
Methods in org.sat4j.minisat.constraints.cnf that throw ContradictionException | |
---|---|
static IVecInt |
Clauses.sanityCheck(IVecInt ps,
ILits voc,
UnitPropagationListener s)
Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation |
Uses of ContradictionException in org.sat4j.minisat.core |
---|
Methods in org.sat4j.minisat.core that throw ContradictionException | |
---|---|
void |
Solver.addAllClauses(IVec<IVecInt> clauses)
|
IConstr |
Solver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
Solver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
Solver.addBlockingClause(IVecInt literals)
|
IConstr |
Solver.addClause(IVecInt literals)
|
Constr |
DataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
DataStructureFactory.createClause(IVecInt literals)
|
Uses of ContradictionException in org.sat4j.multicore |
---|
Methods in org.sat4j.multicore that throw ContradictionException | |
---|---|
void |
ManyCore.addAllClauses(IVec<IVecInt> clauses)
|
IConstr |
ManyCore.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
ManyCore.addAtMost(IVecInt literals,
int degree)
|
IConstr |
ManyCore.addBlockingClause(IVecInt literals)
|
IConstr |
ManyCore.addClause(IVecInt literals)
|
IConstr |
ManyCorePB.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
Uses of ContradictionException in org.sat4j.opt |
---|
Methods in org.sat4j.opt that throw ContradictionException | |
---|---|
IConstr |
MaxSatDecorator.addClause(IVecInt literals)
|
void |
MaxSatDecorator.discard()
|
void |
MinOneDecorator.discard()
|
void |
MaxSatDecorator.discardCurrentSolution()
|
void |
MinOneDecorator.discardCurrentSolution()
|
void |
MaxSatDecorator.forceObjectiveValueTo(Number forcedValue)
|
void |
MinOneDecorator.forceObjectiveValueTo(Number forcedValue)
|
Uses of ContradictionException in org.sat4j.pb |
---|
Methods in org.sat4j.pb that throw ContradictionException | |
---|---|
IConstr |
UserFriendlyPBStringSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
OPBStringSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
UserFriendlyPBStringSolver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
OPBStringSolver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
UserFriendlyPBStringSolver.addClause(IVecInt literals)
|
IConstr |
OPBStringSolver.addClause(IVecInt literals)
|
IConstr |
IPBSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied" |
IConstr |
UserFriendlyPBStringSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
PBSolverDecorator.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
IConstr |
OPBStringSolver.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
void |
PseudoOptDecorator.discard()
|
void |
PseudoOptDecorator.discardCurrentSolution()
|
void |
PseudoIteratorDecorator.discardCurrentSolution()
|
void |
PseudoOptDecorator.forceObjectiveValueTo(Number forcedValue)
|
Uses of ContradictionException in org.sat4j.pb.constraints |
---|
Methods in org.sat4j.pb.constraints that throw ContradictionException | |
---|---|
protected abstract Constr |
AbstractPBDataStructureFactory.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree)
|
protected Constr |
AbstractPBClauseCardConstrDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree)
|
protected PBConstr |
PuebloPBMinDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree)
|
protected PBConstr |
PBMinDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree)
|
protected Constr |
PBMaxDataStructure.constraintFactory(int[] literals,
BigInteger[] coefs,
BigInteger degree)
|
protected Constr |
CompetResolutionPBMixedHTClauseCardConstrDataStructure.constructCard(IVecInt theLits,
int degree)
|
protected PBConstr |
PBMaxClauseAtLeastConstrDataStructure.constructCard(IVecInt theLits,
int degree)
|
protected abstract Constr |
AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt theLits,
int degree)
|
protected Constr |
CompetResolutionPBMixedWLClauseCardConstrDataStructure.constructCard(IVecInt theLits,
int degree)
|
protected Constr |
CompetMinHTmixedClauseCardConstrDataStructureFactory.constructCard(IVecInt theLits,
int degree)
|
protected PBConstr |
PuebloPBMinClauseAtLeastConstrDataStructure.constructCard(IVecInt theLits,
int degree)
|
protected Constr |
PuebloPBMinClauseCardConstrDataStructure.constructCard(IVecInt theLits,
int degree)
|
protected abstract Constr |
AbstractPBClauseCardConstrDataStructure.constructPB(int[] theLits,
BigInteger[] coefs,
BigInteger degree)
|
protected PBConstr |
PBMinClauseCardConstrDataStructure.constructPB(int[] theLits,
BigInteger[] coefs,
BigInteger degree)
|
protected Constr |
PuebloPBMinClauseCardConstrDataStructure.constructPB(int[] theLits,
BigInteger[] coefs,
BigInteger degree)
|
protected Constr |
PBMaxClauseCardConstrDataStructure.constructPB(int[] theLits,
BigInteger[] coefs,
BigInteger degree)
|
Constr |
AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals,
int degree)
|
Constr |
CompetResolutionPBMixedHTClauseCardConstrDataStructure.createClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createClause(IVecInt literals)
|
Constr |
CompetResolutionPBMixedWLClauseCardConstrDataStructure.createClause(IVecInt literals)
|
Constr |
PuebloPBMinClauseCardConstrDataStructure.createClause(IVecInt literals)
|
Constr |
AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<BigInteger> coefs,
boolean moreThan,
BigInteger degree)
|
Uses of ContradictionException in org.sat4j.pb.constraints.pb |
---|
Methods in org.sat4j.pb.constraints.pb that throw ContradictionException | |
---|---|
static AtLeastPB |
AtLeastPB.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
protected void |
MaxWatchPb.computePropagation(UnitPropagationListener s)
|
protected abstract void |
WatchPb.computePropagation(UnitPropagationListener s)
|
protected void |
MinWatchPb.computePropagation(UnitPropagationListener s)
|
protected void |
MaxWatchPb.computeWatches()
All the literals are watched. |
protected abstract void |
WatchPb.computeWatches()
|
protected void |
MinWatchPb.computeWatches()
|
static MinWatchCardPB |
MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr? |
static IDataStructurePB |
Pseudos.niceParameters(IVecInt ps,
IVec<BigInteger> bigCoefs,
boolean moreThan,
BigInteger bigDeg,
ILits voc)
|
static BigInteger |
Pseudos.niceParametersForCompetition(int[] ps,
BigInteger[] bigCoefs,
boolean moreThan,
BigInteger bigDeg)
|
static MaxWatchPb |
MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree)
build a pseudo boolean constraint. |
static MinWatchCardPB |
MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int degree)
Permet la cr? |
static MinWatchPb |
MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree)
build a pseudo boolean constraint. |
static PuebloMinWatchPb |
PuebloMinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree)
|
Uses of ContradictionException in org.sat4j.pb.core |
---|
Methods in org.sat4j.pb.core that throw ContradictionException | |
---|---|
IConstr |
PBSolver.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
|
IConstr |
PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger degree)
|
Constr |
PBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals,
IVec<BigInteger> coefs,
boolean moreThan,
BigInteger degree)
|
Uses of ContradictionException in org.sat4j.pb.reader |
---|
Methods in org.sat4j.pb.reader that throw ContradictionException | |
---|---|
protected void |
OPBReader2005.endConstraint()
|
protected void |
OPBReader2010.endConstraint()
|
void |
OPBReader2005.parse()
parses the file and uses the callbacks to send to send the data back to the program |
IProblem |
PBInstanceReader.parseInstance(Reader in)
|
IProblem |
OPBReader2005.parseInstance(Reader input)
|
IProblem |
OPBReader2010.parseInstance(Reader input)
|
IProblem |
PBInstanceReader.parseInstance(String filename)
|
protected void |
OPBReader2005.readConstraint()
read a constraint calls beginConstraint, constraintTerm and endConstraint |
Uses of ContradictionException in org.sat4j.pb.tools |
---|
Methods in org.sat4j.pb.tools that throw ContradictionException | |
---|---|
IConstr |
XplainPB.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
XplainPB.addAtMost(IVecInt literals,
int degree)
|
IConstr |
XplainPB.addPseudoBoolean(IVecInt lits,
IVec<BigInteger> coeffs,
boolean moreThan,
BigInteger d)
|
void |
DependencyHelper.and(C name,
T thing,
T... otherThings)
Create a constraint of the form thing <=> (thing1 and thing 2 ... and thingn) |
ImplicationAnd<T,C> |
ImplicationAnd.and(T thing)
Add a new positive literal to the conjunction of literals. |
ImplicationAnd<T,C> |
ImplicationAnd.andNot(T thing)
Add a new negative literal to the conjunction of literals. |
void |
DependencyHelper.atLeast(C name,
BigInteger degree,
WeightedObject<T>... wobj)
Create a PB constraint of the form
w1.l1 + w2.l2 + ... wn.ln >= degree
where wi are position integers and li are domain objects. |
void |
DependencyHelper.atLeast(C name,
int i,
T... things)
Create a constraint stating that at most i domain object should be set to true. |
void |
DependencyHelper.atMost(C name,
BigInteger degree,
WeightedObject<T>... wobj)
Create a PB constraint of the form
w1.l1 + w2.l2 + ... wn.ln <= degree
where wi are position integers and li are domain objects. |
void |
DependencyHelper.atMost(C name,
int i,
T... things)
Create a constraint stating that at most i domain object should be set to true. |
void |
DependencyHelper.atMost(C name,
int degree,
WeightedObject<T>... wobj)
|
ImplicationNamer<T,C> |
DependencyHelper.atMost(int i,
T... things)
Create a constraint stating that at most i domain object should be set to true. |
void |
DependencyHelper.clause(C name,
T... things)
Create a clause (thing1 or thing 2 ... or thingn) |
void |
DependencyHelper.discard(IVec<T> things)
|
void |
DependencyHelper.discardSolutionsWithObjectiveValueGreaterThan(long value)
|
void |
DependencyHelper.iff(C name,
T thing,
T... otherThings)
Create a constraint using equivalency chains thing <=> (thing1 <=> thing2 <=> ... <=> thingn) |
void |
DependencyHelper.ifThenElse(C name,
T thing,
T conditionThing,
T thenThing,
T elseThing)
Create a constraint of the form thing <=> (if conditionThing then thenThing else elseThing) |
ImplicationNamer<T,C> |
DisjunctionRHS.implies(T... things)
|
ImplicationNamer<T,C> |
ImplicationRHS.implies(T... things)
Build an implication with a disjunction of literals in the RHS. |
ImplicationAnd<T,C> |
ImplicationRHS.implies(T thing)
Build an implication with a conjunction of literals in the RHS. |
ImplicationAnd<T,C> |
ImplicationRHS.impliesNot(T thing)
Build an implication with a conjunction of literals in the RHS. |
void |
DependencyHelper.or(C name,
T thing,
T... otherThings)
Create a constraint of the form thing <=> (thing1 or thing 2 ... or thingn) |
void |
DependencyHelper.setFalse(T thing,
C name)
Add a constraint to set the value of a domain object to false. |
void |
DependencyHelper.setTrue(T thing,
C name)
Add a constraint to set the value of a domain object to true. |
Uses of ContradictionException in org.sat4j.reader |
---|
Uses of ContradictionException in org.sat4j.sat |
---|
Methods in org.sat4j.sat that throw ContradictionException | |
---|---|
protected IProblem |
Lanceur.readProblem(String problemname)
|
Uses of ContradictionException in org.sat4j.specs |
---|
Methods in org.sat4j.specs that throw ContradictionException | |
---|---|
void |
ISolver.addAllClauses(IVec<IVecInt> clauses)
Create clauses from a set of set of literals. |
IConstr |
ISolver.addAtLeast(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at least n of those literals must be satisfied" |
IConstr |
ISolver.addAtMost(IVecInt literals,
int degree)
Create a cardinality constraint of the type "at most n of those literals must be satisfied" |
IConstr |
ISolver.addBlockingClause(IVecInt literals)
Add a clause in order to prevent an assignment to occur. |
IConstr |
ISolver.addClause(IVecInt literals)
Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values. |
void |
IOptimizationProblem.discard()
Deprecated. |
void |
IOptimizationProblem.discardCurrentSolution()
Discard the current solution in the optimization problem. |
void |
IOptimizationProblem.forceObjectiveValueTo(Number forcedValue)
Force the value of the objective function. |
Uses of ContradictionException in org.sat4j.tools |
---|
Methods in org.sat4j.tools that throw ContradictionException | |
---|---|
void |
DimacsOutputSolver.addAllClauses(IVec<IVecInt> clauses)
|
void |
DimacsStringSolver.addAllClauses(IVec<IVecInt> clauses)
|
void |
SolverDecorator.addAllClauses(IVec<IVecInt> clauses)
|
IConstr |
DimacsOutputSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
DimacsStringSolver.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
SolverDecorator.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
DimacsOutputSolver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
DimacsStringSolver.addAtMost(IVecInt literals,
int degree)
|
IConstr |
SolverDecorator.addAtMost(IVecInt literals,
int degree)
|
IConstr |
DimacsOutputSolver.addBlockingClause(IVecInt literals)
|
IConstr |
DimacsStringSolver.addBlockingClause(IVecInt literals)
|
IConstr |
SolverDecorator.addBlockingClause(IVecInt literals)
|
IConstr |
DimacsOutputSolver.addClause(IVecInt literals)
|
IConstr |
DimacsStringSolver.addClause(IVecInt literals)
|
IConstr |
SolverDecorator.addClause(IVecInt literals)
|
void |
GateTranslator.additionalFullAdderConstraints(int xcarry,
int xsum,
int a,
int b,
int c)
|
IConstr[] |
GateTranslator.and(int y,
int x1,
int x2)
Translate y <=> x1 /\ x2 |
IConstr[] |
GateTranslator.and(int y,
IVecInt literals)
Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses. |
void |
GateTranslator.fullAdderCarry(int x,
int a,
int b,
int c)
|
void |
GateTranslator.fullAdderSum(int x,
int a,
int b,
int c)
|
IConstr |
GateTranslator.gateFalse(int y)
translate y <=> FALSE into a clause. |
IConstr |
GateTranslator.gateTrue(int y)
translate y <=> TRUE into a clause. |
void |
GateTranslator.halfAdderCarry(int x,
int a,
int b)
|
void |
GateTranslator.halfAdderSum(int x,
int a,
int b)
|
protected boolean |
DimacsArrayReader.handleConstr(int gateType,
int output,
int[] inputs)
|
protected boolean |
ExtendedDimacsArrayReader.handleConstr(int gateType,
int output,
int[] inputs)
Handles a single constraint (constraint == Extended Dimacs circuit gate). |
IConstr[] |
GateTranslator.iff(int y,
IVecInt literals)
translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses. |
IConstr[] |
GateTranslator.ite(int y,
int x1,
int x2,
int x3)
translate y <=> if x1 then x2 else x3 into clauses. |
IConstr[] |
GateTranslator.not(int y,
int x)
Translate y <=> not x into clauses. |
void |
GateTranslator.optimisationFunction(IVecInt literals,
IVec<BigInteger> coefs,
IVecInt result)
Translate an optimization function into constraints and provides the binary literals in results. |
IConstr[] |
GateTranslator.or(int y,
IVecInt literals)
translate y <=> x1 \/ x2 \/ ... \/ xn into clauses. |
ISolver |
DimacsArrayReader.parseInstance(int[] gateType,
int[] outputs,
int[][] inputs,
int maxVar)
|
void |
GateTranslator.xor(int x,
int a,
int b)
|
IConstr[] |
GateTranslator.xor(int y,
IVecInt literals)
translate y <=> x1 xor x2 xor ... xor xn into clauses. |
Uses of ContradictionException in org.sat4j.tools.xplain |
---|
Methods in org.sat4j.tools.xplain that throw ContradictionException | |
---|---|
IConstr |
Xplain.addAtLeast(IVecInt literals,
int degree)
|
IConstr |
Xplain.addAtMost(IVecInt literals,
int degree)
|
IConstr |
Xplain.addClause(IVecInt literals)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |