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;
27  
28  import java.math.BigInteger;
29  
30  import org.sat4j.minisat.constraints.card.AtLeast;
31  import org.sat4j.minisat.constraints.cnf.Lits;
32  import org.sat4j.minisat.core.Constr;
33  import org.sat4j.minisat.core.ILits;
34  import org.sat4j.specs.ContradictionException;
35  import org.sat4j.specs.IVec;
36  import org.sat4j.specs.IVecInt;
37  
38  /**
39   * @author leberre To change the template for this generated type comment go to
40   *         Window - Preferences - Java - Code Generation - Code and Comments
41   */
42  @SuppressWarnings("PMD")
43  public abstract class AbstractCardinalityDataStructure extends
44          AbstractDataStructureFactory<ILits> {
45  
46      /*
47       * Create a Cardinality Constraint from a PB format. The coefs should all be
48       * equal to 1.
49       */
50      @Override
51      public Constr createPseudoBooleanConstraint(IVecInt literals,
52              IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
53              throws ContradictionException {
54          BigInteger diff = reduceToCard(coefs, literals);
55          degree = degree.add(diff);
56          assert coefficientsEqualToOne(coefs);
57          if (moreThan) {
58              return AtLeast.atLeastNew(solver, getVocabulary(), literals, degree
59                      .intValue());
60          }
61          for (int i = 0; i < literals.size(); i++) {
62              literals.set(i, literals.get(i) ^ 1);
63          }
64          return AtLeast.atLeastNew(solver, getVocabulary(), literals, coefs
65                  .size()
66                  - degree.intValue());
67      }
68  
69      public static boolean coefficientsEqualToOne(IVec<BigInteger> v) {
70          for (int i = 0; i < v.size(); i++) {
71              if (!v.get(i).equals(BigInteger.ONE))
72                  return false;
73          }
74          return true;
75      }
76  
77      private BigInteger reduceToCard(IVec<BigInteger> coefs, IVecInt literals) {
78          int diff = 0;
79          for (int i = 0; i < coefs.size(); i++) {
80              assert coefs.get(i).abs().equals(BigInteger.ONE);
81              if (coefs.get(i).signum() < 0) {
82                  assert coefs.get(i).equals(BigInteger.ONE.negate());
83                  diff++;
84                  literals.set(i, literals.get(i) ^ 1);
85                  coefs.set(i, BigInteger.ONE);
86              }
87          }
88          return BigInteger.valueOf(diff);
89      }
90  
91      @Override
92      protected ILits createLits() {
93          return new Lits();
94      }
95  }