Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
26   157   5   2,17
8   76   0,62   12
12     1,33  
1    
 
  MinCostDecorator       Line # 40 26 5 0% 0.0
 
No Tests
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    *
4    * Based on the original minisat specification from:
5    *
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    *
10    * This library is free software; you can redistribute it and/or modify it under
11    * the terms of the GNU Lesser General Public License as published by the Free
12    * Software Foundation; either version 2.1 of the License, or (at your option)
13    * any later version.
14    *
15    * This library is distributed in the hope that it will be useful, but WITHOUT
16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18    * details.
19    *
20    * You should have received a copy of the GNU Lesser General Public License
21    * along with this library; if not, write to the Free Software Foundation, Inc.,
22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
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.IOptimizationProblem;
34    import org.sat4j.specs.ISolver;
35    import org.sat4j.specs.IVec;
36    import org.sat4j.specs.IVecInt;
37    import org.sat4j.specs.TimeoutException;
38    import org.sat4j.tools.SolverDecorator;
39   
 
40    public class MinCostDecorator extends SolverDecorator implements
41    IOptimizationProblem {
42   
43    /**
44    *
45    */
46    private static final long serialVersionUID = 1L;
47   
48    private int[] costs;
49   
50    private int[] prevmodel;
51   
52    private final IVecInt vars = new VecInt();
53   
54    private final IVec<BigInteger> coeffs = new Vec<BigInteger>();
55   
 
56  0 toggle public MinCostDecorator(ISolver solver) {
57  0 super(solver);
58    }
59   
60    /*
61    * (non-Javadoc)
62    *
63    * @see org.sat4j.tools.SolverDecorator#newVar()
64    */
 
65  0 toggle @Override
66    public int newVar() {
67  0 throw new UnsupportedOperationException();
68    }
69   
70    /**
71    * Setup the number of variables to use inside the solver.
72    *
73    * It is mandatory to call that method before setting the cost of the
74    * variables.
75    *
76    * @param howmany
77    * the maximum number of variables in the solver.
78    */
 
79  0 toggle @Override
80    public int newVar(int howmany) {
81  0 costs = new int[howmany + 1];
82    // Arrays.fill(costs, 1);
83  0 vars.clear();
84  0 coeffs.clear();
85  0 for (int i = 1; i <= howmany; i++) {
86  0 vars.push(i);
87  0 coeffs.push(BigInteger.ZERO);
88    }
89    // should the default cost be 1????
90    // here it is 0
91  0 return super.newVar(howmany);
92    }
93   
94    /**
95    * to know the cost of a given var.
96    *
97    * @param var
98    * a variable in dimacs format
99    * @return the cost of that variable when assigned to true
100    */
 
101  0 toggle public int costOf(int var) {
102  0 return costs[var];
103    }
104   
105    /**
106    * to set the cost of a given var.
107    *
108    * @param var
109    * a variable in dimacs format
110    * @param cost
111    * the cost of var when assigned to true
112    */
 
113  0 toggle public void setCost(int var, int cost) {
114  0 costs[var] = cost;
115  0 coeffs.set(var - 1, BigInteger.valueOf(cost));
116    }
117   
 
118  0 toggle public boolean admitABetterSolution() throws TimeoutException {
119  0 boolean result = super.isSatisfiable();
120  0 if (result)
121  0 prevmodel = super.model();
122  0 return result;
123    }
124   
 
125  0 toggle public boolean hasNoObjectiveFunction() {
126  0 return false;
127    }
128   
 
129  0 toggle public boolean nonOptimalMeansSatisfiable() {
130  0 return true;
131    }
132   
 
133  0 toggle public Number calculateObjective() {
134  0 return calculateDegree(prevmodel);
135    }
136   
 
137  0 toggle private int calculateDegree(int[] prevmodel2) {
138  0 int tmpcost = 0;
139  0 for (int i = 1; i < costs.length; i++) {
140  0 if (prevmodel2[i - 1] > 0) {
141  0 tmpcost += costs[i];
142    }
143    }
144  0 return tmpcost;
145    }
146   
 
147  0 toggle public void discard() throws ContradictionException {
148  0 super.addPseudoBoolean(vars, coeffs, false, BigInteger
149    .valueOf(calculateDegree(prevmodel) - 1));
150    }
151   
 
152  0 toggle @Override
153    public int[] model() {
154  0 return prevmodel;
155    }
156   
157    }