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.pb;
31
32 import java.math.BigInteger;
33
34 import org.sat4j.minisat.core.ILits;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.UnitPropagationListener;
37
38 public final class PuebloMinWatchPb extends MinWatchPb {
39
40 private static final long serialVersionUID = 1L;
41
42 /**
43 * Constructeur de base des contraintes
44 *
45 * @param voc
46 * Informations sur le vocabulaire employ???
47 * @param ps
48 * Liste des litt???raux
49 * @param weightedLits
50 * Liste des coefficients
51 * @param moreThan
52 * Indication sur le comparateur
53 * @param degree
54 * Stockage du degr??? de la contrainte
55 */
56 private PuebloMinWatchPb(ILits voc, int[] lits, BigInteger[] coefs,
57 BigInteger degree, BigInteger sumCoefs) {
58 super(voc, lits, coefs, degree, sumCoefs);
59 }
60
61 private PuebloMinWatchPb(ILits voc, IDataStructurePB mpb) {
62
63 super(voc, mpb);
64 }
65
66 /**
67 * @param s
68 * a unit propagation listener
69 * @param voc
70 * the vocabulary
71 * @param lits
72 * the literals
73 * @param coefs
74 * the coefficients
75 * @param degree
76 * the degree of the constraint to normalize.
77 * @return a new PB constraint or null if a trivial inconsistency is
78 * detected.
79 */
80 public static PuebloMinWatchPb normalizedMinWatchPbNew(
81 UnitPropagationListener s, ILits voc, int[] lits,
82 BigInteger[] coefs, BigInteger degree)
83 throws ContradictionException {
84 // Il ne faut pas modifier les param?tres
85 BigInteger sumCoefs = BigInteger.ZERO;
86 for (BigInteger c : coefs) {
87 sumCoefs = sumCoefs.add(c);
88 }
89 PuebloMinWatchPb outclause = new PuebloMinWatchPb(voc, lits, coefs,
90 degree, sumCoefs);
91
92 if (outclause.degree.signum() <= 0) {
93 return null;
94 }
95
96 outclause.computeWatches();
97
98 outclause.computePropagation(s);
99
100 return outclause;
101
102 }
103
104 public static WatchPb normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) {
105 return new PuebloMinWatchPb(voc, mpb);
106 }
107
108 @Override
109 protected BigInteger maximalCoefficient(int pIndice) {
110 return this.coefs[0];
111 }
112
113 @Override
114 protected BigInteger updateWatched(BigInteger mc, int pIndice) {
115 BigInteger maxCoef = mc;
116 if (this.watchingCount < size()) {
117 BigInteger upWatchCumul = this.watchCumul
118 .subtract(this.coefs[pIndice]);
119 BigInteger borneSup = this.degree.add(maxCoef);
120 for (int ind = 0; ind < this.lits.length
121 && upWatchCumul.compareTo(borneSup) < 0; ind++) {
122 if (!this.voc.isFalsified(this.lits[ind]) && !this.watched[ind]) {
123 upWatchCumul = upWatchCumul.add(this.coefs[ind]);
124 this.watched[ind] = true;
125 assert this.watchingCount < size();
126 this.watching[this.watchingCount++] = ind;
127 this.voc.watch(this.lits[ind] ^ 1, this);
128 }
129 }
130 this.watchCumul = upWatchCumul.add(this.coefs[pIndice]);
131 }
132 return maxCoef;
133 }
134
135 }