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.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  
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  
49      public WeightedMaxSatDecorator(ISolver solver) {
50          super(solver);
51      }
52      
53      
54      protected int top = -1;
55  
56      public void setTopWeight(int top) {
57          this.top = top;
58      }
59      
60      @Override
61      public IConstr addClause(IVecInt literals) throws ContradictionException {
62          int weight = literals.get(0);
63          if (weight<top) {
64          coefs.push(BigInteger.valueOf(weight));
65          literals.set(0, nborigvars + ++nbnewvar);        
66          } else {
67              literals.delete(0);
68          }
69          return super.addClause(literals);
70      }
71  
72      @Override
73      public void reset() {
74          coefs.clear();
75          vec.clear();
76          super.reset();
77      }
78  
79      public boolean hasNoObjectiveFunction() {
80          return false;
81      }
82  
83      public boolean nonOptimalMeansSatisfiable() {
84          return false;
85      }
86  
87      private BigInteger counter;
88  
89      public Number calculateObjective() {
90          counter = BigInteger.ZERO;
91          for (int q : prevfullmodel) {
92              if (q > nborigvars) {
93                  counter = counter.add(coefs.get(q - nborigvars - 1));
94              }
95          }
96          return counter;
97      }
98  
99      private final IVecInt vec = new VecInt();
100 
101     // private IConstr prevconstr;
102 
103     public void discard() throws ContradictionException {
104         if (vec.isEmpty()) {
105             for (int i = 1; i <= nbnewvar; i++) {
106                 vec.push(nborigvars+i);
107             }
108         }
109         // if (prevconstr!=null)
110         // super.removeConstr(prevconstr);
111 
112         // prevconstr =
113         super.addPseudoBoolean(vec, coefs, false, counter
114                 .subtract(BigInteger.ONE));
115     }
116 
117 }