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 /**
41 * A decorator that computes minimal cost models.
42 *
43 * Please make sure that newVar(howmany) is called first to setup the decorator.
44 *
45 * @author daniel
46 *
47 */
48 public class MinCostDecorator extends SolverDecorator implements
49 IOptimizationProblem {
50
51 /**
52 *
53 */
54 private static final long serialVersionUID = 1L;
55
56 private int[] costs;
57
58 private int[] prevmodel;
59
60 private final IVecInt vars = new VecInt();
61
62 private final IVec<BigInteger> coeffs = new Vec<BigInteger>();
63
64 public MinCostDecorator(ISolver solver) {
65 super(solver);
66 }
67
68 /*
69 * (non-Javadoc)
70 *
71 * @see org.sat4j.tools.SolverDecorator#newVar()
72 */
73 @Override
74 public int newVar() {
75 throw new UnsupportedOperationException();
76 }
77
78 /**
79 * Setup the number of variables to use inside the solver.
80 *
81 * It is mandatory to call that method before setting the cost of the
82 * variables.
83 *
84 * @param howmany
85 * the maximum number of variables in the solver.
86 */
87 @Override
88 public int newVar(int howmany) {
89 costs = new int[howmany + 1];
90 // Arrays.fill(costs, 1);
91 vars.clear();
92 coeffs.clear();
93 for (int i = 1; i <= howmany; i++) {
94 vars.push(i);
95 coeffs.push(BigInteger.ZERO);
96 }
97 // should the default cost be 1????
98 // here it is 0
99 return super.newVar(howmany);
100 }
101
102 /**
103 * to know the cost of a given var.
104 *
105 * @param var
106 * a variable in dimacs format
107 * @return the cost of that variable when assigned to true
108 */
109 public int costOf(int var) {
110 return costs[var];
111 }
112
113 /**
114 * to set the cost of a given var.
115 *
116 * @param var
117 * a variable in dimacs format
118 * @param cost
119 * the cost of var when assigned to true
120 */
121 public void setCost(int var, int cost) {
122 costs[var] = cost;
123 coeffs.set(var - 1, BigInteger.valueOf(cost));
124 }
125
126 public boolean admitABetterSolution() throws TimeoutException {
127 boolean result = super.isSatisfiable();
128 if (result)
129 prevmodel = super.model();
130 return result;
131 }
132
133 public boolean hasNoObjectiveFunction() {
134 return false;
135 }
136
137 public boolean nonOptimalMeansSatisfiable() {
138 return true;
139 }
140
141 public Number calculateObjective() {
142 return calculateDegree(prevmodel);
143 }
144
145 private int calculateDegree(int[] prevmodel2) {
146 int tmpcost = 0;
147 for (int i = 1; i < costs.length; i++) {
148 if (prevmodel2[i - 1] > 0) {
149 tmpcost += costs[i];
150 }
151 }
152 return tmpcost;
153 }
154
155 public void discard() throws ContradictionException {
156 super.addPseudoBoolean(vars, coeffs, false, BigInteger
157 .valueOf(calculateDegree(prevmodel) - 1));
158 }
159
160 @Override
161 public int[] model() {
162 // DLB findbugs ok
163 return prevmodel;
164 }
165
166 }