Uses of Class
org.sat4j.specs.ContradictionException

Packages that use ContradictionException

org.sat4j	Contains a command line launcher for the SAT solvers.
org.sat4j.minisat.constraints	Implementations of various constraints for MiniSAT.
org.sat4j.minisat.constraints.card	Implementations of cardinality constraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal 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.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

Methods in org.sat4j that throw ContradictionException

protected IProblem

AbstractLauncher.readProblem(java.lang.String problemname) Reads a problem file from the command line.

Uses of ContradictionException in org.sat4j.minisat.constraints

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

Constr	MixedDataStructureDaniel.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielCBHT.createClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createClause(IVecInt literals)
Constr	ClausalDataStructureHT.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createClause(IVecInt literals)
Constr	ClausalDataStructureCBHT.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createClause(IVecInt literals)
Constr	ClausalDataStructureCB.createClause(IVecInt literals)

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)
protected MinWatchCard	MinWatchCard.computePropagation(UnitPropagationListener s)
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?
static int	Cards.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.addClause(IVecInt literals)
Constr	DataStructureFactory.createCardinalityConstraint(IVecInt literals, int 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	MinOneDecorator.discard()
void	MaxSatDecorator.discard()

Uses of ContradictionException in org.sat4j.reader

Methods in org.sat4j.reader that throw ContradictionException

protected boolean	ExtendedDimacsReader.handleConstr(java.lang.String line, IVecInt literals)
protected boolean	DimacsReader.handleConstr(java.lang.String line, IVecInt literals)
IProblem	LecteurDimacs.parseInstance(java.io.InputStream input)
IProblem	Reader.parseInstance(java.io.InputStream in)
IProblem	AIGReader.parseInstance(java.io.InputStream in)
IProblem	AAGReader.parseInstance(java.io.Reader in)
IProblem	InstanceReader.parseInstance(java.io.Reader in)
IProblem	DimacsReader.parseInstance(java.io.Reader in)
IProblem	LecteurDimacs.parseInstance(java.io.Reader input)
abstract IProblem	Reader.parseInstance(java.io.Reader in)
IProblem	AIGReader.parseInstance(java.io.Reader in)
IProblem	InstanceReader.parseInstance(java.lang.String filename)
IProblem	Reader.parseInstance(java.lang.String filename)
protected void	CardDimacsReader.readConstrs(java.io.LineNumberReader in) Deprecated.
protected void	DimacsReader.readConstrs(java.io.LineNumberReader in)

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.
void	IOptimizationProblem.discard() Discard the current solution in the optimization problem.

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)
void	DimacsStringSolver.addAllClauses(IVec<IVecInt> clauses)
IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)
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.
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).
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.
ISolver	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.