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