org.sat4j.minisat.constraints.cnf
Class MixableCBClause

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.CBClause
      extended by org.sat4j.minisat.constraints.cnf.MixableCBClause
All Implemented Interfaces:
java.io.Serializable, Constr, Propagatable, Undoable, IConstr
Direct Known Subclasses:
MixableCBClausePB

public class MixableCBClause
extends CBClause

Counter Based clauses that can be mixed with WLCLauses

Author:
leberre
See Also:
Serialized Form

Field Summary
 
Fields inherited from class org.sat4j.minisat.constraints.cnf.CBClause
falsified, lits, voc
 
Constructor Summary
MixableCBClause(IVecInt ps, ILits voc)
           
MixableCBClause(IVecInt ps, ILits voc, boolean learnt)
           
 
Method Summary
static CBClause brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
           
 boolean propagate(UnitPropagationListener s, int p)
          Propagate the truth value of a literal in constraints in which that literal is falsified.
 
Methods inherited from class org.sat4j.minisat.constraints.cnf.CBClause
assertConstraint, calcReason, get, getActivity, incActivity, learnt, locked, register, remove, rescaleBy, setLearnt, simplify, size, toString, undo
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Constructor Detail

MixableCBClause

public MixableCBClause(IVecInt ps,
                       ILits voc)
Parameters:
ps -
voc -

MixableCBClause

public MixableCBClause(IVecInt ps,
                       ILits voc,
                       boolean learnt)
Parameters:
ps -
voc -
learnt -
Method Detail

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)
Description copied from interface: Propagatable
Propagate the truth value of a literal in constraints in which that literal is falsified.

Specified by:
propagate in interface Propagatable
Overrides:
propagate in class CBClause
Parameters:
s - something able to perform unit propagation
p - the literal being propagated. Its negation must appear in the constraint.
Returns:
false iff an inconsistency (a contradiction) is detected.

brandNewClause

public static CBClause brandNewClause(UnitPropagationListener s,
                                      ILits voc,
                                      IVecInt literals)


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