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.pb;
29
30 import java.math.BigInteger;
31
32 import org.sat4j.minisat.constraints.card.MinWatchCard;
33 import org.sat4j.minisat.core.ILits;
34 import org.sat4j.minisat.core.UnitPropagationListener;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IVecInt;
37
38 public final class MinWatchCardPB extends MinWatchCard implements PBConstr {
39
40 /**
41 *
42 */
43 private static final long serialVersionUID = 1L;
44
45 private final BigInteger bigDegree;
46
47 public MinWatchCardPB(ILits voc, IVecInt ps, boolean moreThan, int degree) {
48 super(voc, ps, moreThan, degree);
49 // this.degree has been computed in the superclass constructor.
50 this.bigDegree = BigInteger.valueOf(this.degree);
51 }
52
53 public MinWatchCardPB(ILits voc, IVecInt ps, int degree) {
54 super(voc, ps, degree);
55 this.bigDegree = BigInteger.valueOf(this.degree);
56 }
57
58 /*
59 * (non-Javadoc)
60 *
61 * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefficient(int)
62 */
63 public BigInteger getCoef(int literal) {
64 return BigInteger.ONE;
65 }
66
67 /*
68 * (non-Javadoc)
69 *
70 * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
71 */
72 public BigInteger getDegree() {
73 return bigDegree;
74 }
75
76 public BigInteger[] getCoefs() {
77 BigInteger[] tmp = new BigInteger[size()];
78 for (int i = 0; i < tmp.length; i++)
79 tmp[i] = BigInteger.ONE;
80 return tmp;
81 }
82
83 /**
84 * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
85 *
86 * @param s
87 * outil pour la propagation des litt?raux
88 * @param voc
89 * vocabulaire utilis? par la contrainte
90 * @param ps
91 * liste des litt?raux de la nouvelle contrainte
92 * @param degree
93 * fournit le degr? de la contrainte
94 * @return une nouvelle clause si tout va bien, null sinon
95 * @throws ContradictionException
96 */
97 public static MinWatchCardPB normalizedMinWatchCardPBNew(
98 UnitPropagationListener s, ILits voc, IVecInt ps, int degree)
99 throws ContradictionException {
100 return minWatchCardPBNew(s, voc, ps, ATLEAST, degree, true);
101 }
102
103 /**
104 * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
105 *
106 * @param s
107 * outil pour la propagation des litt?raux
108 * @param voc
109 * vocabulaire utilis? par la contrainte
110 * @param ps
111 * liste des litt?raux de la nouvelle contrainte
112 * @param moreThan
113 * d?termine si c'est une sup?rieure ou ?gal ? l'origine
114 * @param degree
115 * fournit le degr? de la contrainte
116 * @return une nouvelle clause si tout va bien, null sinon
117 * @throws ContradictionException
118 */
119 public static MinWatchCardPB minWatchCardPBNew(UnitPropagationListener s,
120 ILits voc, IVecInt ps, boolean moreThan, int degree)
121 throws ContradictionException {
122 return minWatchCardPBNew(s, voc, ps, moreThan, degree, false);
123 }
124
125 private static MinWatchCardPB minWatchCardPBNew(UnitPropagationListener s,
126 ILits voc, IVecInt ps, boolean moreThan, int degree,
127 boolean normalized) throws ContradictionException {
128 int mydegree = degree + linearisation(voc, ps);
129
130 if (ps.size() == 0 && mydegree > 0) {
131 throw new ContradictionException();
132 } else if (ps.size() == mydegree || ps.size() <= 0) {
133 for (int i = 0; i < ps.size(); i++)
134 if (!s.enqueue(ps.get(i))) {
135 throw new ContradictionException();
136 }
137 return null;
138 }
139
140 // constraint is now instanciated
141 MinWatchCardPB retour = null;
142 if (normalized)
143 retour = new MinWatchCardPB(voc, ps, mydegree);
144 else
145 retour = new MinWatchCardPB(voc, ps, moreThan, mydegree);
146
147 if (retour.bigDegree.signum() <= 0)
148 return null;
149
150 retour.computeWatches();
151
152 return ((MinWatchCardPB) retour.computePropagation(s));
153 }
154
155 /**
156 *
157 */
158 private boolean learnt = false;
159
160 /**
161 * D?termine si la contrainte est apprise
162 *
163 * @return true si la contrainte est apprise, false sinon
164 * @see org.sat4j.specs.IConstr#learnt()
165 */
166 @Override
167 public boolean learnt() {
168 return learnt;
169 }
170
171 @Override
172 public void setLearnt() {
173 learnt = true;
174 }
175
176 @Override
177 public void register() {
178 assert learnt;
179 computeWatches();
180 }
181
182 @Override
183 public void assertConstraint(UnitPropagationListener s) {
184 for (int i = 0; i < size(); i++) {
185 if (getVocabulary().isUnassigned(get(i))) {
186 boolean ret = s.enqueue(get(i), this);
187 assert ret;
188 }
189 }
190 }
191
192 public IVecInt computeAnImpliedClause() {
193 return null;
194 }
195
196 }