View Javadoc

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.reader;
29  
30  import java.io.IOException;
31  import java.io.PrintWriter;
32  import java.util.Scanner;
33  
34  import org.sat4j.core.VecInt;
35  import org.sat4j.specs.ContradictionException;
36  import org.sat4j.specs.IProblem;
37  import org.sat4j.specs.ISolver;
38  import org.sat4j.specs.IVecInt;
39  import org.sat4j.tools.GateTranslator;
40  
41  /**
42   * Reader for the ASCII And Inverter Graph format defined by Armin Biere.
43   * 
44   * @author daniel
45   *
46   */
47  public class AAGReader extends Reader {
48  
49      private final static int FALSE = 0;
50  
51      private final static int TRUE = 1;
52  
53      private final GateTranslator solver;
54  
55      private int maxvarid;
56  
57      private int nbinputs;
58  
59      AAGReader(ISolver s) {
60          solver = new GateTranslator(s);
61      }
62  
63      @Override
64      public String decode(int[] model) {
65          StringBuffer stb = new StringBuffer();
66          for (int i = 0; i < nbinputs; i++) {
67              stb.append(model[i]>0?1:0);
68          }
69          return stb.toString();
70      }
71  
72      @Override
73      public void decode(int[] model, PrintWriter out) {
74          for (int i = 0; i < nbinputs; i++) {
75              out.print(model[i]>0?1:0);
76          }
77      }
78  
79      @Override
80      public IProblem parseInstance(java.io.Reader in)
81              throws ParseFormatException, ContradictionException, IOException {
82          Scanner scanner = new Scanner(in);
83          String prefix = scanner.next();
84          if (!"aag".equals(prefix)) {
85              throw new ParseFormatException("AAG format only!");
86          }
87          maxvarid = scanner.nextInt();
88          nbinputs = scanner.nextInt();
89          int nblatches = scanner.nextInt();
90          int nboutputs = scanner.nextInt();
91          if (nboutputs > 1) {
92              throw new ParseFormatException(
93                      "CNF conversion allowed for single output circuit only!");
94          }
95          int nbands = scanner.nextInt();
96          solver.newVar(maxvarid + 1);
97          solver.setExpectedNumberOfClauses(3 * nbands + 2);
98          readInput(nbinputs, scanner);
99          assert nblatches==0;
100         if (nboutputs > 0) {
101             int output0 = readOutput(nboutputs, scanner);
102             readAnd(nbands, output0, scanner);
103         }
104         return solver;
105     }
106 
107     private void readAnd(int nbands, int output0, Scanner scanner)
108             throws ContradictionException {
109         
110         for (int i = 0; i < nbands; i++) {
111             int lhs = scanner.nextInt();
112             int rhs0 = scanner.nextInt();
113             int rhs1 = scanner.nextInt();
114             solver.and(toDimacs(lhs), toDimacs(rhs0), toDimacs(rhs1));
115         }
116         solver.gateTrue(maxvarid + 1);
117         solver.gateTrue(toDimacs(output0));
118     }
119 
120     private int toDimacs(int v) {
121         if (v == FALSE) {
122             return -(maxvarid + 1);
123         }
124         if (v == TRUE) {
125             return maxvarid + 1;
126         }
127         int var = v >> 1;
128         if ((v & 1) == 0) {
129             return var;
130         }
131         return -var;
132     }
133 
134     private int readOutput(int nboutputs, Scanner scanner) {
135         IVecInt outputs = new VecInt(nboutputs);
136         for (int i = 0; i < nboutputs; i++) {
137             outputs.push(scanner.nextInt());
138         }
139         return outputs.get(0);
140     }
141 
142 
143     private IVecInt readInput(int numberOfInputs, Scanner scanner) {
144         IVecInt inputs = new VecInt(numberOfInputs);
145         for (int i = 0; i < numberOfInputs; i++) {
146             inputs.push(scanner.nextInt());
147         }
148         return inputs;
149     }
150 
151 }