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 pseudo boolean algorithms described in:
20  * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21  * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22  * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23  * 
24  * and 
25  * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL 
26  * Framework. Ph.D. Dissertation, University of Oregon.
27  *******************************************************************************/
28  
29  package org.sat4j.pb.constraints;
30  
31  import java.io.FileNotFoundException;
32  import java.io.IOException;
33  
34  import org.sat4j.pb.IPBSolver;
35  import org.sat4j.pb.reader.PBInstanceReader;
36  import org.sat4j.reader.InstanceReader;
37  import org.sat4j.reader.ParseFormatException;
38  
39  /**
40   * @author leberre
41   * 
42   * Those pseudo boolean problems were kindly provided by Niklas Een.
43   * 
44   */
45  public abstract class AbstractEZPseudoBooleanAndPigeonHoleTest extends
46          AbstractPigeonHoleWithCardinalityTest<IPBSolver> {
47  
48      /**
49       * Cr?ation d'un test
50       * 
51       * @param arg
52       *            argument ?ventuel
53       */
54      public AbstractEZPseudoBooleanAndPigeonHoleTest(String arg) {
55          super(arg);
56      }
57  
58      @Override
59      protected InstanceReader createInstanceReader(IPBSolver theSolver1){
60      	return new PBInstanceReader(theSolver1);
61      }
62      
63      @Override
64      protected void tearDown() {
65          super.tearDown();
66      }
67  
68  
69      // VASCO: traveling tournament problem
70      public void testncirc43() throws FileNotFoundException, IOException,
71              ParseFormatException {
72          assertTrue(solveInstance(PREFIX
73                  + "normalized-opb/submitted/manquinho/ttp/normalized-circ4_3.opb"));
74      }
75  
76      public void testncirc63() throws FileNotFoundException, IOException,
77              ParseFormatException {
78          assertTrue(solveInstance(PREFIX
79                  + "normalized-opb/submitted/manquinho/ttp/normalized-circ6_3.opb"));
80      }
81  
82      public void testncirc83() throws FileNotFoundException, IOException,
83              ParseFormatException {
84          assertTrue(solveInstance(PREFIX
85                  + "normalized-opb/submitted/manquinho/ttp/normalized-circ8_3.opb"));
86      }
87  
88  
89      public void testndata43() throws FileNotFoundException, IOException,
90              ParseFormatException {
91          assertTrue(solveInstance(PREFIX
92                  + "normalized-opb/submitted/manquinho/ttp/normalized-data4_3.opb"));
93      }
94  
95      public void testndata63() throws FileNotFoundException, IOException,
96              ParseFormatException {
97          assertTrue(solveInstance(PREFIX
98                  + "normalized-opb/submitted/manquinho/ttp/normalized-data6_3.opb"));
99      }
100 
101     public void testndata83() throws FileNotFoundException, IOException,
102             ParseFormatException {
103         assertTrue(solveInstance(PREFIX
104                 + "normalized-opb/submitted/manquinho/ttp/normalized-data8_3.opb"));
105     }
106 
107 
108     public void testn9symml() throws FileNotFoundException, IOException,
109             ParseFormatException {
110         assertTrue(solveInstance(PREFIX
111                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-9symml.opb"));
112     }
113 
114     public void testnC17() throws FileNotFoundException, IOException,
115             ParseFormatException {
116         assertTrue(solveInstance(PREFIX
117                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-C17.opb"));
118     }
119 
120     public void testnC432() throws FileNotFoundException, IOException,
121             ParseFormatException {
122         assertTrue(solveInstance(PREFIX
123                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-C432.opb"));
124     }
125 
126     public void testnb1() throws FileNotFoundException, IOException,
127             ParseFormatException {
128         assertTrue(solveInstance(PREFIX
129                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-b1.opb"));
130     }
131 
132     public void testnc8() throws FileNotFoundException, IOException,
133             ParseFormatException {
134         assertTrue(solveInstance(PREFIX
135                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-c8.opb"));
136     }
137 
138     public void testncc() throws FileNotFoundException, IOException,
139             ParseFormatException {
140         assertTrue(solveInstance(PREFIX
141                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cc.opb"));
142     }
143 
144     public void testncm42a() throws FileNotFoundException, IOException,
145             ParseFormatException {
146         assertTrue(solveInstance(PREFIX
147                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cm42a.opb"));
148     }
149 
150     public void testncmb() throws FileNotFoundException, IOException,
151             ParseFormatException {
152         assertTrue(solveInstance(PREFIX
153                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb"));
154     }
155 
156     public void testnmux() throws FileNotFoundException, IOException,
157             ParseFormatException {
158         assertTrue(solveInstance(PREFIX
159                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-mux.opb"));
160     }
161 
162     public void testnmyadder() throws FileNotFoundException, IOException,
163             ParseFormatException {
164         assertTrue(solveInstance(PREFIX
165                 + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-my_adder.opb"));
166     }
167 }