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 constraints.
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 intended for users dealing with SAT solvers as black boxes.
org.sat4j.tools	Tools to be used on top of an ISolver.
org.sat4j.tools.encoding	Implementation of different encodings.
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.minisat.constraints

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

Constr	MixedDataStructureSingleWL.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureSingleWL.createClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	CardinalityDataStructure.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	MinOneDecorator.discard()
void	MaxSatDecorator.discard()
void	MinOneDecorator.discardCurrentSolution()
void	MaxSatDecorator.discardCurrentSolution()
void	MinOneDecorator.forceObjectiveValueTo(Number forcedValue)
void	MaxSatDecorator.forceObjectiveValueTo(Number forcedValue)

Uses of ContradictionException in org.sat4j.reader

Methods in org.sat4j.reader that throw ContradictionException

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

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	SolverDecorator.addAllClauses(IVec<IVecInt> clauses)
void	ManyCore.addAllClauses(IVec<IVecInt> clauses)
void	AbstractOutputSolver.addAllClauses(IVec<IVecInt> clauses)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	ManyCore.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtLeast(IVecInt literals, int k)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	ManyCore.addAtMost(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtMost(IVecInt literals, int k)
IConstr	SolverDecorator.addBlockingClause(IVecInt literals)
IConstr	ManyCore.addBlockingClause(IVecInt literals)
IConstr	AbstractOutputSolver.addBlockingClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	ManyCore.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addExactly(IVecInt literals, int n)
IConstr	ManyCore.addExactly(IVecInt literals, int n)
IConstr	DimacsStringSolver.addExactly(IVecInt literals, int n)
IConstr	DimacsOutputSolver.addExactly(IVecInt literals, int n)
IConstr	ClausalCardinalitiesDecorator.addExactly(IVecInt literals, int k)
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	ExtendedDimacsArrayReader.handleConstr(int gateType, int output, int[] inputs) Handles a single constraint (constraint == Extended Dimacs circuit gate).
protected boolean	DimacsArrayReader.handleConstr(int gateType, int output, int[] inputs)
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	Product.addAtLeast(ISolver solver, IVecInt literals, int k)
IConstr	Policy.addAtLeast(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	Commander.addAtLeast(ISolver solver, IVecInt literals, int k)
IConstr	Binomial.addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addAtLeast(ISolver solver, IVecInt literals, int k)
IConstr	EncodingStrategyAdapter.addAtLeastOne(ISolver solver, IVecInt literals)
IConstr	Binomial.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	Product.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Policy.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	EncodingStrategyAdapter.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Commander.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Product.addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
IConstr	Product.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Commander.addAtMostOne(ISolver solver, IVecInt literals) In this encoding, variables are partitioned in groups.
IConstr	Binomial.addAtMostOne(ISolver solver, IVecInt literals)
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	Product.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Policy.addExactly(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Commander.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Commander.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binomial.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binary.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)