org.sat4j.minisat.constraints.pb
Class ConflictMap

java.lang.Object
  org.sat4j.minisat.constraints.pb.MapPb
      org.sat4j.minisat.constraints.pb.ConflictMap

All Implemented Interfaces:

IConflict, IDataStructurePB

public class ConflictMap
extends MapPb
implements IConflict

Author:

parrain TODO To change the template for this generated type comment go to Window - Preferences - Java - Code Style - Code Templates

Method Summary

static IConflict	createConflict(PBConstr cpb)
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 class org.sat4j.minisat.constraints.pb.MapPb

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

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

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

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

Method Detail

createConflict

public static IConflict createConflict(PBConstr cpb)

resolve

public java.math.BigInteger resolve(PBConstr cpb,
                                    int litImplied)

Effectue une resolution avec une contrainte PB. Met a jour le Conflict.

Specified by:

resolve in interface IConflict

Parameters:

cpb - contrainte avec laquelle on va faire la resolution

litImplied - litteral devant etre resolu

Returns:

la mise a jour du degre

slackConflict

public java.math.BigInteger slackConflict()

Specified by:

slackConflict in interface IConflict

isAssertive

public boolean isAssertive(int dl)

Specified by:

isAssertive in interface IConflict

reduceInConstraint

public 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.

Specified by:

reduceInConstraint in interface IConflict

Returns:

mise a jour du degre

getBacktrackLevel

public int getBacktrackLevel(int maxLevel)

retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut pour lequel la contrainte est assertive

Specified by:

getBacktrackLevel in interface IConflict

Parameters:

maxLevel - le plus bas niveau pour lequel la contrainte est assertive

Returns:

the highest level (smaller int) for which the constraint is assertive.