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.IVecInt;
30  
31  /**
32   * Converter from the Extended Dimacs format proposed by Fahiem Bacchus and Toby
33   * Walsh in array representation (without the terminating 0) to the Dimacs
34   * format.
35   * 
36   * Adaptation of org.sat4j.reader.ExtendedDimacsReader.
37   * 
38   * @author leberre
39   * @author fuhs
40   */
41  public class ExtendedDimacsArrayToDimacsConverter extends
42          DimacsArrayToDimacsConverter {
43  
44      public static final int FALSE = 1;
45  
46      public static final int TRUE = 2;
47  
48      public static final int NOT = 3;
49  
50      public static final int AND = 4;
51  
52      public static final int NAND = 5;
53  
54      public static final int OR = 6;
55  
56      public static final int NOR = 7;
57  
58      public static final int XOR = 8;
59  
60      public static final int XNOR = 9;
61  
62      public static final int IMPLIES = 10;
63  
64      public static final int IFF = 11;
65  
66      public static final int IFTHENELSE = 12;
67  
68      public static final int ATLEAST = 13;
69  
70      public static final int ATMOST = 14;
71  
72      public static final int COUNT = 15;
73  
74      private static final long serialVersionUID = 1L;
75  
76      public ExtendedDimacsArrayToDimacsConverter(int bufSize) {
77          super(bufSize);
78      }
79  
80      /**
81       * Handles a single constraint (constraint == Extended Dimacs circuit gate).
82       * 
83       * @param gateType
84       *            the type of the gate in question
85       * @param output
86       *            the number of the output of the gate in question
87       * @param inputs
88       *            the numbers of the inputs of the gates in question
89       * @return true
90       */
91      @Override
92      protected boolean handleConstr(int gateType, int output, int[] inputs)
93              throws ContradictionException {
94          IVecInt literals = new VecInt(inputs);
95          switch (gateType) {
96          case FALSE:
97              gateFalse(output, literals);
98              break;
99          case TRUE:
100             gateTrue(output, literals);
101             break;
102         case OR:
103             or(output, literals);
104             break;
105         case NOT:
106             not(output, literals);
107             break;
108         case AND:
109             and(output, literals);
110             break;
111         case XOR:
112             xor(output, literals);
113             break;
114         case IFF:
115             iff(output, literals);
116             break;
117         case IFTHENELSE:
118             ite(output, literals);
119             break;
120         default:
121             throw new UnsupportedOperationException("Gate type " + gateType
122                     + " not handled yet");
123         }
124         return true;
125     }
126 
127     private void gateFalse(int y, IVecInt literals)
128             throws ContradictionException {
129         assert literals.size() == 0;
130         IVecInt clause = new VecInt(1);
131         clause.push(-y);
132         processClause(clause);
133     }
134 
135     private void gateTrue(int y, IVecInt literals)
136             throws ContradictionException {
137         assert literals.size() == 0;
138         IVecInt clause = new VecInt(1);
139         clause.push(y);
140         processClause(clause);
141     }
142 
143     private void ite(int y, IVecInt literals) throws ContradictionException {
144         assert literals.size() == 3;
145         IVecInt clause = new VecInt(2);
146         // y <=> (x1 -> x2) and (not x1 -> x3)
147         // y -> (x1 -> x2) and (not x1 -> x3)
148         clause.push(-y).push(-literals.get(0)).push(literals.get(1));
149         processClause(clause);
150         clause.clear();
151         clause.push(-y).push(literals.get(0)).push(literals.get(2));
152         processClause(clause);
153         // y <- (x1 -> x2) and (not x1 -> x3)
154         // not(x1 -> x2) or not(not x1 -> x3) or y
155         // x1 and not x2 or not x1 and not x3 or y
156         // (x1 and not x2) or ((not x1 or y) and (not x3 or y))
157         // (x1 or not x1 or y) and (not x2 or not x1 or y) and (x1 or not x3 or
158         // y) and (not x2 or not x3 or y)
159         // not x1 or not x2 or y and x1 or not x3 or y and not x2 or not x3 or y
160         clause.clear();
161         clause.push(-literals.get(0)).push(-literals.get(1)).push(y);
162         processClause(clause);
163         clause.clear();
164         clause.push(literals.get(0)).push(-literals.get(2)).push(y);
165         processClause(clause);
166         clause.clear();
167         clause.push(-literals.get(1)).push(-literals.get(2)).push(y);
168         processClause(clause);
169     }
170 
171     private void and(int y, IVecInt literals) throws ContradictionException {
172         // y <=> AND x1 ... xn
173 
174         // y <= x1 .. xn
175         IVecInt clause = new VecInt(literals.size() + 1);
176         clause.push(y);
177         for (int i = 0; i < literals.size(); i++) {
178             clause.push(-literals.get(i));
179         }
180         processClause(clause);
181         clause.clear();
182         for (int i = 0; i < literals.size(); i++) {
183             // y => xi
184             clause.clear();
185             clause.push(-y);
186             clause.push(literals.get(i));
187             processClause(clause);
188         }
189     }
190 
191     private void or(int y, IVecInt literals) throws ContradictionException {
192         // y <=> OR x1 x2 ...xn
193         // y => x1 x2 ... xn
194         IVecInt clause = new VecInt(literals.size() + 1);
195         literals.copyTo(clause);
196         clause.push(-y);
197         processClause(clause);
198         clause.clear();
199         for (int i = 0; i < literals.size(); i++) {
200             // xi => y
201             clause.clear();
202             clause.push(y);
203             clause.push(-literals.get(i));
204             processClause(clause);
205         }
206     }
207 
208     private void processClause(IVecInt clause) throws ContradictionException {
209         final int length = clause.size();
210         for (int i = 0; i < length; ++i) {
211             this.dimacs.append(clause.get(i));
212             this.dimacs.append(" ");
213         }
214         this.dimacs.append("0\n");
215         ++this.clauses;
216     }
217 
218     private void not(int y, IVecInt literals) throws ContradictionException {
219         assert literals.size() == 1;
220         IVecInt clause = new VecInt(2);
221         // y <=> not x
222         // y => not x = not y or not x
223         clause.push(-y).push(-literals.get(0));
224         processClause(clause);
225         // y <= not x = y or x
226         clause.clear();
227         clause.push(y).push(literals.get(0));
228         processClause(clause);
229     }
230 
231     void xor(int y, IVecInt literals) throws ContradictionException {
232         literals.push(-y);
233         int[] f = new int[literals.size()];
234         literals.copyTo(f);
235         xor2Clause(f, 0, false);
236     }
237 
238     void iff(int y, IVecInt literals) throws ContradictionException {
239         literals.push(y);
240         int[] f = new int[literals.size()];
241         literals.copyTo(f);
242         iff2Clause(f, 0, false);
243     }
244 
245     void xor2Clause(int[] f, int prefix, boolean negation)
246             throws ContradictionException {
247         if (prefix == f.length - 1) {
248             IVecInt clause = new VecInt(f.length);
249             for (int i = 0; i < f.length - 1; ++i) {
250                 clause.push(f[i]);
251             }
252             clause.push(f[f.length - 1] * (negation ? -1 : 1));
253             processClause(clause);
254             return;
255         }
256 
257         if (negation) {
258             f[prefix] = -f[prefix];
259             xor2Clause(f, prefix + 1, false);
260             f[prefix] = -f[prefix];
261 
262             xor2Clause(f, prefix + 1, true);
263         } else {
264             xor2Clause(f, prefix + 1, false);
265 
266             f[prefix] = -f[prefix];
267             xor2Clause(f, prefix + 1, true);
268             f[prefix] = -f[prefix];
269         }
270     }
271 
272     void iff2Clause(int[] f, int prefix, boolean negation)
273             throws ContradictionException {
274         if (prefix == f.length - 1) {
275             IVecInt clause = new VecInt(f.length);
276             for (int i = 0; i < f.length - 1; ++i) {
277                 clause.push(f[i]);
278             }
279             clause.push(f[f.length - 1] * (negation ? -1 : 1));
280             processClause(clause);
281             return;
282         }
283 
284         if (negation) {
285             iff2Clause(f, prefix + 1, false);
286             f[prefix] = -f[prefix];
287             iff2Clause(f, prefix + 1, true);
288             f[prefix] = -f[prefix];
289         } else {
290             f[prefix] = -f[prefix];
291             iff2Clause(f, prefix + 1, false);
292             f[prefix] = -f[prefix];
293             iff2Clause(f, prefix + 1, true);
294         }
295     }
296 
297 }