View Javadoc

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