org.sat4j.minisat.constraints.cnf
Class MixableCBClause

java.lang.Object
  org.sat4j.minisat.constraints.cnf.CBClause
      org.sat4j.minisat.constraints.cnf.MixableCBClause

All Implemented Interfaces:

Serializable, Constr, Propagatable, Undoable, IConstr

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, forwardActivity, 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)