Uses of Interface
org.sat4j.specs.IConstr

Packages that use IConstr
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.minisat.uip Various ways to compute an asserting clause (containing one Unique Implication Point). 
org.sat4j.opt Built-in optimization framework. 
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 IConstr in org.sat4j.minisat.constraints
 

Methods in org.sat4j.minisat.constraints that return IConstr
 IConstr AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
           
 

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

Classes in org.sat4j.minisat.constraints.card that implement IConstr
 class AtLeast
           
 class MaxWatchCard
           
 class MinWatchCard
           
 

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

Classes in org.sat4j.minisat.constraints.cnf that implement IConstr
 class BinaryClauses
           
 class CBClause
           
 class DefaultWLClause
           
 class LearntWLClause
           
 class MixableCBClause
          Counter Based clauses that can be mixed with WLCLauses
 class OriginalWLClause
           
 class TernaryClauses
           
 class WLClause
          Lazy data structure for clause using Watched Literals.
 

Uses of IConstr in org.sat4j.minisat.constraints.pb
 

Subinterfaces of IConstr in org.sat4j.minisat.constraints.pb
 interface PBConstr
           
 

Classes in org.sat4j.minisat.constraints.pb that implement IConstr
 class AtLeastPB
           
 class MaxWatchPb
           
 class MinWatchCardPB
           
 class MinWatchPb
           
 class MixableCBClausePB
           
 class PuebloMinWatchPb
           
 class WatchPb
           
 class WLClausePB
           
 

Methods in org.sat4j.minisat.constraints.pb that return IConstr
 IConstr PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
           
 IConstr IInternalPBConstraintCreator.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
           
 

Uses of IConstr in org.sat4j.minisat.core
 

Subinterfaces of IConstr in org.sat4j.minisat.core
 interface Constr
          Basic constraint abstraction used in Solver.
 

Methods in org.sat4j.minisat.core that return IConstr
 IConstr Solver.addAtLeast(IVecInt literals, int degree)
           
 IConstr Solver.addAtMost(IVecInt literals, int degree)
           
 IConstr Solver.addClause(IVecInt literals)
           
protected  IConstr Solver.addConstr(Constr constr)
           
 IConstr Solver.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
           
 IConstr Solver.getIthConstr(int i)
          returns the ith constraint in the solver.
 

Methods in org.sat4j.minisat.core with parameters of type IConstr
 boolean AssertingClauseGenerator.clauseNonAssertive(IConstr reason)
          method indicating if an asserting clause has been built. note that this method is called right after a resolution step is finished.
 boolean Solver.removeConstr(IConstr co)
           
 

Uses of IConstr in org.sat4j.minisat.uip
 

Methods in org.sat4j.minisat.uip with parameters of type IConstr
 boolean FirstUIP.clauseNonAssertive(IConstr reason)
           
 boolean DecisionUIP.clauseNonAssertive(IConstr reason)
           
 

Uses of IConstr in org.sat4j.opt
 

Methods in org.sat4j.opt that return IConstr
 IConstr MaxSatDecorator.addClause(IVecInt literals)
           
 IConstr WeightedMaxSatDecorator.addClause(IVecInt literals)
           
 

Uses of IConstr in org.sat4j.specs
 

Methods in org.sat4j.specs that return IConstr
 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"
 

Methods in org.sat4j.specs with parameters of type IConstr
 boolean ISolver.removeConstr(IConstr c)
          Remove a constraint returned by one of the add method from the solver.
 

Uses of IConstr in org.sat4j.tools
 

Methods in org.sat4j.tools that return IConstr
 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)
           
 

Methods in org.sat4j.tools with parameters of type IConstr
 boolean DimacsOutputSolver.removeConstr(IConstr c)
           
 boolean SolverDecorator.removeConstr(IConstr c)
           
 



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