org.sat4j.minisat.constraints.pb
Interface IConflict

All Superinterfaces:

IDataStructurePB

All Known Implementing Classes:

ConflictArrayCard, ConflictArrayClause, ConflictMap

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) Effectue une resolution avec une contrainte PB.
java.math.BigInteger	slackConflict()

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)

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

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.