Uses of Interface
org.sat4j.minisat.core.UnitPropagationListener

Packages that use UnitPropagationListener
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. 
 

Uses of UnitPropagationListener in org.sat4j.minisat.constraints
 

Fields in org.sat4j.minisat.constraints declared as UnitPropagationListener
protected  UnitPropagationListener AbstractDataStructureFactory.solver
           
 

Methods in org.sat4j.minisat.constraints with parameters of type UnitPropagationListener
 void AbstractDataStructureFactory.setUnitPropagationListener(UnitPropagationListener s)
           
 

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

Methods in org.sat4j.minisat.constraints.card with parameters of type UnitPropagationListener
 void MaxWatchCard.assertConstraint(UnitPropagationListener s)
           
 void AtLeast.assertConstraint(UnitPropagationListener s)
           
 void MinWatchCard.assertConstraint(UnitPropagationListener s)
           
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)
           
 boolean MaxWatchCard.propagate(UnitPropagationListener s, int p)
          Propagation de la valeur de v?rit? d'un litt?ral falsifi?
 boolean AtLeast.propagate(UnitPropagationListener s, int p)
           
 boolean MinWatchCard.propagate(UnitPropagationListener s, int p)
          propagates the value of a falsified literal
 void MaxWatchCard.remove(UnitPropagationListener upl)
           
 void AtLeast.remove(UnitPropagationListener upl)
           
 void MinWatchCard.remove(UnitPropagationListener upl)
          Removes a constraint from the solver
 

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

Methods in org.sat4j.minisat.constraints.cnf with parameters of type UnitPropagationListener
 void HTClause.assertConstraint(UnitPropagationListener s)
           
 void BinaryClause.assertConstraint(UnitPropagationListener s)
           
 void WLClause.assertConstraint(UnitPropagationListener s)
           
 void CBClause.assertConstraint(UnitPropagationListener s)
           
 void UnitClauses.assertConstraint(UnitPropagationListener s)
           
 void UnitClause.assertConstraint(UnitPropagationListener s)
           
static OriginalWLClause OriginalWLClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
static CBClause CBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
           
static CBClause MixableCBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
           
static OriginalBinaryClause OriginalBinaryClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
static OriginalHTClause OriginalHTClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
 boolean HTClause.propagate(UnitPropagationListener s, int p)
           
 boolean BinaryClause.propagate(UnitPropagationListener s, int p)
           
 boolean WLClause.propagate(UnitPropagationListener s, int p)
           
 boolean CBClause.propagate(UnitPropagationListener s, int p)
           
 boolean UnitClauses.propagate(UnitPropagationListener s, int p)
           
 boolean MixableCBClause.propagate(UnitPropagationListener s, int p)
           
 boolean UnitClause.propagate(UnitPropagationListener s, int p)
           
 void HTClause.remove(UnitPropagationListener upl)
           
 void BinaryClause.remove(UnitPropagationListener upl)
           
 void WLClause.remove(UnitPropagationListener upl)
           
 void CBClause.remove(UnitPropagationListener upl)
           
 void UnitClauses.remove(UnitPropagationListener upl)
           
 void UnitClause.remove(UnitPropagationListener upl)
           
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 UnitPropagationListener in org.sat4j.minisat.core
 

Classes in org.sat4j.minisat.core that implement UnitPropagationListener
 class Solver<D extends DataStructureFactory>
          The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.
 

Methods in org.sat4j.minisat.core with parameters of type UnitPropagationListener
 void Constr.assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
 boolean Propagatable.propagate(UnitPropagationListener s, int p)
          Propagate the truth value of a literal in constraints in which that literal is falsified.
 void Constr.remove(UnitPropagationListener upl)
          Remove a constraint from the solver.
 void DataStructureFactory.setUnitPropagationListener(UnitPropagationListener s)
           
 



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