View Javadoc

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.minisat.constraints.pb;
27  
28  import java.math.BigInteger;
29  import java.util.HashMap;
30  import java.util.Map;
31  
32  import org.sat4j.minisat.constraints.cnf.Lits;
33  import org.sat4j.minisat.core.VarActivityListener;
34  import org.sat4j.specs.IVec;
35  import org.sat4j.specs.IVecInt;
36  
37  /**
38   * @author parrain 
39   * 
40   */
41  public class MapPb implements IDataStructurePB {
42  
43      /*
44       * During the process of cutting planes, pseudo-boolean constraints are
45       * coded with a HashMap <literal, coefficient> and a BigInteger for the
46       * degree.
47       */
48      protected Map<Integer, BigInteger> coefs;
49  
50      protected BigInteger degree;
51  
52      MapPb(Map<Integer, BigInteger> m, BigInteger d) {
53          coefs = m;
54          degree = d;
55      }
56  
57      MapPb() {
58          this(new HashMap<Integer, BigInteger>(), BigInteger.ZERO);
59      }
60  
61      public BigInteger saturation() {
62          assert degree.signum() > 0;
63          BigInteger minimum = degree;
64          for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
65              assert e.getValue().signum() > 0;
66              // e.setValue(degree.min(e.getValue()));
67              if (degree.compareTo(e.getValue()) < 0)
68                  setCoef(e.getKey(), degree);
69              assert e.getValue().signum() > 0;
70              minimum = minimum.min(e.getValue());
71          }
72          // on a appris une clause
73          if (minimum.equals(degree) && minimum.compareTo(BigInteger.ONE) > 0) {
74              degree = BigInteger.ONE;
75              for (Integer i : coefs.keySet())
76                  // coefs.put(i, BigInteger.ONE);
77                  setCoef(i, BigInteger.ONE);
78          }
79  
80          return degree;
81      }
82  
83      public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
84              BigInteger[] reducedCoefs, VarActivityListener val) {
85          return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE, val);
86      }
87  
88      public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
89              BigInteger[] reducedCoefs, BigInteger coefMult,
90              VarActivityListener val) {
91          degree = degree.add(degreeCons);
92          assert degree.signum() > 0;
93  
94          if (reducedCoefs == null)
95              for (int i = 0; i < cpb.size(); i++) {
96                  val.varBumpActivity(cpb.get(i));
97                  cuttingPlaneStep(cpb.get(i), multiplyCoefficient(
98                          cpb.getCoef(i), coefMult));
99              }
100         else
101             for (int i = 0; i < cpb.size(); i++) {
102                 val.varBumpActivity(cpb.get(i));
103                 cuttingPlaneStep(cpb.get(i), multiplyCoefficient(
104                         reducedCoefs[i], coefMult));
105             }
106 
107         return degree;
108     }
109 
110     public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
111             BigInteger deg) {
112         return cuttingPlane(lits, reducedCoefs, deg, BigInteger.ONE);
113     }
114 
115     public BigInteger cuttingPlane(int lits[], BigInteger[] reducedCoefs,
116             BigInteger degreeCons, BigInteger coefMult) {
117         degree = degree.add(degreeCons);
118         assert degree.signum() > 0;
119 
120         for (int i = 0; i < lits.length; i++)
121             cuttingPlaneStep(lits[i], reducedCoefs[i].multiply(coefMult));
122 
123         return degree;
124     }
125 
126     private void cuttingPlaneStep(final int lit, final BigInteger coef) {
127         assert coef.signum() >= 0;
128         Integer blit = Integer.valueOf(lit);
129         Integer bnlit = Integer.valueOf(lit ^ 1);
130         if (coef.signum() > 0) {
131             if (coefs.containsKey(bnlit)) {
132                 assert !coefs.containsKey(blit);
133                 if (coefs.get(bnlit).compareTo(coef) < 0) {
134                     BigInteger tmp = coefs.get(bnlit);
135                     // coefs.put(blit, coef.subtract(tmp));
136                     setCoef(blit, coef.subtract(tmp));
137                     assert coefs.get(blit).signum() > 0;
138                     degree = degree.subtract(tmp);
139                     // coefs.remove(bnlit);
140                     removeCoef(bnlit);
141                 } else {
142                     if (coefs.get(bnlit).equals(coef)) {
143                         degree = degree.subtract(coef);
144                         // coefs.remove(bnlit);
145                         removeCoef(bnlit);
146                     } else {
147                         // coefs.put(bnlit, coefs.get(bnlit).subtract(coef));
148                         decreaseCoef(bnlit, coef);
149                         assert coefs.get(bnlit).signum() > 0;
150                         degree = degree.subtract(coef);
151                     }
152                 }
153             } else {
154                 assert (!coefs.containsKey(blit))
155                         || (coefs.get(blit).signum() > 0);
156                 if (coefs.containsKey(blit))
157                     increaseCoef(blit, coef);
158                 else
159                     setCoef(blit, coef);
160                 // coefs.put(blit, (coefs.containsKey(blit) ? coefs.get(blit)
161                 // : BigInteger.ZERO).add(coef));
162                 assert coefs.get(blit).signum() > 0;
163             }
164         }
165         assert (!coefs.containsKey(bnlit)) || (!coefs.containsKey(blit));
166     }
167 
168     public void buildConstraintFromConflict(IVecInt resLits,
169             IVec<BigInteger> resCoefs) {
170         resLits.clear();
171         resCoefs.clear();
172         // On recherche tous les litt?raux concern?s
173         for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
174             resLits.push(e.getKey());
175             assert e.getValue().signum() > 0;
176             resCoefs.push(e.getValue());
177         }
178     };
179 
180     public void buildConstraintFromMapPb(int[] resLits, BigInteger[] resCoefs) {
181         // On recherche tous les litt?raux concern?s
182         assert resLits.length == resCoefs.length;
183         assert resLits.length == coefs.keySet().size();
184         int i = 0;
185         for (Map.Entry<Integer, BigInteger> e : coefs.entrySet()) {
186             resLits[i] = e.getKey();
187             assert e.getValue().signum() > 0;
188             resCoefs[i] = e.getValue();
189             i++;
190         }
191     };
192 
193     public BigInteger getDegree() {
194         return degree;
195     }
196 
197     public int size() {
198         return coefs.keySet().size();
199     }
200 
201     /*
202      * (non-Javadoc)
203      * 
204      * @see java.lang.Object#toString()
205      */
206     @Override
207     public String toString() {
208         StringBuilder stb = new StringBuilder();
209         for (Map.Entry<Integer, BigInteger> entry : coefs.entrySet()) {
210             stb.append(entry.getValue());
211             stb.append(".");
212             stb.append(Lits.toString(entry.getKey()));
213             stb.append(" ");
214         }
215         return stb.toString() + " >= " + degree; //$NON-NLS-1$
216     }
217 
218     private BigInteger multiplyCoefficient(BigInteger coef, BigInteger mult) {
219         if (coef.equals(BigInteger.ONE))
220             return mult;
221         return coef.multiply(mult);
222     }
223 
224     void increaseCoef(Integer lit, BigInteger incCoef) {
225         coefs.put(lit, coefs.get(lit).add(incCoef));
226     }
227 
228     void decreaseCoef(Integer lit, BigInteger decCoef) {
229         coefs.put(lit, coefs.get(lit).subtract(decCoef));
230     }
231 
232     void setCoef(Integer lit, BigInteger newValue) {
233         coefs.put(lit, newValue);
234     }
235 
236     void removeCoef(Integer lit) {
237         coefs.remove(lit);
238     }
239 
240 }