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  package org.sat4j.minisat.constraints;
26  
27  import java.math.BigInteger;
28  
29  import org.sat4j.core.Vec;
30  import org.sat4j.core.VecInt;
31  import org.sat4j.minisat.constraints.cnf.WLClause;
32  import org.sat4j.minisat.constraints.pb.IDataStructurePB;
33  import org.sat4j.minisat.constraints.pb.PBConstr;
34  import org.sat4j.minisat.constraints.pb.WatchPb;
35  import org.sat4j.specs.ContradictionException;
36  import org.sat4j.specs.IVec;
37  import org.sat4j.specs.IVecInt;
38  
39  public abstract class AbstractPBClauseCardConstrDataStructure extends
40          AbstractPBDataStructureFactory {
41  
42      private static final BigInteger MAX_INT_VALUE = BigInteger
43              .valueOf(Integer.MAX_VALUE);
44  
45      /*
46       * (non-Javadoc)
47       * 
48       * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
49       *      org.sat4j.specs.VecInt, boolean, int)
50       */
51      @Override
52      protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs,
53              boolean moreThan, int degree) throws ContradictionException {
54          return constraintFactory(literals, WatchPb.toVecBigInt(coefs),
55                  moreThan, WatchPb.toBigInt(degree));
56      }
57  
58      /*
59       * (non-Javadoc)
60       * 
61       * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
62       *      org.sat4j.specs.VecInt, int)
63       */
64      @Override
65      protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs,
66              int degree) {
67          return constraintFactory(literals, WatchPb.toVecBigInt(coefs), WatchPb
68                  .toBigInt(degree));
69      }
70  
71      /*
72       * (non-Javadoc)
73       * 
74       * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
75       *      org.sat4j.specs.VecInt, boolean, int)
76       */
77      @Override
78      protected PBConstr constraintFactory(IVecInt literals,
79              IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
80              throws ContradictionException {
81          IDataStructurePB mpb = WatchPb.niceParameters(literals, coefs,
82                  moreThan, degree, getVocabulary());
83          if (mpb == null)
84              return null;
85          int size = mpb.size();
86          int[] lits = new int[size];
87          BigInteger[] normCoefs = new BigInteger[size];
88          mpb.buildConstraintFromMapPb(lits, normCoefs);
89          if (mpb.getDegree().equals(BigInteger.ONE)) {
90              IVecInt v = WLClause.sanityCheck(new VecInt(lits), getVocabulary(),
91                      solver);
92              if (v == null)
93                  return null;
94              return constructClause(v);
95          }
96          if (coefficientsEqualToOne(new Vec<BigInteger>(normCoefs))) {
97              assert mpb.getDegree().compareTo(MAX_INT_VALUE) < 0;
98              return constructCard(new VecInt(lits), mpb.getDegree().intValue());
99          }
100         //return constructPB(mpb);
101         return constructPB(lits,normCoefs,mpb.getDegree());
102     }
103 
104     /*
105      * (non-Javadoc)
106      * 
107      * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
108      *      org.sat4j.specs.VecInt, int)
109      */
110     @Override
111     protected PBConstr constraintFactory(IVecInt literals,
112             IVec<BigInteger> coefs, BigInteger degree) {
113         if (degree.equals(BigInteger.ONE)) {
114             return constructLearntClause(literals);
115         }
116         if (coefficientsEqualToOne(coefs)) {
117             return constructLearntCard(literals, degree.intValue());
118         }
119         return constructLearntPB(literals, coefs, degree);
120     }
121 
122     private static boolean coefficientsEqualToOne(IVec<BigInteger> coeffs) {
123         for (int i = 0; i < coeffs.size(); i++)
124             if (!coeffs.get(i).equals(BigInteger.ONE))
125                 return false;
126         return true;
127     }
128 
129     abstract protected PBConstr constructClause(IVecInt v);
130 
131     abstract protected PBConstr constructCard(IVecInt lits, int degree)
132             throws ContradictionException;
133 
134     abstract protected PBConstr constructPB(IDataStructurePB mpb)
135             throws ContradictionException;
136 
137     abstract protected PBConstr constructPB(int[] lits, BigInteger[] coefs, BigInteger degree)
138     throws ContradictionException;
139 
140    abstract protected PBConstr constructLearntClause(IVecInt literals);
141 
142     abstract protected PBConstr constructLearntCard(IVecInt literals, int degree);
143 
144     abstract protected PBConstr constructLearntPB(IVecInt literals,
145             IVec<BigInteger> coefs, BigInteger degree);
146 
147 }