1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23 *
24 */
25 package org.sat4j.minisat.constraints.pb;
26
27 import java.math.BigInteger;
28
29 import org.sat4j.minisat.constraints.card.MinWatchCard;
30 import org.sat4j.minisat.core.ILits;
31 import org.sat4j.minisat.core.UnitPropagationListener;
32 import org.sat4j.specs.ContradictionException;
33 import org.sat4j.specs.IVecInt;
34
35 public class MinWatchCardPB extends MinWatchCard implements PBConstr {
36
37 /**
38 *
39 */
40 private static final long serialVersionUID = 1L;
41
42 private final BigInteger degree;
43
44 public MinWatchCardPB(ILits voc, IVecInt ps, boolean moreThan, int degree) {
45 super(voc, ps, moreThan, degree);
46 this.degree = BigInteger.valueOf(degree);
47 }
48
49 public MinWatchCardPB(ILits voc, IVecInt ps, int degree) {
50 super(voc, ps, degree);
51 this.degree = BigInteger.valueOf(degree);
52 }
53
54 /*
55 * (non-Javadoc)
56 *
57 * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefficient(int)
58 */
59 public BigInteger getCoef(int literal) {
60 return BigInteger.ONE;
61 }
62
63 /*
64 * (non-Javadoc)
65 *
66 * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
67 */
68 public BigInteger getDegree() {
69 return degree;
70 }
71
72 public BigInteger[] getCoefs() {
73 BigInteger[] tmp = new BigInteger[size()];
74 for (int i = 0; i < tmp.length; i++)
75 tmp[i] = BigInteger.ONE;
76 return tmp;
77 }
78
79 /**
80 * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
81 *
82 * @param s
83 * outil pour la propagation des litt?raux
84 * @param voc
85 * vocabulaire utilis? par la contrainte
86 * @param ps
87 * liste des litt?raux de la nouvelle contrainte
88 * @param degree
89 * fournit le degr? de la contrainte
90 * @return une nouvelle clause si tout va bien, null sinon
91 * @throws ContradictionException
92 */
93 public static MinWatchCardPB normalizedMinWatchCardPBNew(
94 UnitPropagationListener s, ILits voc, IVecInt ps, int degree)
95 throws ContradictionException {
96 return minWatchCardPBNew(s, voc, ps, ATLEAST, degree, true);
97 }
98
99 /**
100 * Permet la cr?ation de contrainte de cardinalit? ? observation minimale
101 *
102 * @param s
103 * outil pour la propagation des litt?raux
104 * @param voc
105 * vocabulaire utilis? par la contrainte
106 * @param ps
107 * liste des litt?raux de la nouvelle contrainte
108 * @param moreThan
109 * d?termine si c'est une sup?rieure ou ?gal ? l'origine
110 * @param degree
111 * fournit le degr? de la contrainte
112 * @return une nouvelle clause si tout va bien, null sinon
113 * @throws ContradictionException
114 */
115 public static MinWatchCardPB minWatchCardPBNew(UnitPropagationListener s,
116 ILits voc, IVecInt ps, boolean moreThan, int degree)
117 throws ContradictionException {
118 return minWatchCardPBNew(s, voc, ps, moreThan, degree, false);
119 }
120
121 private static MinWatchCardPB minWatchCardPBNew(UnitPropagationListener s,
122 ILits voc, IVecInt ps, boolean moreThan, int degree,
123 boolean normalized) throws ContradictionException {
124 int mydegree = degree + linearisation(voc, ps);
125
126 if (ps.size() == 0 && mydegree > 0) {
127 throw new ContradictionException();
128 } else if (ps.size() == mydegree || ps.size() <= 0) {
129 for (int i = 0; i < ps.size(); i++)
130 if (!s.enqueue(ps.get(i))) {
131 throw new ContradictionException();
132 }
133 return null;
134 }
135
136 // constraint is now instanciated
137 MinWatchCardPB retour = null;
138 if (normalized)
139 retour = new MinWatchCardPB(voc, ps, mydegree);
140 else
141 retour = new MinWatchCardPB(voc, ps, moreThan, mydegree);
142
143 if (retour.degree.signum() <= 0)
144 return null;
145
146 retour.computeWatches();
147
148 return ((MinWatchCardPB) retour.computePropagation(s));
149 }
150
151 /**
152 *
153 */
154 private boolean learnt = false;
155
156 /**
157 * D?termine si la contrainte est apprise
158 *
159 * @return true si la contrainte est apprise, false sinon
160 * @see org.sat4j.specs.IConstr#learnt()
161 */
162 @Override
163 public boolean learnt() {
164 return learnt;
165 }
166
167 @Override
168 public void setLearnt() {
169 learnt = true;
170 }
171
172 @Override
173 public void register() {
174 assert learnt;
175 computeWatches();
176 }
177
178 @Override
179 public void assertConstraint(UnitPropagationListener s) {
180 for (int i = 0; i < size(); i++) {
181 if (getVocabulary().isUnassigned(get(i))) {
182 boolean ret = s.enqueue(get(i), this);
183 assert ret;
184 }
185 }
186 }
187
188 public IVecInt computeAnImpliedClause() {
189 return null;
190 }
191
192 }