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.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.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 CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr MixedDataStructureDaniel.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr CardinalityDataStructure.createClause(IVecInt literals)
           
 Constr CardinalityDataStructureYanMax.createClause(IVecInt literals)
           
 Constr CardinalityDataStructureYanMin.createClause(IVecInt literals)
           
 Constr ClausalDataStructureCB.createClause(IVecInt literals)
           
 Constr ClausalDataStructureCBWL.createClause(IVecInt literals)
           
 Constr ClausalDataStructureWL.createClause(IVecInt literals)
           
 Constr MixedDataStructureDaniel.createClause(IVecInt literals)
           
 Constr MixedDataStructureDanielCBWL.createClause(IVecInt literals)
           
 Constr MixedDataStructureWithBinary.createClause(IVecInt literals)
           
 Constr MixedDataStructureWithBinaryAndTernary.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)
           
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.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 MaxSatDecorator.discard()
           
 void MinOneDecorator.discard()
           
 

Uses of ContradictionException in org.sat4j.reader
 

Methods in org.sat4j.reader that throw ContradictionException
 IProblem AIGReader.parseInstance(java.io.InputStream in)
           
 IProblem LecteurDimacs.parseInstance(java.io.InputStream in)
           
 IProblem Reader.parseInstance(java.io.InputStream in)
           
 IProblem AAGReader.parseInstance(java.io.Reader in)
           
 IProblem AIGReader.parseInstance(java.io.Reader in)
           
 IProblem DimacsReader.parseInstance(java.io.Reader in)
           
 IProblem InstanceReader.parseInstance(java.io.Reader in)
           
 IProblem LecteurDimacs.parseInstance(java.io.Reader in)
           
abstract  IProblem Reader.parseInstance(java.io.Reader in)
           
 IProblem InstanceReader.parseInstance(java.lang.String filename)
           
 IProblem Reader.parseInstance(java.lang.String filename)
           
 

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 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.addClause(IVecInt literals)
           
 IConstr DimacsStringSolver.addClause(IVecInt literals)
           
 IConstr SolverDecorator.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.
 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.