org.sat4j.minisat.constraints.pb
Interface IConflict

All Superinterfaces:

IDataStructurePB

All Known Implementing Classes:

ConflictMap, ConflictMapCardinality, ConflictMapClause, ConflictMapMerging

public interface IConflict
extends IDataStructurePB

Method Summary

int	getBacktrackLevel(int maxLevel) retourne le niveau de backtrack : c'est-?
boolean	isAssertive(int dl)
java.math.BigInteger	reduceInConstraint(WatchPb wpb, java.math.BigInteger[] coefsBis, int indLitImplied, java.math.BigInteger degreeBis) Reduction d'une contrainte On supprime un litteral non assigne prioritairement, vrai sinon.
java.math.BigInteger	resolve(PBConstr cpb, int litImplied, VarActivityListener val) Effectue une resolution avec une contrainte PB.
java.math.BigInteger	slackConflict()
boolean	slackIsCorrect(int decisionLevel)
void	updateSlack(int level)

Methods inherited from interface org.sat4j.minisat.constraints.pb.IDataStructurePB

buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getDegree, saturation, size

Method Detail

resolve

java.math.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

java.math.BigInteger slackConflict()

isAssertive

boolean isAssertive(int dl)

reduceInConstraint

java.math.BigInteger reduceInConstraint(WatchPb wpb,
                                        java.math.BigInteger[] coefsBis,
                                        int indLitImplied,
                                        java.math.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)