Uses of Class
org.sat4j.specs.ContradictionException

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.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.encoding
org.sat4j.tools.xplain	Implementation of an explanation engine in case of unsatisfiability.

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 soft clause 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.addSoftAtLeast(BigInteger weight, IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtLeast(int weight, IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtLeast(IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtMost(BigInteger weight, IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtMost(int weight, IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
IConstr	WeightedMaxSatDecorator.addSoftAtMost(IVecInt literals, int degree) Allow adding a new soft cardinality constraint in the solver.
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	MinCostDecorator.discard()
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	MixedDataStructureSingleWL.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	MixedDataStructureSingleWL.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.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 Constr	MaxWatchCard.maxWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Permet la cr?
static Constr	MinWatchCard.minWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Constructs a cardinality constraint with a minimal set of watched literals Permet la cr?
protected static int	AtLeast.niceParameters(UnitPropagationListener s, ILits voc, IVecInt ps, int deg)

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)
IConstr	Solver.addExactly(IVecInt literals, int n)
Constr	DataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree) Create a cardinality constraint of the form sum li >= degree.
Constr	DataStructureFactory.createClause(IVecInt literals)

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	PseudoBitsAdderDecorator.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	IPBSolver.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	UserFriendlyPBStringSolver.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolverDecorator.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	OPBStringSolver.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PseudoBitsAdderDecorator.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	IPBSolver.addAtLeast(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo-boolean constraint of the type "at least".
IConstr	UserFriendlyPBStringSolver.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	PBSolverDecorator.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	OPBStringSolver.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	UserFriendlyPBStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	OPBStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	PseudoBitsAdderDecorator.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	IPBSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree) Create a pseudo boolean constraint of the type "at most".
IConstr	UserFriendlyPBStringSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolverDecorator.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	OPBStringSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PseudoBitsAdderDecorator.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	IPBSolver.addAtMost(IVecInt literals, IVecInt coeffs, int degree) Create a pseudo boolean constraint of the type "at most".
IConstr	UserFriendlyPBStringSolver.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	PBSolverDecorator.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	OPBStringSolver.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	UserFriendlyPBStringSolver.addClause(IVecInt literals)
IConstr	OPBStringSolver.addClause(IVecInt literals)
IConstr	PseudoBitsAdderDecorator.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	IPBSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	UserFriendlyPBStringSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	PBSolverDecorator.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	OPBStringSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	PseudoBitsAdderDecorator.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	IPBSolver.addExactly(IVecInt literals, IVecInt coeffs, int weight) Create a pseudo-boolean constraint of the type "subset sum".
IConstr	UserFriendlyPBStringSolver.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	PBSolverDecorator.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	OPBStringSolver.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	PseudoBitsAdderDecorator.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	IPBSolver.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n or at most 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	ConstraintRelaxingPseudoOptDecorator.forceObjectiveValueTo(Number forcedValue)
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	AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
Constr	MinCardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	ICardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	AtLeastCardPBConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	MinCardPBConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	AtLeastCardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
protected Constr	AbstractPBClauseCardConstrDataStructure.constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MinLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	IPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	PuebloMinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractPBDataStructureFactory.createClause(IVecInt literals)
Constr	AbstractPBClauseCardConstrDataStructure.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 PBConstr	AtLeastPB.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
protected void	MaxWatchPb.computePropagation(UnitPropagationListener s)
protected void	MinWatchPbLong.computePropagation(UnitPropagationListener s)
protected void	MinWatchPbLongLimit.computePropagation(UnitPropagationListener s)
protected abstract void	WatchPbLongCP.computePropagation(UnitPropagationListener s)
protected abstract void	WatchPb.computePropagation(UnitPropagationListener s)
protected void	MaxWatchPbLongCP.computePropagation(UnitPropagationListener s)
protected void	MinWatchPb.computePropagation(UnitPropagationListener s)
protected abstract void	WatchPbLong.computePropagation(UnitPropagationListener s)
protected void	MinWatchPbLongCP.computePropagation(UnitPropagationListener s)
protected void	MaxWatchPbLong.computePropagation(UnitPropagationListener s)
protected void	MaxWatchPb.computeWatches() All the literals are watched.
protected void	MinWatchPbLong.computeWatches()
protected void	MinWatchPbLongLimit.computeWatches()
protected abstract void	WatchPbLongCP.computeWatches()
protected abstract void	WatchPb.computeWatches()
protected void	MaxWatchPbLongCP.computeWatches() All the literals are watched.
protected void	MinWatchPb.computeWatches()
protected abstract void	WatchPbLong.computeWatches()
protected void	MinWatchPbLongCP.computeWatches()
protected void	MaxWatchPbLong.computeWatches() All the literals are watched.
static PBConstr	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 MaxWatchPbLongCP	MaxWatchPbLongCP.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MaxWatchPbLong	MaxWatchPbLong.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static PBConstr	MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, int degree) Permet la cr?
static MinWatchPbLong	MinWatchPbLong.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MinWatchPbLongLimit	MinWatchPbLongLimit.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MinWatchPb	MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MinWatchPbLongCP	MinWatchPbLongCP.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.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolver.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	PBSolver.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	PBSolver.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	PBSolver.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	PBSolver.addExactly(IVecInt literals, IVecInt coeffs, int weight)
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	OPBReader2005.parseInstance(InputStream 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	ClausalConstraintsDecorator.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	XplainPB.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ManyCorePB.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	LexicoDecoratorPB.addAtLeast(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ClausalConstraintsDecorator.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	XplainPB.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	ManyCorePB.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	LexicoDecoratorPB.addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
IConstr	XplainPB.addAtMost(IVecInt literals, int degree)
IConstr	ClausalConstraintsDecorator.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	XplainPB.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ManyCorePB.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	LexicoDecoratorPB.addAtMost(IVecInt literals, IVec<BigInteger> coeffs, BigInteger degree)
IConstr	ClausalConstraintsDecorator.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	XplainPB.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	ManyCorePB.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	LexicoDecoratorPB.addAtMost(IVecInt literals, IVecInt coeffs, int degree)
IConstr	XplainPB.addExactly(IVecInt literals, int n)
IConstr	ClausalConstraintsDecorator.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	XplainPB.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	ManyCorePB.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	LexicoDecoratorPB.addExactly(IVecInt literals, IVec<BigInteger> coeffs, BigInteger weight)
IConstr	ClausalConstraintsDecorator.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	XplainPB.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	ManyCorePB.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	LexicoDecoratorPB.addExactly(IVecInt literals, IVecInt coeffs, int weight)
IConstr	ClausalConstraintsDecorator.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	XplainPB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	ManyCorePB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	LexicoDecoratorPB.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)
protected IConstr	LexicoDecoratorPB.discardSolutionsForOptimizing()
void	DependencyHelper.discardSolutionsWithObjectiveValueGreaterThan(long value)
protected void	LexicoDecoratorPB.fixCriterionValue()
void	DependencyHelper.halfOr(C name, T thing, T... otherThings) Create a constraint of the form thing <= (thing1 or thing 2 ... or thingn)
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

Methods in org.sat4j.reader that throw ContradictionException

protected void	DimacsReader.flushConstraint()
protected void	GroupedCNFReader.flushConstraint()
protected boolean	DimacsReader.handleLine()
protected boolean	GroupedCNFReader.handleLine()
IProblem	CSPReader.parseInstance(InputStream in)
IProblem	XMLCSPReader.parseInstance(InputStream in)
IProblem	InstanceReader.parseInstance(InputStream in)
IProblem	AAGReader.parseInstance(InputStream in)
IProblem	LecteurDimacs.parseInstance(InputStream input)
abstract IProblem	Reader.parseInstance(InputStream in) Read a file from a stream.
IProblem	AIGReader.parseInstance(InputStream in)
IProblem	DimacsReader.parseInstance(InputStream in)
IProblem	CSPReader.parseInstance(Reader in)
IProblem	CSPInstanceReader.parseInstance(Reader in)
IProblem	XMLCSPReader.parseInstance(Reader in)
IProblem	Reader.parseInstance(Reader in) Deprecated.
IProblem	CSPInstanceReader.parseInstance(String filename)
IProblem	XMLCSPReader.parseInstance(String filename)
IProblem	InstanceReader.parseInstance(String filename)
IProblem	Reader.parseInstance(String filename) This is the usual method to feed a solver with a benchmark.
protected void	DimacsReader.readConstrs()

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.
IConstr	ISolver.addExactly(IVecInt literals, int n) Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
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	AbstractOutputSolver.addAllClauses(IVec<IVecInt> clauses)
void	ManyCore.addAllClauses(IVec<IVecInt> clauses)
void	SolverDecorator.addAllClauses(IVec<IVecInt> clauses)
IConstr	ManyCore.addAtLeast(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtLeast(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	ManyCore.addAtMost(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtMost(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	AbstractOutputSolver.addBlockingClause(IVecInt literals)
IConstr	ManyCore.addBlockingClause(IVecInt literals)
IConstr	SolverDecorator.addBlockingClause(IVecInt literals)
IConstr	ManyCore.addClause(IVecInt literals)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	ManyCore.addExactly(IVecInt literals, int n)
IConstr	ClausalCardinalitiesDecorator.addExactly(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addExactly(IVecInt literals, int n)
IConstr	DimacsStringSolver.addExactly(IVecInt literals, int n)
IConstr	SolverDecorator.addExactly(IVecInt literals, int n)
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	LexicoDecorator.discard()
void	LexicoDecorator.discardCurrentSolution()
protected IConstr	LexicoDecorator.discardSolutionsForOptimizing()
protected void	LexicoDecorator.fixCriterionValue()
void	LexicoDecorator.forceObjectiveValueTo(Number forcedValue)
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)
IConstr[]	GateTranslator.halfOr(int y, IVecInt literals) translate y <= x1 \/ x2 \/ ... \/ xn into clauses.
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.encoding

Methods in org.sat4j.tools.encoding that throw ContradictionException

IConstr	EncodingStrategyAdapter.addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	EncodingStrategyAdapter.addAtLeastOne(ISolver solver, IVecInt literals)
IConstr	Sequential.addAtMost(ISolver solver, IVecInt literals, int k) This encoding adds (n-1)*k variables (n is the number of variables in the at most constraint and k is the degree of the constraint) and 2nk+n-3k-1 clauses.
IConstr	Policy.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	EncodingStrategyAdapter.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Commander.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
IConstr	Ladder.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Product.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Commander.addAtMostOne(ISolver solver, IVecInt literals) In this encoding, variables are partitioned in groups.
IConstr	Binary.addAtMostOne(ISolver solver, IVecInt literals) p being the smaller integer greater than log_2(n), this encoding adds p variables and n*p clauses.
IConstr	Binomial.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Policy.addExactly(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Ladder.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addExactlyOne(ISolver solver, IVecInt literals)

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	HighLevelXplain.addAtLeast(IVecInt literals, int degree)
IConstr	Xplain.addAtMost(IVecInt literals, int degree)
IConstr	HighLevelXplain.addAtMost(IVecInt literals, int degree)
IConstr	Xplain.addClause(IVecInt literals)
IConstr	HighLevelXplain.addClause(IVecInt literals, int desc)
IConstr	Xplain.addExactly(IVecInt literals, int n)