Uses of Class
org.sat4j.specs.ContradictionException

Packages that use ContradictionException

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.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.opt	Built-in optimization framework.
org.sat4j.reader	Some utility classes to read problems from plain text files.
org.sat4j.reader.csp	Classes needed for CSP to SAT translation.
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.

Uses of ContradictionException in org.sat4j.minisat.constraints

Methods in org.sat4j.minisat.constraints that throw ContradictionException

Constr	CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDaniel.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createClause(IVecInt literals)
Constr	MixedDataStructureDanielCBWL.createClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createClause(IVecInt literals)
Constr	ClausalDataStructureCB.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createClause(IVecInt literals)
Constr	AbstractCardinalityDataStructure.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	AbstractDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
IConstr	AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)

Uses of ContradictionException in org.sat4j.minisat.constraints.card

Methods in org.sat4j.minisat.constraints.card that throw ContradictionException

static AtLeast	AtLeast.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
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?

Uses of ContradictionException in org.sat4j.minisat.constraints.cnf

Methods in org.sat4j.minisat.constraints.cnf that throw ContradictionException

static IVecInt

WLClause.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.constraints.pb

Methods in org.sat4j.minisat.constraints.pb that throw ContradictionException

IConstr	PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
static AtLeastPB	AtLeastPB.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
static MaxWatchPb	MaxWatchPb.maxWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
static MaxWatchPb	MaxWatchPb.maxWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
static MinWatchCardPB	MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Permet la cr?
static PuebloMinWatchPb	PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)
static PuebloMinWatchPb	PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
static MinWatchPb	MinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
static PuebloMinWatchPb	PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
static MinWatchPb	MinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
static IDataStructurePB	WatchPb.niceParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)
static MaxWatchPb	MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)
static MaxWatchPb	MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)
static MinWatchCardPB	MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, int degree) Permet la cr?
static MinWatchPb	MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)
static MinWatchPb	MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)

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.addClause(IVecInt literals)
IConstr	Solver.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
Constr	DataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	DataStructureFactory.createClause(IVecInt literals)
Constr	DataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)

Uses of ContradictionException in org.sat4j.opt

Methods in org.sat4j.opt that throw ContradictionException

IConstr	WeightedMaxSatDecorator.addClause(IVecInt literals)
IConstr	MaxSatDecorator.addClause(IVecInt literals)
void	WeightedMaxSatDecorator.discard()
void	MaxSatDecorator.discard()
void	PseudoOptDecorator.discard()
void	MinOneDecorator.discard()
void	MinCostDecorator.discard()

Uses of ContradictionException in org.sat4j.reader

Methods in org.sat4j.reader that throw ContradictionException

void	OPBReader2005.parse() parses the file and uses the callbacks to send to send the data back to the program
IProblem	LecteurDimacs.parseInstance(java.io.InputStream in)
IProblem	AIGReader.parseInstance(java.io.InputStream in)
IProblem	Reader.parseInstance(java.io.InputStream in)
IProblem	OPBReader2005.parseInstance(java.io.Reader in)
IProblem	XMLCSPReader.parseInstance(java.io.Reader in)
IProblem	LecteurDimacs.parseInstance(java.io.Reader in)
IProblem	InstanceReader.parseInstance(java.io.Reader in)
IProblem	GoodOPBReader.parseInstance(java.io.Reader in)
IProblem	DimacsReader.parseInstance(java.io.Reader in)
IProblem	CSPReader.parseInstance(java.io.Reader in)
IProblem	AIGReader.parseInstance(java.io.Reader in)
IProblem	AAGReader.parseInstance(java.io.Reader in)
abstract IProblem	Reader.parseInstance(java.io.Reader in)
IProblem	XMLCSPReader.parseInstance(java.lang.String filename)
IProblem	InstanceReader.parseInstance(java.lang.String filename)
IProblem	Reader.parseInstance(java.lang.String filename)

Uses of ContradictionException in org.sat4j.reader.csp

Methods in org.sat4j.reader.csp that throw ContradictionException

void	GeneralizedSupportEncoding.onFinish(ISolver solver, IVec<Var> scope)
void	BinarySupportEncoding.onFinish(ISolver solver, IVec<Var> scope)
void	Encoding.onFinish(ISolver solver, IVec<Var> scope)
void	GeneralizedSupportEncoding.onNogood(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	DirectEncoding.onNogood(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	BinarySupportEncoding.onNogood(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	Encoding.onNogood(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	GeneralizedSupportEncoding.onSupport(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	BinarySupportEncoding.onSupport(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
void	Encoding.onSupport(ISolver solver, IVec<Var> scope, java.util.Map<Evaluable,java.lang.Integer> tuple)
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	Var.toClause(ISolver solver)
void	Nogoods.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
void	Supports.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
void	AllDiff.toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
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.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.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.addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
void	IOptimizationProblem.discard()

Uses of ContradictionException in org.sat4j.tools

Methods in org.sat4j.tools that throw ContradictionException

void	DimacsOutputSolver.addAllClauses(IVec<IVecInt> clauses)
void	SolverDecorator.addAllClauses(IVec<IVecInt> clauses)
IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	DimacsOutputSolver.addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d)
IConstr	SolverDecorator.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
void	GateTranslator.and(int y, int x1, int x2) Translate y <=> x1 /\ x2
void	GateTranslator.and(int y, IVecInt literals) Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
void	GateTranslator.gateFalse(int y) translate y <=> FALSE into a clause.
void	GateTranslator.gateTrue(int y) translate y <=> TRUE into a clause.
void	GateTranslator.iff(int y, IVecInt literals) translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
void	GateTranslator.ite(int y, int x1, int x2, int x3) translate y <=> if x1 then x2 else x3 into clauses.
void	GateTranslator.not(int y, int x) Translate y <=> not x into clauses.
void	GateTranslator.or(int y, IVecInt literals) translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
java.lang.String	DimacsArrayToDimacsConverter.parseInstance(int[] gateType, int[] outputs, int[][] inputs, int maxVar)
IProblem	DimacsArrayReader.parseInstance(int[] gateType, int[] outputs, int[][] inputs, int maxVar)
void	GateTranslator.xor(int y, IVecInt literals) translate y <=> x1 xor x2 xor ... xor xn into clauses.