org.sat4j.minisat.constraints.pb
Class ConflictArrayClause

java.lang.Object
  org.sat4j.minisat.constraints.pb.ArrayPb
      org.sat4j.minisat.constraints.pb.ConflictArrayClause

All Implemented Interfaces:

IConflict, IDataStructurePB

public class ConflictArrayClause
extends ArrayPb

Field Summary

boolean

affiche

Constructor Summary

ConflictArrayClause(int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger d, ILits voc)

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

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

Field Detail

affiche

public boolean affiche

Constructor Detail

ConflictArrayClause

public ConflictArrayClause(int[] lits,
                           java.math.BigInteger[] coefs,
                           java.math.BigInteger d,
                           ILits voc)

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.