1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3 *
4 * All rights reserved. This program and the accompanying materials
5 * are made available under the terms of the Eclipse Public License v1.0
6 * which accompanies this distribution, and is available at
7 * http://www.eclipse.org/legal/epl-v10.html
8 *
9 * Alternatively, the contents of this file may be used under the terms of
10 * either the GNU Lesser General Public License Version 2.1 or later (the
11 * "LGPL"), in which case the provisions of the LGPL are applicable instead
12 * of those above. If you wish to allow use of your version of this file only
13 * under the terms of the LGPL, and not to allow others to use your version of
14 * this file under the terms of the EPL, indicate your decision by deleting
15 * the provisions above and replace them with the notice and other provisions
16 * required by the LGPL. If you do not delete the provisions above, a recipient
17 * may use your version of this file under the terms of the EPL or the LGPL.
18 *******************************************************************************/
19 package org.sat4j.maxsat;
20
21 import java.math.BigInteger;
22
23 import org.sat4j.core.Vec;
24 import org.sat4j.core.VecInt;
25 import org.sat4j.pb.IPBSolver;
26 import org.sat4j.pb.PBSolverDecorator;
27 import org.sat4j.specs.ContradictionException;
28 import org.sat4j.specs.IOptimizationProblem;
29 import org.sat4j.specs.IVec;
30 import org.sat4j.specs.IVecInt;
31 import org.sat4j.specs.TimeoutException;
32
33 /**
34 * A decorator that computes minimal cost models. That problem is also known as binate covering problem.
35 *
36 * Please make sure that newVar(howmany) is called first to setup the decorator.
37 *
38 * @author daniel
39 *
40 */
41 public class MinCostDecorator extends PBSolverDecorator implements
42 IOptimizationProblem {
43
44 /**
45 *
46 */
47 private static final long serialVersionUID = 1L;
48
49 private int[] costs;
50
51 private int[] prevmodel;
52
53 private final IVecInt vars = new VecInt();
54
55 private final IVec<BigInteger> coeffs = new Vec<BigInteger>();
56
57 public MinCostDecorator(IPBSolver solver) {
58 super(solver);
59 }
60
61 /*
62 * (non-Javadoc)
63 *
64 * @see org.sat4j.tools.SolverDecorator#newVar()
65 */
66 @Override
67 public int newVar() {
68 throw new UnsupportedOperationException();
69 }
70
71 /**
72 * Setup the number of variables to use inside the solver.
73 *
74 * It is mandatory to call that method before setting the cost of the
75 * variables.
76 *
77 * @param howmany
78 * the maximum number of variables in the solver.
79 */
80 @Override
81 public int newVar(int howmany) {
82 costs = new int[howmany + 1];
83 // Arrays.fill(costs, 1);
84 vars.clear();
85 coeffs.clear();
86 for (int i = 1; i <= howmany; i++) {
87 vars.push(i);
88 coeffs.push(BigInteger.ZERO);
89 }
90 // should the default cost be 1????
91 // here it is 0
92 return super.newVar(howmany);
93 }
94
95 /**
96 * to know the cost of a given var.
97 *
98 * @param var
99 * a variable in dimacs format
100 * @return the cost of that variable when assigned to true
101 */
102 public int costOf(int var) {
103 return costs[var];
104 }
105
106 /**
107 * to set the cost of a given var.
108 *
109 * @param var
110 * a variable in dimacs format
111 * @param cost
112 * the cost of var when assigned to true
113 */
114 public void setCost(int var, int cost) {
115 costs[var] = cost;
116 coeffs.set(var - 1, BigInteger.valueOf(cost));
117 }
118
119 public boolean admitABetterSolution() throws TimeoutException {
120 boolean result = super.isSatisfiable(true);
121 if (result)
122 prevmodel = super.model();
123 return result;
124 }
125
126 public boolean hasNoObjectiveFunction() {
127 return false;
128 }
129
130 public boolean nonOptimalMeansSatisfiable() {
131 return true;
132 }
133
134 public Number calculateObjective() {
135 return new Integer(calculateDegree(prevmodel));
136 }
137
138 private int calculateDegree(int[] prevmodel2) {
139 int tmpcost = 0;
140 for (int i = 1; i < costs.length; i++) {
141 if (prevmodel2[i - 1] > 0) {
142 tmpcost += costs[i];
143 }
144 }
145 return tmpcost;
146 }
147
148 public void discard() throws ContradictionException {
149 super.addPseudoBoolean(vars, coeffs, false, BigInteger
150 .valueOf(calculateDegree(prevmodel) - 1));
151 }
152
153 @Override
154 public int[] model() {
155 // DLB findbugs ok
156 return prevmodel;
157 }
158
159 }