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 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 *******************************************************************************/
28 package org.sat4j.tools;
29
30 import org.sat4j.core.VecInt;
31 import org.sat4j.specs.ContradictionException;
32 import org.sat4j.specs.ISolver;
33 import org.sat4j.specs.IVecInt;
34
35 /**
36 * Utility class to easily feed a SAT solver using logical gates.
37 *
38 * @author leberre
39 *
40 */
41 public class GateTranslator extends SolverDecorator<ISolver> {
42
43 /**
44 *
45 */
46 private static final long serialVersionUID = 1L;
47
48 public GateTranslator(ISolver solver) {
49 super(solver);
50 }
51
52 /**
53 * translate y <=> FALSE into a clause.
54 * @param y a variable to falsify
55 * @throws ContradictionException iff a trivial inconsistency is found.
56 */
57 public void gateFalse(int y)
58 throws ContradictionException {
59 IVecInt clause = new VecInt(2);
60 clause.push(-y);
61 processClause(clause);
62 }
63
64 /**
65 * translate y <=> TRUE into a clause.
66 * @param y a variable to verify
67 * @throws ContradictionException
68 */
69 public void gateTrue(int y)
70 throws ContradictionException {
71 IVecInt clause = new VecInt(2);
72 clause.push(y);
73 processClause(clause);
74 }
75
76 /**
77 * translate y <=> if x1 then x2 else x3 into clauses.
78 * @param y
79 * @param x1 the selector variable
80 * @param x2
81 * @param x3
82 * @throws ContradictionException
83 */
84 public void ite(int y, int x1, int x2, int x3) throws ContradictionException {
85 IVecInt clause = new VecInt(5);
86 // y <=> (x1 -> x2) and (not x1 -> x3)
87 // y -> (x1 -> x2) and (not x1 -> x3)
88 clause.push(-y).push(-x1).push(x2);
89 processClause(clause);
90 clause.clear();
91 clause.push(-y).push(x1).push(x3);
92 processClause(clause);
93 // y <- (x1 -> x2) and (not x1 -> x3)
94 // not(x1 -> x2) or not(not x1 -> x3) or y
95 // x1 and not x2 or not x1 and not x3 or y
96 // (x1 and not x2) or ((not x1 or y) and (not x3 or y))
97 // (x1 or not x1 or y) and (not x2 or not x1 or y) and (x1 or not x3 or
98 // y) and (not x2 or not x3 or y)
99 // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
100 clause.clear();
101 clause.push(-x1).push(-x2).push(y);
102 processClause(clause);
103 clause.clear();
104 clause.push(x1).push(-x3).push(y);
105 processClause(clause);
106 clause.clear();
107 clause.push(-x2).push(-x3).push(y);
108 processClause(clause);
109 // taken from Niklas Een et al SAT 2007 paper
110 // Adding the following redundant clause will improve unit propagation
111 // y -> x2 or x3
112 clause.clear();
113 clause.push(-y).push(x2).push(x3);
114 processClause(clause);
115 }
116
117 /**
118 * Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
119 *
120 * @param y
121 * @param literals the x1 ... xn literals.
122 * @throws ContradictionException
123 */
124 public void and(int y, IVecInt literals) throws ContradictionException {
125 // y <=> AND x1 ... xn
126
127 // y <= x1 .. xn
128 IVecInt clause = new VecInt(literals.size() + 2);
129 clause.push(y);
130 for (int i = 0; i < literals.size(); i++) {
131 clause.push(-literals.get(i));
132 }
133 processClause(clause);
134 clause.clear();
135 for (int i = 0; i < literals.size(); i++) {
136 // y => xi
137 clause.clear();
138 clause.push(-y);
139 clause.push(literals.get(i));
140 processClause(clause);
141 }
142 }
143
144 /**
145 * Translate y <=> x1 /\ x2
146 * @param y
147 * @param x1
148 * @param x2
149 * @throws ContradictionException
150 */
151 public void and(int y, int x1, int x2) throws ContradictionException {
152 IVecInt clause = new VecInt(4);
153 clause.push(-y);
154 clause.push(x1);
155 addClause(clause);
156 clause.clear();
157 clause.push(-y);
158 clause.push(x2);
159 addClause(clause);
160 clause.clear();
161 clause.push(y);
162 clause.push(-x1);
163 clause.push(-x2);
164 addClause(clause);
165 }
166
167 /**
168 * translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
169 *
170 * @param y
171 * @param literals
172 * @throws ContradictionException
173 */
174 public void or(int y, IVecInt literals) throws ContradictionException {
175 // y <=> OR x1 x2 ...xn
176 // y => x1 x2 ... xn
177 IVecInt clause = new VecInt(literals.size() + 2);
178 literals.copyTo(clause);
179 clause.push(-y);
180 processClause(clause);
181 clause.clear();
182 for (int i = 0; i < literals.size(); i++) {
183 // xi => y
184 clause.clear();
185 clause.push(y);
186 clause.push(-literals.get(i));
187 processClause(clause);
188 }
189 }
190
191 private void processClause(IVecInt clause) throws ContradictionException {
192 addClause(clause);
193 }
194
195 /**
196 * Translate y <=> not x into clauses.
197 *
198 * @param y
199 * @param x
200 * @throws ContradictionException
201 */
202 public void not(int y, int x) throws ContradictionException {
203 IVecInt clause = new VecInt(3);
204 // y <=> not x
205 // y => not x = not y or not x
206 clause.push(-y).push(-x);
207 processClause(clause);
208 // y <= not x = y or x
209 clause.clear();
210 clause.push(y).push(x);
211 processClause(clause);
212 }
213
214 /**
215 * translate y <=> x1 xor x2 xor ... xor xn into clauses.
216 * @param y
217 * @param literals
218 * @throws ContradictionException
219 */
220 public void xor(int y, IVecInt literals) throws ContradictionException {
221 literals.push(-y);
222 int[] f = new int[literals.size()];
223 literals.copyTo(f);
224 xor2Clause(f, 0, false);
225 }
226
227 /**
228 * translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
229 * @param y
230 * @param literals
231 * @throws ContradictionException
232 */
233 public void iff(int y, IVecInt literals) throws ContradictionException {
234 literals.push(y);
235 int[] f = new int[literals.size()];
236 literals.copyTo(f);
237 iff2Clause(f, 0, false);
238 }
239
240 private void xor2Clause(int[] f, int prefix, boolean negation)
241 throws ContradictionException {
242 if (prefix == f.length - 1) {
243 IVecInt clause = new VecInt(f.length + 1);
244 for (int i = 0; i < f.length - 1; ++i) {
245 clause.push(f[i]);
246 }
247 clause.push(f[f.length - 1] * (negation ? -1 : 1));
248 processClause(clause);
249 return;
250 }
251
252 if (negation) {
253 f[prefix] = -f[prefix];
254 xor2Clause(f, prefix + 1, false);
255 f[prefix] = -f[prefix];
256
257 xor2Clause(f, prefix + 1, true);
258 } else {
259 xor2Clause(f, prefix + 1, false);
260
261 f[prefix] = -f[prefix];
262 xor2Clause(f, prefix + 1, true);
263 f[prefix] = -f[prefix];
264 }
265 }
266
267 private void iff2Clause(int[] f, int prefix, boolean negation)
268 throws ContradictionException {
269 if (prefix == f.length - 1) {
270 IVecInt clause = new VecInt(f.length + 1);
271 for (int i = 0; i < f.length - 1; ++i) {
272 clause.push(f[i]);
273 }
274 clause.push(f[f.length - 1] * (negation ? -1 : 1));
275 processClause(clause);
276 return;
277 }
278
279 if (negation) {
280 iff2Clause(f, prefix + 1, false);
281 f[prefix] = -f[prefix];
282 iff2Clause(f, prefix + 1, true);
283 f[prefix] = -f[prefix];
284 } else {
285 f[prefix] = -f[prefix];
286 iff2Clause(f, prefix + 1, false);
287 f[prefix] = -f[prefix];
288 iff2Clause(f, prefix + 1, true);
289 }
290 }
291
292 }