View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
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   * Based on the original MiniSat specification from:
20   *
21   * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22   * Sixth International Conference on Theory and Applications of Satisfiability
23   * Testing, LNCS 2919, pp 502-518, 2003.
24   *
25   * See www.minisat.se for the original solver in C++.
26   *
27   * Contributors:
28   *   CRIL - initial API and implementation
29   *******************************************************************************/
30  
31  package org.sat4j.pb.tools;
32  
33  import java.math.BigInteger;
34  import java.util.Iterator;
35  
36  import org.sat4j.core.ConstrGroup;
37  import org.sat4j.core.VecInt;
38  import org.sat4j.pb.IPBSolver;
39  import org.sat4j.pb.ObjectiveFunction;
40  import org.sat4j.specs.ContradictionException;
41  import org.sat4j.specs.IConstr;
42  import org.sat4j.specs.IVec;
43  import org.sat4j.specs.IVecInt;
44  import org.sat4j.tools.xplain.Xplain;
45  
46  public class XplainPB extends Xplain<IPBSolver> implements IPBSolver {
47  
48      /**
49  	 * 
50  	 */
51      private static final long serialVersionUID = 1L;
52  
53      public XplainPB(IPBSolver solver) {
54          super(solver);
55      }
56  
57      @Override
58      public IConstr addAtLeast(IVecInt literals, int degree)
59              throws ContradictionException {
60          IVecInt coeffs = new VecInt(literals.size(), 1);
61          int newvar = createNewVar(literals);
62          literals.push(newvar);
63          coeffs.push(coeffs.size() - degree);
64          IConstr constr = decorated().addAtLeast(literals, coeffs, degree);
65          if (constr == null) {
66              // constraint trivially satisfied
67              discardLastestVar();
68          } else {
69              this.constrs.put(newvar, constr);
70          }
71          return constr;
72      }
73  
74      @Override
75      public IConstr addAtMost(IVecInt literals, int degree)
76              throws ContradictionException {
77          IVecInt coeffs = new VecInt(literals.size(), 1);
78          int newvar = createNewVar(literals);
79          literals.push(newvar);
80          coeffs.push(degree - coeffs.size());
81          IConstr constr = decorated().addAtMost(literals, coeffs, degree);
82          if (constr == null) {
83              // constraint trivially satisfied
84              discardLastestVar();
85          } else {
86              this.constrs.put(newvar, constr);
87          }
88          return constr;
89      }
90  
91      @Override
92      public IConstr addExactly(IVecInt literals, int n)
93              throws ContradictionException {
94          int newvar = createNewVar(literals);
95  
96          // at most
97          IVecInt coeffs = new VecInt(literals.size(), 1);
98          literals.push(newvar);
99          coeffs.push(n - coeffs.size());
100         IConstr constr1 = decorated().addAtMost(literals, coeffs, n);
101         // at least
102         coeffs.pop();
103         coeffs.push(coeffs.size() - n);
104         IConstr constr2 = decorated().addAtLeast(literals, coeffs, n);
105         if (constr1 == null && constr2 == null) {
106             discardLastestVar();
107             return null;
108         }
109         ConstrGroup group = new ConstrGroup();
110         group.add(constr1);
111         group.add(constr2);
112         this.constrs.put(newvar, group);
113         return group;
114     }
115 
116     public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
117             boolean moreThan, BigInteger d) throws ContradictionException {
118         int newvar = createNewVar(lits);
119         lits.push(newvar);
120         if (moreThan && d.signum() >= 0) {
121             coeffs.push(d);
122         } else {
123             BigInteger sum = BigInteger.ZERO;
124             for (Iterator<BigInteger> ite = coeffs.iterator(); ite.hasNext();) {
125                 sum = sum.add(ite.next());
126             }
127             sum = sum.subtract(d);
128             coeffs.push(sum.negate());
129         }
130         IConstr constr = decorated()
131                 .addPseudoBoolean(lits, coeffs, moreThan, d);
132         if (constr == null) {
133             // constraint trivially satisfied
134             discardLastestVar();
135             // System.err.println(lits.toString()+"/"+coeffs+"/"+(moreThan?">=":"<=")+d);
136         } else {
137             this.constrs.put(newvar, constr);
138         }
139         return constr;
140     }
141 
142     public void setObjectiveFunction(ObjectiveFunction obj) {
143         decorated().setObjectiveFunction(obj);
144     }
145 
146     public ObjectiveFunction getObjectiveFunction() {
147         return decorated().getObjectiveFunction();
148     }
149 
150     public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
151             throws ContradictionException {
152         throw new UnsupportedOperationException();
153     }
154 
155     public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
156             BigInteger degree) throws ContradictionException {
157         throw new UnsupportedOperationException();
158     }
159 
160     public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
161             throws ContradictionException {
162         throw new UnsupportedOperationException();
163     }
164 
165     public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
166             BigInteger degree) throws ContradictionException {
167         throw new UnsupportedOperationException();
168     }
169 
170     public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
171             throws ContradictionException {
172         throw new UnsupportedOperationException();
173     }
174 
175     public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
176             BigInteger weight) throws ContradictionException {
177         throw new UnsupportedOperationException();
178     }
179 }