View Javadoc

1   /*******************************************************************************
2   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
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 pseudo boolean algorithms described in:
20  * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21  * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22  * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23  * 
24  * and 
25  * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL 
26  * Framework. Ph.D. Dissertation, University of Oregon.
27  *******************************************************************************/
28  package org.sat4j.pb.constraints;
29  
30  import java.math.BigInteger;
31  
32  import org.sat4j.core.Vec;
33  import org.sat4j.core.VecInt;
34  import org.sat4j.minisat.constraints.cnf.Clauses;
35  import org.sat4j.pb.constraints.pb.IDataStructurePB;
36  import org.sat4j.pb.constraints.pb.PBConstr;
37  import org.sat4j.pb.constraints.pb.Pseudos;
38  import org.sat4j.specs.ContradictionException;
39  import org.sat4j.specs.IVec;
40  import org.sat4j.specs.IVecInt;
41  
42  public abstract class AbstractPBClauseCardConstrDataStructure extends
43          AbstractPBDataStructureFactory {
44  
45      /**
46  	 * 
47  	 */
48  	private static final long serialVersionUID = 1L;
49  	
50  	static final BigInteger MAX_INT_VALUE = BigInteger
51              .valueOf(Integer.MAX_VALUE);
52  
53      /*
54       * (non-Javadoc)
55       * 
56       * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
57       *      org.sat4j.specs.VecInt, boolean, int)
58       */
59      @Override
60      protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs,
61              boolean moreThan, int degree) throws ContradictionException {
62          return constraintFactory(literals, Pseudos.toVecBigInt(coefs),
63                  moreThan, BigInteger.valueOf(degree));
64      }
65  
66      /*
67       * (non-Javadoc)
68       * 
69       * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
70       *      org.sat4j.specs.VecInt, int)
71       */
72      @Override
73      protected PBConstr constraintFactory(IVecInt literals, IVecInt coefs,
74              int degree) {
75          return constraintFactory(literals, Pseudos.toVecBigInt(coefs), BigInteger.valueOf(degree));
76      }
77  
78      /*
79       * (non-Javadoc)
80       * 
81       * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
82       *      org.sat4j.specs.VecInt, boolean, int)
83       */
84      @Override
85      protected PBConstr constraintFactory(IVecInt literals,
86              IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
87              throws ContradictionException {
88          IDataStructurePB mpb = Pseudos.niceParameters(literals, coefs,
89                  moreThan, degree, getVocabulary());
90          if (mpb == null)
91              return null;
92          int size = mpb.size();
93          int[] theLists = new int[size];
94          BigInteger[] normCoefs = new BigInteger[size];
95          mpb.buildConstraintFromMapPb(theLists, normCoefs);
96          if (mpb.getDegree().equals(BigInteger.ONE)) {
97              IVecInt v = Clauses.sanityCheck(new VecInt(theLists), getVocabulary(),
98                      solver);
99              if (v == null)
100                 return null;
101             return constructClause(v);
102         }
103         if (coefficientsEqualToOne(new Vec<BigInteger>(normCoefs))) {
104             assert mpb.getDegree().compareTo(MAX_INT_VALUE) < 0;
105             return constructCard(new VecInt(theLists), mpb.getDegree().intValue());
106         }
107         //return constructPB(mpb);
108         return constructPB(theLists,normCoefs,mpb.getDegree());
109     }
110 
111     /*
112      * (non-Javadoc)
113      * 
114      * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
115      *      org.sat4j.specs.VecInt, int)
116      */
117     @Override
118     protected PBConstr constraintFactory(IDataStructurePB dspb) {
119         if (dspb.getDegree().equals(BigInteger.ONE)) {
120             return constructLearntClause(dspb);
121         }
122         if (dspb.isCardinality()) {
123             return constructLearntCard(dspb);
124         }
125         return constructLearntPB(dspb);
126     }
127 
128     /*
129      * (non-Javadoc)
130      * 
131      * @see org.sat4j.minisat.constraints.AbstractPBDataStructureFactory#constraintFactory(org.sat4j.specs.VecInt,
132      *      org.sat4j.specs.VecInt, int)
133      */
134     @Override
135     protected PBConstr constraintFactory(IVecInt literals,
136             IVec<BigInteger> coefs, BigInteger degree) {
137         if (degree.equals(BigInteger.ONE)) {
138             return constructLearntClause(literals);
139         }
140         if (coefficientsEqualToOne(coefs)) {
141             return constructLearntCard(literals, degree.intValue());
142         }
143         return constructLearntPB(literals, coefs, degree);
144     }
145 
146 
147     
148     static boolean coefficientsEqualToOne(IVec<BigInteger> coeffs) {
149         for (int i = 0; i < coeffs.size(); i++)
150             if (!coeffs.get(i).equals(BigInteger.ONE))
151                 return false;
152         return true;
153     }
154 
155     abstract protected PBConstr constructClause(IVecInt v) throws ContradictionException;
156 
157     abstract protected PBConstr constructCard(IVecInt theLits, int degree)
158             throws ContradictionException;
159 
160     abstract protected PBConstr constructPB(IDataStructurePB mpb)
161             throws ContradictionException;
162 
163     abstract protected PBConstr constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
164     throws ContradictionException;
165 
166     abstract protected PBConstr constructLearntClause(IVecInt literals);
167 
168     abstract protected PBConstr constructLearntCard(IVecInt literals, int degree);
169 
170     abstract protected PBConstr constructLearntPB(IVecInt literals,
171             IVec<BigInteger> coefs, BigInteger degree);
172 
173     abstract protected PBConstr constructLearntClause(IDataStructurePB dspb);
174 
175     abstract protected PBConstr constructLearntCard(IDataStructurePB dspb);
176 
177     abstract protected PBConstr constructLearntPB(IDataStructurePB dspb);
178 
179 
180 }