| 1 |  |  | 
        
| 2 |  |  | 
        
| 3 |  |  | 
        
| 4 |  |  | 
        
| 5 |  |  | 
        
| 6 |  |  | 
        
| 7 |  |  | 
        
| 8 |  |  | 
        
| 9 |  |  | 
        
| 10 |  |  | 
        
| 11 |  |  | 
        
| 12 |  |  | 
        
| 13 |  |  | 
        
| 14 |  |  | 
        
| 15 |  |  | 
        
| 16 |  |  | 
        
| 17 |  |  | 
        
| 18 |  |  | 
        
| 19 |  |  | 
        
| 20 |  |  | 
        
| 21 |  |  | 
        
| 22 |  |  | 
        
| 23 |  |  | 
        
| 24 |  |  | 
        
| 25 |  |  | 
        
| 26 |  | package org.sat4j.opt; | 
        
| 27 |  |  | 
        
| 28 |  | import java.math.BigInteger; | 
        
| 29 |  |  | 
        
| 30 |  | import org.sat4j.core.Vec; | 
        
| 31 |  | import org.sat4j.core.VecInt; | 
        
| 32 |  | import org.sat4j.specs.ContradictionException; | 
        
| 33 |  | import org.sat4j.specs.IConstr; | 
        
| 34 |  | import org.sat4j.specs.IOptimizationProblem; | 
        
| 35 |  | import org.sat4j.specs.ISolver; | 
        
| 36 |  | import org.sat4j.specs.IVec; | 
        
| 37 |  | import org.sat4j.specs.IVecInt; | 
        
| 38 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 38 (38) | Complexity: 6 | Complexity Density: 0,59 |  | 
  
| 39 |  | public class WeightedMaxSatDecorator extends AbstractSelectorVariablesDecorator | 
        
| 40 |  | implements IOptimizationProblem { | 
        
| 41 |  |  | 
        
| 42 |  |  | 
        
| 43 |  |  | 
        
| 44 |  |  | 
        
| 45 |  | private static final long serialVersionUID = 1L; | 
        
| 46 |  |  | 
        
| 47 |  | private final IVec<BigInteger> coefs = new Vec<BigInteger>(); | 
        
| 48 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 1 (1) | Complexity: 1 | Complexity Density: 1 |  | 
  
| 49 | 0 |  public WeightedMaxSatDecorator(ISolver solver) {... | 
        
| 50 | 0 | super(solver); | 
        
| 51 |  | } | 
        
| 52 |  |  | 
        
| 53 |  |  | 
        
| 54 |  | protected int top = -1; | 
        
| 55 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 1 (1) | Complexity: 1 | Complexity Density: 1 |  | 
  
| 56 | 0 |  public void setTopWeight(int top) {... | 
        
| 57 | 0 | this.top = top; | 
        
| 58 |  | } | 
        
| 59 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 8 (8) | Complexity: 2 | Complexity Density: 0,33 |  | 
  
| 60 | 0 |  @Override... | 
        
| 61 |  | public IConstr addClause(IVecInt literals) throws ContradictionException { | 
        
| 62 | 0 | int weight = literals.get(0); | 
        
| 63 | 0 | if (weight<top) { | 
        
| 64 | 0 | coefs.push(BigInteger.valueOf(weight)); | 
        
| 65 | 0 | literals.set(0, nborigvars + ++nbnewvar); | 
        
| 66 |  | } else { | 
        
| 67 | 0 | literals.delete(0); | 
        
| 68 |  | } | 
        
| 69 | 0 | return super.addClause(literals); | 
        
| 70 |  | } | 
        
| 71 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 3 (3) | Complexity: 1 | Complexity Density: 0,33 |  | 
  
| 72 | 0 |  @Override... | 
        
| 73 |  | public void reset() { | 
        
| 74 | 0 | coefs.clear(); | 
        
| 75 | 0 | vec.clear(); | 
        
| 76 | 0 | super.reset(); | 
        
| 77 |  | } | 
        
| 78 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 1 (1) | Complexity: 1 | Complexity Density: 1 |  | 
  
| 79 | 0 |  public boolean hasNoObjectiveFunction() {... | 
        
| 80 | 0 | return false; | 
        
| 81 |  | } | 
        
| 82 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 1 (1) | Complexity: 1 | Complexity Density: 1 |  | 
  
| 83 | 0 |  public boolean nonOptimalMeansSatisfiable() {... | 
        
| 84 | 0 | return false; | 
        
| 85 |  | } | 
        
| 86 |  |  | 
        
| 87 |  | private BigInteger counter; | 
        
| 88 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 7 (7) | Complexity: 3 | Complexity Density: 0,6 |  | 
  
| 89 | 0 |  public Number calculateObjective() {... | 
        
| 90 | 0 | counter = BigInteger.ZERO; | 
        
| 91 | 0 | for (int q : prevfullmodel) { | 
        
| 92 | 0 | if (q > nborigvars) { | 
        
| 93 | 0 | counter = counter.add(coefs.get(q - nborigvars - 1)); | 
        
| 94 |  | } | 
        
| 95 |  | } | 
        
| 96 | 0 | return counter; | 
        
| 97 |  | } | 
        
| 98 |  |  | 
        
| 99 |  | private final IVecInt vec = new VecInt(); | 
        
| 100 |  |  | 
        
| 101 |  |  | 
        
| 102 |  |  | 
           
        |  |  | 
           
           |  | 0% | Uncovered Elements: 8 (8) | Complexity: 3 | Complexity Density: 0,75 |  | 
  
| 103 | 0 |  public void discard() throws ContradictionException {... | 
        
| 104 | 0 | if (vec.isEmpty()) { | 
        
| 105 | 0 | for (int i = 1; i <= nbnewvar; i++) { | 
        
| 106 | 0 | vec.push(nborigvars+i); | 
        
| 107 |  | } | 
        
| 108 |  | } | 
        
| 109 |  |  | 
        
| 110 |  |  | 
        
| 111 |  |  | 
        
| 112 |  |  | 
        
| 113 | 0 | super.addPseudoBoolean(vec, coefs, false, counter | 
        
| 114 |  | .subtract(BigInteger.ONE)); | 
        
| 115 |  | } | 
        
| 116 |  |  | 
        
| 117 |  | } |