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  package org.sat4j.pb.constraints;
31  
32  import java.lang.reflect.Field;
33  import java.math.BigInteger;
34  
35  import org.sat4j.core.Vec;
36  import org.sat4j.core.VecInt;
37  import org.sat4j.minisat.constraints.AbstractDataStructureFactory;
38  import org.sat4j.minisat.constraints.card.AtLeast;
39  import org.sat4j.minisat.constraints.cnf.Clauses;
40  import org.sat4j.minisat.constraints.cnf.LearntBinaryClause;
41  import org.sat4j.minisat.constraints.cnf.LearntHTClause;
42  import org.sat4j.minisat.constraints.cnf.Lits;
43  import org.sat4j.minisat.constraints.cnf.OriginalBinaryClause;
44  import org.sat4j.minisat.constraints.cnf.OriginalHTClause;
45  import org.sat4j.minisat.constraints.cnf.UnitClause;
46  import org.sat4j.minisat.core.Constr;
47  import org.sat4j.minisat.core.ILits;
48  import org.sat4j.pb.constraints.pb.AtLeastPB;
49  import org.sat4j.pb.constraints.pb.IDataStructurePB;
50  import org.sat4j.pb.constraints.pb.Pseudos;
51  import org.sat4j.pb.core.PBDataStructureFactory;
52  import org.sat4j.specs.ContradictionException;
53  import org.sat4j.specs.IVec;
54  import org.sat4j.specs.IVecInt;
55  
56  /**
57   * @author leberre To change the template for this generated type comment go to
58   *         Window>Preferences>Java>Code Generation>Code and Comments
59   */
60  public abstract class AbstractPBDataStructureFactory extends
61          AbstractDataStructureFactory implements PBDataStructureFactory {
62  
63      interface INormalizer {
64          PBContainer nice(IVecInt ps, IVec<BigInteger> bigCoefs,
65                  boolean moreThan, BigInteger bigDeg, ILits voc)
66                  throws ContradictionException;
67      }
68  
69      public static final INormalizer FOR_COMPETITION = new INormalizer() {
70  
71          public PBContainer nice(IVecInt literals, IVec<BigInteger> coefs,
72                  boolean moreThan, BigInteger degree, ILits voc)
73                  throws ContradictionException {
74              if (literals.size() != coefs.size()) {
75                  throw new IllegalArgumentException(
76                          "Number of coeff and literals are different!!!");
77              }
78              IVecInt cliterals = new VecInt(literals.size());
79              literals.copyTo(cliterals);
80              IVec<BigInteger> ccoefs = new Vec<BigInteger>(literals.size());
81              coefs.copyTo(ccoefs);
82              for (int i = 0; i < cliterals.size();) {
83                  if (ccoefs.get(i).equals(BigInteger.ZERO)) {
84                      cliterals.delete(i);
85                      ccoefs.delete(i);
86                  } else {
87                      i++;
88                  }
89              }
90              int[] theLits = new int[cliterals.size()];
91              cliterals.copyTo(theLits);
92              BigInteger[] normCoefs = new BigInteger[ccoefs.size()];
93              ccoefs.copyTo(normCoefs);
94              BigInteger degRes = Pseudos.niceParametersForCompetition(theLits,
95                      normCoefs, moreThan, degree);
96              return new PBContainer(theLits, normCoefs, degRes);
97  
98          }
99  
100     };
101 
102     public static final INormalizer NO_COMPETITION = new INormalizer() {
103 
104         public PBContainer nice(IVecInt literals, IVec<BigInteger> coefs,
105                 boolean moreThan, BigInteger degree, ILits voc)
106                 throws ContradictionException {
107             IDataStructurePB res = Pseudos.niceParameters(literals, coefs,
108                     moreThan, degree, voc);
109             int size = res.size();
110             int[] theLits = new int[size];
111             BigInteger[] theCoefs = new BigInteger[size];
112             res.buildConstraintFromMapPb(theLits, theCoefs);
113             BigInteger theDegree = res.getDegree();
114             return new PBContainer(theLits, theCoefs, theDegree);
115         }
116     };
117 
118     private INormalizer norm = FOR_COMPETITION;
119 
120     protected INormalizer getNormalizer() {
121         return this.norm;
122     }
123 
124     public void setNormalizer(String simp) {
125         Field f;
126         try {
127             f = AbstractPBDataStructureFactory.class.getDeclaredField(simp);
128             this.norm = (INormalizer) f.get(this);
129         } catch (Exception e) {
130             e.printStackTrace();
131             this.norm = FOR_COMPETITION;
132         }
133     }
134 
135     public void setNormalizer(INormalizer normalizer) {
136         this.norm = normalizer;
137     }
138 
139     /**
140 	 * 
141 	 */
142     private static final long serialVersionUID = 1L;
143 
144     public Constr createClause(IVecInt literals) throws ContradictionException {
145         IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), this.solver);
146         if (v == null) {
147             // tautological clause
148             return null;
149         }
150         if (v.size() == 1) {
151             return new UnitClause(v.last());
152         }
153         if (v.size() == 2) {
154             return OriginalBinaryClause.brandNewClause(this.solver,
155                     getVocabulary(), v);
156         }
157         return OriginalHTClause.brandNewClause(this.solver, getVocabulary(), v);
158     }
159 
160     public Constr createUnregisteredClause(IVecInt literals) {
161         if (literals.size() == 1) {
162             return new UnitClause(literals.last());
163         }
164         if (literals.size() == 2) {
165             return new LearntBinaryClause(literals, getVocabulary());
166         }
167         return new LearntHTClause(literals, getVocabulary());
168     }
169 
170     @Override
171     public Constr createCardinalityConstraint(IVecInt literals, int degree)
172             throws ContradictionException {
173         return AtLeastPB.atLeastNew(this.solver, getVocabulary(), literals,
174                 degree);
175     }
176 
177     public Constr createPseudoBooleanConstraint(IVecInt literals,
178             IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
179             throws ContradictionException {
180         PBContainer res = getNormalizer().nice(literals, coefs, moreThan,
181                 degree, getVocabulary());
182         return constraintFactory(res.lits, res.coefs, res.degree);
183     }
184 
185     public Constr createAtMostPBConstraint(IVecInt literals,
186             IVec<BigInteger> coefs, BigInteger degree)
187             throws ContradictionException {
188         return createPseudoBooleanConstraint(literals, coefs, false, degree);
189     }
190 
191     public Constr createAtLeastPBConstraint(IVecInt literals,
192             IVec<BigInteger> coefs, BigInteger degree)
193             throws ContradictionException {
194         return createPseudoBooleanConstraint(literals, coefs, true, degree);
195     }
196 
197     public Constr createUnregisteredPseudoBooleanConstraint(
198             IDataStructurePB dspb) {
199         return learntConstraintFactory(dspb);
200     }
201 
202     public Constr createUnregisteredAtLeastConstraint(IVecInt literals,
203             IVec<BigInteger> coefs, BigInteger degree) {
204         return learntAtLeastConstraintFactory(literals, coefs, degree);
205     }
206 
207     public Constr createUnregisteredAtMostConstraint(IVecInt literals,
208             IVec<BigInteger> coefs, BigInteger degree) {
209         return learntAtMostConstraintFactory(literals, coefs, degree);
210     }
211 
212     protected abstract Constr constraintFactory(int[] literals,
213             BigInteger[] coefs, BigInteger degree)
214             throws ContradictionException;
215 
216     protected abstract Constr learntConstraintFactory(IDataStructurePB dspb);
217 
218     protected abstract Constr learntAtLeastConstraintFactory(IVecInt literals,
219             IVec<BigInteger> coefs, BigInteger degree);
220 
221     protected abstract Constr learntAtMostConstraintFactory(IVecInt literals,
222             IVec<BigInteger> coefs, BigInteger degree);
223 
224     @Override
225     protected ILits createLits() {
226         return new Lits();
227     }
228 
229     @Override
230     public Constr createUnregisteredCardinalityConstraint(IVecInt literals,
231             int degree) {
232         return new AtLeast(getVocabulary(), literals, degree);
233     }
234 
235 }