View Javadoc

1   package org.sat4j.minisat.constraints.pb;
2   
3   import java.math.BigInteger;
4   import java.util.HashMap;
5   import java.util.Map;
6   
7   import org.sat4j.minisat.core.ILits;
8   
9   public class ConflictMapMerging extends ConflictMap {
10  
11  	public ConflictMapMerging(Map<Integer, BigInteger> m, BigInteger d, ILits voc,
12  			int level) {
13  		super(m, d, voc, level);
14  	}
15      public static IConflict createConflict(PBConstr cpb, int level) {
16          Map<Integer, BigInteger> m = new HashMap<Integer, BigInteger>();
17          int lit;
18          BigInteger coefLit;
19          for (int i = 0; i < cpb.size(); i++) {
20              lit = cpb.get(i);
21              coefLit = cpb.getCoef(i);
22              assert cpb.get(i) != 0;
23              assert cpb.getCoef(i).signum() > 0;
24              m.put(lit, coefLit);
25          }
26          return new ConflictMapMerging(m, cpb.getDegree(), cpb.getVocabulary(),
27                  level);
28      }
29  
30      /**
31       * reduces the constraint defined by wpb until the result of the cutting
32       * plane is a conflict. this reduction returns a PB constraint.
33       * 
34       * @param litImplied
35       * @param ind
36       * @param reducedCoefs
37       * @param wpb
38       * @return the degree of the constraint
39       */
40      @Override
41      protected BigInteger reduceUntilConflict(int litImplied, int ind,
42              BigInteger[] reducedCoefs, WatchPb wpb) {
43      	BigInteger tmp = reducedCoefs[ind].subtract(BigInteger.ONE);
44          reducedCoefs[ind] = BigInteger.ONE;
45          coefMultCons = coefs.get(litImplied ^ 1);
46          coefMult = BigInteger.ONE;
47          return saturation(reducedCoefs,wpb.getDegree().subtract(tmp));
48      }
49  
50  	
51  	
52  }