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 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. 
org.sat4j.tools.xplain   
 

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 AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
           
 Constr ClausalDataStructureCB.createClause(IVecInt literals)
           
 Constr CardinalityDataStructureYanMin.createClause(IVecInt literals)
           
 Constr ClausalDataStructureCBWL.createClause(IVecInt literals)
           
 Constr ClausalDataStructureWL.createClause(IVecInt literals)
           
 Constr MixedDataStructureDanielHT.createClause(IVecInt literals)
           
 Constr CardinalityDataStructure.createClause(IVecInt literals)
           
 Constr MixedDataStructureDanielCBWL.createClause(IVecInt literals)
           
 Constr MixedDataStructureDanielWL.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 MaxWatchCard MaxWatchCard.maxWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree)
          Permet la cr?ation de contrainte de cardinalit? ? observation minimale
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?ation de contrainte de cardinalit? ? observation minimale
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)
           
 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()
           
 void MinOneDecorator.discardCurrentSolution()
           
 void MaxSatDecorator.discardCurrentSolution()
           
 void MinOneDecorator.forceObjectiveValueTo(java.lang.Number forcedValue)
           
 void MaxSatDecorator.forceObjectiveValueTo(java.lang.Number forcedValue)
           
 

Uses of ContradictionException in org.sat4j.reader
 

Methods in org.sat4j.reader that throw ContradictionException
protected  void DimacsReader.flushConstraint()
           
protected  boolean DimacsReader.handleLine()
           
 IProblem Reader.parseInstance(java.io.InputStream in)
           
 IProblem AAGReader.parseInstance(java.io.InputStream in)
           
 IProblem AIGReader.parseInstance(java.io.InputStream in)
           
 IProblem LecteurDimacs.parseInstance(java.io.InputStream input)
           
 IProblem DimacsReader.parseInstance(java.io.InputStream in)
           
abstract  IProblem Reader.parseInstance(java.io.Reader in)
           
 IProblem AAGReader.parseInstance(java.io.Reader in)
           
 IProblem InstanceReader.parseInstance(java.io.Reader in)
           
 IProblem AIGReader.parseInstance(java.io.Reader in)
           
 IProblem LecteurDimacs.parseInstance(java.io.Reader input)
           
 IProblem DimacsReader.parseInstance(java.io.Reader in)
           
 IProblem Reader.parseInstance(java.lang.String filename)
           
 IProblem InstanceReader.parseInstance(java.lang.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.
 void IOptimizationProblem.discard()
          Deprecated. 
 void IOptimizationProblem.discardCurrentSolution()
          Discard the current solution in the optimization problem.
 void IOptimizationProblem.forceObjectiveValueTo(java.lang.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 DimacsOutputSolver.addAllClauses(IVec<IVecInt> clauses)
           
 void DimacsStringSolver.addAllClauses(IVec<IVecInt> clauses)
           
 IConstr SolverDecorator.addAtLeast(IVecInt literals, int degree)
           
 IConstr DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
           
 IConstr DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
           
 IConstr SolverDecorator.addAtMost(IVecInt literals, int degree)
           
 IConstr DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
           
 IConstr DimacsStringSolver.addAtMost(IVecInt literals, int degree)
           
 IConstr SolverDecorator.addBlockingClause(IVecInt literals)
           
 IConstr DimacsOutputSolver.addBlockingClause(IVecInt literals)
           
 IConstr DimacsStringSolver.addBlockingClause(IVecInt literals)
           
 IConstr SolverDecorator.addClause(IVecInt literals)
           
 IConstr DimacsOutputSolver.addClause(IVecInt literals)
           
 IConstr DimacsStringSolver.addClause(IVecInt literals)
           
 IConstr[] GateTranslator.and(int y, int x1, int x2)
          Translate y <=> x1 /\ x2
 IConstr[] GateTranslator.and(int y, IVecInt literals)
          Translate y <=> x1 /\ x2 /\ ...
 IConstr GateTranslator.gateFalse(int y)
          translate y <=> FALSE into a clause.
 IConstr 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).
 IConstr[] GateTranslator.iff(int y, IVecInt literals)
          translate y <=> (x1 <=> x2 <=> ...
 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.
 IConstr[] GateTranslator.or(int y, IVecInt literals)
          translate y <=> x1 \/ x2 \/ ...
 ISolver DimacsArrayReader.parseInstance(int[] gateType, int[] outputs, int[][] inputs, int maxVar)
           
 IConstr[] GateTranslator.xor(int y, IVecInt literals)
          translate y <=> x1 xor x2 xor ...
 

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



Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.