org.sat4j.pb.constraints.pb
Interface IConflict

All Superinterfaces:
IDataStructurePB
All Known Implementing Classes:
ConflictMap, ConflictMapCardinality, ConflictMapClause, ConflictMapMerging, ConflictMapSwitchToClause

public interface IConflict
extends IDataStructurePB


Method Summary
 int getBacktrackLevel(int maxLevel)
          retourne le niveau de backtrack : c'est-?
 boolean isAssertive(int dl)
           
 BigInteger reduceInConstraint(IWatchPb wpb, BigInteger[] coefsBis, int indLitImplied, BigInteger degreeBis)
          Reduction d'une contrainte On supprime un litteral non assigne prioritairement, vrai sinon.
 BigInteger resolve(PBConstr cpb, int litImplied, VarActivityListener val)
          Effectue une resolution avec une contrainte PB.
 BigInteger slackConflict()
           
 boolean slackIsCorrect(int decisionLevel)
           
 void updateSlack(int level)
           
 
Methods inherited from interface org.sat4j.pb.constraints.pb.IDataStructurePB
buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getAssertiveLiteral, getDegree, isCardinality, isLongSufficient, saturation, size
 

Method Detail

resolve

BigInteger resolve(PBConstr cpb,
                   int litImplied,
                   VarActivityListener val)
Effectue une resolution avec une contrainte PB. Met a jour le Conflict.

Parameters:
cpb - contrainte avec laquelle on va faire la resolution
litImplied - litteral devant etre resolu
val - TODO
Returns:
la mise a jour du degre

slackConflict

BigInteger slackConflict()

isAssertive

boolean isAssertive(int dl)

reduceInConstraint

BigInteger reduceInConstraint(IWatchPb wpb,
                              BigInteger[] coefsBis,
                              int indLitImplied,
                              BigInteger degreeBis)
Reduction d'une contrainte On supprime un litteral non assigne prioritairement, vrai sinon. En aucun cas on ne supprime litImplied.

Returns:
mise a jour du degre

getBacktrackLevel

int getBacktrackLevel(int maxLevel)
retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut pour lequel la contrainte est assertive

Parameters:
maxLevel - le plus bas niveau pour lequel la contrainte est assertive
Returns:
the highest level (smaller int) for which the constraint is assertive.

updateSlack

void updateSlack(int level)

slackIsCorrect

boolean slackIsCorrect(int decisionLevel)


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