The following x86-linux executables are available for non-commercial use only. siege takes one or two arguments, (first) the filename of a DIMACS-format CNF, and optionally (second) a seed for the random number generator. For example, "siege_v4 7pipe.cnf 666". If a seed is not given, the system time is used. Certificates, etc., are appended to a file, "siege.results".
siege (variant 4) - new resolution strategy; far more powerful
siege (variant 3) - different decision strategy (too greedy)
siege (variant 1) - cleaned-up version of the late entry to SAT 2003 (first round: 3rd place industrial, 1st place handmade)
Lawrence Ryan authored siege. He published version 4 of the solver in August of 2003. About two weeks later, he started working full-time for Synopsys in California. Lawrence no longer reads the mail sent to his SFU email addresses.
May 12, 2004: because of the anti-blackbox rule, siege did not participate in the SAT 2004 competition.
September 1, 2003: updated v4 to remove the "c3 overflow" limitation.
August 29, 2003: removed Sun executables. Added x86-linux build of v1. Released siege_v4. Please alert me if you find a bug. Note that v4 may use substantially more memory than v3. And, as in v3, the decision strategy is too greedy. This will be addressed in v5.
June 26, 2003: the x86-linux version of siege_v3 became 5-10% faster.
M. Büttner and J. Rintanen, Satisfiability Planning with Constraints on the Number of Actions, Proceedings of the 15th International Conference on Automated Planning and Scheduling, pp. 292-299, AAAI Press, 2005.
P. Manolios and S.K. Srinivasan, A Computationally Efficient Method Based on Commitment Refinement Maps for Verifying Pipelined Machines, ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE '05), 2005.
P. Manolios and S.K. Srinivasan, A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems, the 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME '05), 2005.
P. Manolios and S.K. Srinivasan, Refinement Maps for Efficient Verification of Processor Models, Design, Automation, and Test in Europe (DATE '05), 2005.
P. Manolios and S.K. Srinivasan, A Suite of Hard ACL2 Theorems Arising in Refinement-Based Processor Verification, Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '04), 2004.
E. Zarpas, M. Roveri, A. Cimatti, K. Winkelmann, R. Brinkmann, Y. Novikov, O. Shacham, M. Farkash, Improved Decision Heuristics for High Performance SAT Based Static Property Checking, research report, 2005.
I.P. Gent and I. Lynce, A SAT Encoding for the Social Golfer Problem, IJCAI '05 workshop on Modelling and Solving Problems with Constraints, July 2005.
K. Cao and P. Dhawan and J. Hu, Library Cell Layout with Alt-PSM Compliance and Composability, Proceedings of the Asia and South Pacific Design Automation Conference, pp. 216-219, 2005.
Gianpiero Cabodi and Sergio Nocco and Stefano Quer, Improving SAT-based Bounded Model Checking by Means of BDD-based Approximate Traversals, Journal of Universal Computer Science, vol. 10, no. 12, pp. 1693-1730, 2004.
Feng Lu and Li-C. Wang and Kwang-Ting Cheng and John Moondanos and Ziyad Hanna, A Signal Correlation Guided Circuit-SAT Solver, Journal of Universal Computer Science, vol. 10, no. 12, pp. 1629-1654, 2004.
Daniel Le Berre et al., SAT4J: a satisfiability library for Java.
H. Kautz and D. Roznyai and F. Teydaye-Saheli and S.J. Neph and M. Lindmark, SatPlan 2004 (overview).
V. Ganapathy and S.A. Seshia and S. Jha and T.W. Reps and R.E. Bryant, Automatic Discovery of API-level Exploits, University of Wisconsin-Madison, Computer Sciences, Technical Report 1512, July 2004.
C. Ansotegui and F. Manya, Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables, The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT '04), May 2004.
E. Zarpas, siege vs. zChaff and Berkmin561 on BMC Formulas from the IBM Formal Verification Benchmarks Library, July 2004.
J. Rintanen, Evaluation Strategies for Planning as Satisfiability, Proceedings of the 16th European Conference on Artificial Intelligence (ECAI 2004), IOS Press, 2004.
J. Rintanen, Phase Transitions in Classical Planning: an Experimental Study, Principles of Knowledge Representation and Reasoning: Proceedings of the Ninth International Conference (KR 2004), AAAI Press, 2004.
S. Subbarayan and D. Pradhan, NiVER: Non Increasing Variable Elimination Resolution, The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT '04), May 2004.
P. Manolios and S.K. Srinivasan, Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB-Refinements, Design, Automation and Test in Europe (DATE '04), February 2004.
M.N. Velev, Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors, Design, Automation and Test in Europe (DATE '04), February 2004.
M.N. Velev, Using Positive Equality to Prove Liveness for Pipelined Microprocessors, Asia and South Pacific Design Automation Conference (ASP-DAC '04), January 2004.
M.N. Velev, Efficient Translation of Boolean Formulas to CNF in Formal Verification of Microprocessors, Asia and South Pacific Design Automation Conference (ASP-DAC '04), January 2004.
M.N. Velev, Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-Solver When Formally Verifying Out-of-Order Processors, Artificial Intelligence and Mathematics (AI&MATH '04), January 2004.
J. Rintanen and K. Heljanko and I. Niemelä, Parallel Encodings of Classical Planning as Satisfiability, Logics in Artificial Intelligence, European Conference (JELIA 2004), Lecture Notes in Computer Science, Springer-Verlag, 2004.
M.N. Velev, Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs, International Test Conference (ITC '03), October 2003, pp. 138-147.
M.N. Velev, Automatic Abstraction of Equations in a Logic of Equality, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '03), M.C. Mayer, and F. Pirri, eds., LNAI 2796, Springer-Verlag, September 2003, pp. 196-213.
P. Manolios and S.K. Srinivasan, Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB-Refinements, CERCS TR# GIT-CERCS-03-17, September 2003.
L. Ryan, Efficient Algorithms for Clause-Learning SAT Solvers, M.Sc. Thesis, the psychedelic summer of 2003.
Listed below are runtimes for siege_v4, given seed 123456789. Host has a 2.79 GHz Intel Xeon with 512 KB of L2 cache, and 4 GB of main memory. The leftmost column is runtime, in seconds, rounded up to the nearest integer. The middle column indicates the satisfiability result proved by the solver. A "?" in this column denotes failure to achieve a proof in reasonable time (~24 hours). An "r" indicates siege refused to attempt a proof. Finally, the rightmost column is the name of the benchmark formula.
1 UNSAT /velev/fvp-unsat.1.0/1dlx_c_mc_ex_bp_f.cnf
1 UNSAT /velev/fvp-unsat.1.0/2dlx_ca_mc_ex_bp_f.cnf
1 UNSAT /velev/fvp-unsat.1.0/2dlx_cc_mc_ex_bp_f.cnf
29 UNSAT /velev/fvp-unsat.1.0/9vliw_bp_mc.cnf
9 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug001.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug002.cnf
3 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug003.cnf
6 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug004.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug005.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug006.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug007.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug008.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug009.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug010.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug011.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug012.cnf
3 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug013.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug014.cnf
11 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug015.cnf
7 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug016.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug017.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug018.cnf
8 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug019.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug020.cnf
6 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug021.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug022.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug023.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug024.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug025.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug026.cnf
13 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug027.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug028.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug029.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug030.cnf
3 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug031.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug032.cnf
7 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug033.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug034.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug035.cnf
11 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug036.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug037.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug038.cnf
20 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug039.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug040.cnf
3 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug041.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug042.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug043.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug044.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug045.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug046.cnf
6 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug047.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug048.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug049.cnf
9 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug050.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug051.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug052.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug053.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug054.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug055.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug056.cnf
3 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug057.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug058.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug059.cnf
3 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug060.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug061.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug062.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug063.cnf
11 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug064.cnf
10 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug065.cnf
12 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug066.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug067.cnf
9 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug068.cnf
4 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug069.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug070.cnf
8 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug071.cnf
10 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug072.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug073.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug074.cnf
7 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug075.cnf
9 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug076.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug077.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug078.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug079.cnf
7 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug080.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug081.cnf
3 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug082.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug083.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug084.cnf
6 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug085.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug086.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug087.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug088.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug089.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug090.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug091.cnf
2 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug092.cnf
10 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug093.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug094.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug095.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug096.cnf
3 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug097.cnf
1 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug098.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug099.cnf
5 SAT /velev/vliw-sat-1.0/9vliw_bp_mc_bug100.cnf
1 UNSAT /velev/fvp-unsat.2.0/2pipe_1_ooo.cnf
1 UNSAT /velev/fvp-unsat.2.0/2pipe_2_ooo.cnf
1 UNSAT /velev/fvp-unsat.2.0/2pipe.cnf
1 UNSAT /velev/fvp-unsat.2.0/3pipe_1_ooo.cnf
1 UNSAT /velev/fvp-unsat.2.0/3pipe_2_ooo.cnf
2 UNSAT /velev/fvp-unsat.2.0/3pipe_3_ooo.cnf
1 UNSAT /velev/fvp-unsat.2.0/3pipe.cnf
6 UNSAT /velev/fvp-unsat.2.0/4pipe_1_ooo.cnf
7 UNSAT /velev/fvp-unsat.2.0/4pipe_2_ooo.cnf
8 UNSAT /velev/fvp-unsat.2.0/4pipe_3_ooo.cnf
9 UNSAT /velev/fvp-unsat.2.0/4pipe_4_ooo.cnf
6 UNSAT /velev/fvp-unsat.2.0/4pipe.cnf
21 UNSAT /velev/fvp-unsat.2.0/5pipe_1_ooo.cnf
21 UNSAT /velev/fvp-unsat.2.0/5pipe_2_ooo.cnf
19 UNSAT /velev/fvp-unsat.2.0/5pipe_3_ooo.cnf
36 UNSAT /velev/fvp-unsat.2.0/5pipe_4_ooo.cnf
20 UNSAT /velev/fvp-unsat.2.0/5pipe_5_ooo.cnf
4 UNSAT /velev/fvp-unsat.2.0/5pipe.cnf
99 UNSAT /velev/fvp-unsat.2.0/6pipe_6_ooo.cnf
45 UNSAT /velev/fvp-unsat.2.0/6pipe.cnf
7 SAT /velev/fvp-unsat.2.0/7pipe_bug.cnf
92 UNSAT /velev/fvp-unsat.2.0/7pipe.cnf
683 UNSAT /velev/fvp-unsat.3.0/pipe_64_1.cnf
1028 UNSAT /velev/fvp-unsat.3.0/pipe_64_2.cnf
2104 UNSAT /velev/fvp-unsat.3.0/pipe_64_4.cnf
1979 UNSAT /velev/fvp-unsat.3.0/pipe_64_8.cnf
5923 UNSAT /velev/fvp-unsat.3.0/pipe_64_16.cnf
? /velev/fvp-unsat.3.0/pipe_64_32.cnf
18 SAT /velev/fvp-sat.3.0/pipe_64_4_bug01.cnf
578 SAT /velev/fvp-sat.3.0/pipe_64_4_bug02.cnf
6 SAT /velev/fvp-sat.3.0/pipe_64_4_bug03.cnf
7 SAT /velev/fvp-sat.3.0/pipe_64_4_bug04.cnf
893 SAT /velev/fvp-sat.3.0/pipe_64_4_bug05.cnf
140 SAT /velev/fvp-sat.3.0/pipe_64_4_bug06.cnf
376 SAT /velev/fvp-sat.3.0/pipe_64_4_bug07.cnf
18 SAT /velev/fvp-sat.3.0/pipe_64_4_bug08.cnf
19 SAT /velev/fvp-sat.3.0/pipe_64_4_bug09.cnf
2 SAT /velev/fvp-sat.3.0/pipe_64_4_bug10.cnf
1553 SAT /velev/fvp-sat.3.0/pipe_64_4_bug11.cnf
18 SAT /velev/fvp-sat.3.0/pipe_64_4_bug12.cnf
336 SAT /velev/fvp-sat.3.0/pipe_64_4_bug13.cnf
9 SAT /velev/fvp-sat.3.0/pipe_64_4_bug14.cnf
362 SAT /velev/fvp-sat.3.0/pipe_64_4_bug15.cnf
367 SAT /velev/fvp-sat.3.0/pipe_64_4_bug16.cnf
355 SAT /velev/fvp-sat.3.0/pipe_64_4_bug17.cnf
687 SAT /velev/fvp-sat.3.0/pipe_64_4_bug18.cnf
1354 SAT /velev/fvp-sat.3.0/pipe_64_4_bug19.cnf
116 SAT /velev/fvp-sat.3.0/pipe_64_4_bug20.cnf
1 UNSAT /jpms-miters/c1355.cnf
1 UNSAT /jpms-miters/c1355-s.cnf
1 SAT /jpms-miters/c1908_bug.cnf
1 UNSAT /jpms-miters/c1908.cnf
2 UNSAT /jpms-miters/c1908-s.cnf
1 SAT /jpms-miters/c2670_bug.cnf
1 UNSAT /jpms-miters/c2670.cnf
1 UNSAT /jpms-miters/c2670-s.cnf
1 SAT /jpms-miters/c3540_bug.cnf
14 UNSAT /jpms-miters/c3540.cnf
9 UNSAT /jpms-miters/c3540-s.cnf
1 UNSAT /jpms-miters/c432.cnf
1 UNSAT /jpms-miters/c432-s.cnf
1 UNSAT /jpms-miters/c499.cnf
1 UNSAT /jpms-miters/c499-s.cnf
1 SAT /jpms-miters/c5315_bug.cnf
8 UNSAT /jpms-miters/c5315.cnf
6 UNSAT /jpms-miters/c5315-s.cnf
3877 UNSAT /jpms-miters/c6288.cnf
3962 UNSAT /jpms-miters/c6288-s.cnf
1 SAT /jpms-miters/c7552_bug.cnf
15 UNSAT /jpms-miters/c7552.cnf
16 UNSAT /jpms-miters/c7552-s.cnf
1 UNSAT /jpms-miters/c880.cnf
1 UNSAT /jpms-miters/c880-s.cnf
1 SAT /sat2002/prestwich/mediator/med11.shuffled.cnf
1 SAT /sat2002/prestwich/mediator/med17.shuffled.cnf
1 SAT /sat2002/prestwich/mediator/med19.shuffled.cnf
49 SAT /sat2002/prestwich/mediator/med30.shuffled.cnf
19 UNSAT /sat2002/vangelder/CheckerInterchange/avg-checker-4-23.shuffled.cnf
24 SAT /sat2002/vangelder/CheckerInterchange/avg-checker-4-24.shuffled.cnf
554 UNSAT /sat2002/vangelder/CheckerInterchange/avg-checker-5-34.shuffled.cnf
137 SAT /sat2002/vangelder/CheckerInterchange/avg-checker-5-35.shuffled.cnf
57 SAT /sat2002/dellacherie/cache/cache_05.shuffled.cnf
937 SAT /sat2002/dellacherie/cache/cache_10.shuffled.cnf
? /sat2002/dellacherie/comb/comb1.shuffled.cnf
286 UNSAT /sat2002/dellacherie/comb/comb2.shuffled.cnf
386 UNSAT /sat2002/dellacherie/comb/comb3.shuffled.cnf
58 UNSAT /sat2002/dellacherie/f2clk/f2clk_30.shuffled.cnf
740 UNSAT /sat2002/dellacherie/f2clk/f2clk_40.shuffled.cnf
8078 UNSAT /sat2002/dellacherie/f2clk/f2clk_50.shuffled.cnf
15 UNSAT /sat2002/dellacherie/fifo8/fifo8_100.shuffled.cnf
144 UNSAT /sat2002/dellacherie/fifo8/fifo8_200.shuffled.cnf
207 UNSAT /sat2002/dellacherie/fifo8/fifo8_300.shuffled.cnf
598 UNSAT /sat2002/dellacherie/fifo8/fifo8_400.shuffled.cnf
26 UNSAT /sat2002/dellacherie/ip/ip25.shuffled.cnf
62 UNSAT /sat2002/dellacherie/ip/ip36.shuffled.cnf
91 UNSAT /sat2002/dellacherie/ip/ip38.shuffled.cnf
202 UNSAT /sat2002/dellacherie/ip/ip50.shuffled.cnf
109 UNSAT /sat2002/dellacherie/w08/w08_10.shuffled.cnf
631 SAT /sat2002/dellacherie/w08/w08_14.shuffled.cnf
979 SAT /sat2002/dellacherie/w08/w08_15.shuffled.cnf
5 UNSAT /sat2002/dellacherie/w10/w10_45.shuffled.cnf
20 UNSAT /sat2002/dellacherie/w10/w10_60.shuffled.cnf
73 UNSAT /sat2002/dellacherie/w10/w10_70.shuffled.cnf
46 SAT /sat2002/dellacherie/w10/w10_75.shuffled.cnf
1 UNSAT /sat2002/goldberg/bmc1/23.shuffled.cnf
1 UNSAT /sat2002/goldberg/bmc1/42.shuffled.cnf
1 UNSAT /sat2002/goldberg/bmc1/4.shuffled.cnf
1 UNSAT /sat2002/goldberg/bmc1/61.shuffled.cnf
1 SAT /sat2002/goldberg/bmc2/cnt05.shuffled.cnf
1 SAT /sat2002/goldberg/bmc2/cnt06.shuffled.cnf
1 SAT /sat2002/goldberg/bmc2/cnt07.shuffled.cnf
11 SAT /sat2002/goldberg/bmc2/cnt08.shuffled.cnf
24 SAT /sat2002/goldberg/bmc2/cnt09.shuffled.cnf
137 SAT /sat2002/goldberg/bmc2/cnt10.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/9symml_gr_2pin_w5.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/9symml_gr_2pin_w6.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/9symml_gr_rcs_w5.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/9symml_gr_rcs_w6.shuffled.cnf
6 UNSAT /sat2002/goldberg/fpga_routing/alu2_gr_rcs_w7.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/alu2_gr_rcs_w8.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/apex7_gr_2pin_w4.shuffled.cnf
3 SAT /sat2002/goldberg/fpga_routing/apex7_gr_2pin_w5.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/apex7_gr_rcs_w5.shuffled.cnf
2 UNSAT /sat2002/goldberg/fpga_routing/c499_gr_2pin_w5.shuffled.cnf
12 SAT /sat2002/goldberg/fpga_routing/c499_gr_2pin_w6.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/c499_gr_rcs_w5.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/c499_gr_rcs_w6.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/c880_gr_rcs_w5.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/c880_gr_rcs_w6.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/c880_gr_rcs_w7.shuffled.cnf
2 UNSAT /sat2002/goldberg/fpga_routing/example2_gr_2pin_w5.shuffled.cnf
22 SAT /sat2002/goldberg/fpga_routing/example2_gr_2pin_w6.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/example2_gr_rcs_w5.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/example2_gr_rcs_w6.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/term1_gr_2pin_w3.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/term1_gr_2pin_w4.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/term1_gr_rcs_w3.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/term1_gr_rcs_w4.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/too_large_gr_rcs_w5.shuffled.cnf
1 UNSAT /sat2002/goldberg/fpga_routing/too_large_gr_rcs_w6.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/too_large_gr_rcs_w7.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/too_large_gr_rcs_w8.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/too_large_gr_rcs_w9.shuffled.cnf
18 UNSAT /sat2002/goldberg/fpga_routing/vda_gr_rcs_w7.shuffled.cnf
48 SAT /sat2002/goldberg/fpga_routing/vda_gr_rcs_w8.shuffled.cnf
1 SAT /sat2002/goldberg/fpga_routing/vda_gr_rcs_w9.shuffled.cnf
1 SAT /sat2002/goldberg/hanoi/hanoi4.shuffled.cnf
38 SAT /sat2002/goldberg/hanoi/hanoi5.shuffled.cnf
28 SAT /sat2002/goldberg/hanoi/hanoi6_fast.shuffled.cnf
50 SAT /sat2002/goldberg/hanoi/hanoi6_on.shuffled.cnf
384 SAT /sat2002/goldberg/hanoi/hanoi6.shuffled.cnf
1 UNSAT /sat2002/goldberg/rand_net/rand_net40-25-1.shuffled.cnf
15 UNSAT /sat2002/goldberg/rand_net/rand_net40-25-5.shuffled.cnf
30 UNSAT /sat2002/goldberg/rand_net/rand_net40-25-10.shuffled.cnf
1 UNSAT /sat2002/goldberg/rand_net/rand_net40-30-1.shuffled.cnf
25 UNSAT /sat2002/goldberg/rand_net/rand_net40-30-5.shuffled.cnf
18 UNSAT /sat2002/goldberg/rand_net/rand_net40-30-10.shuffled.cnf
1 UNSAT /sat2002/goldberg/rand_net/rand_net40-40-1.shuffled.cnf
23 UNSAT /sat2002/goldberg/rand_net/rand_net40-40-5.shuffled.cnf
39 UNSAT /sat2002/goldberg/rand_net/rand_net40-40-10.shuffled.cnf
1 UNSAT /sat2002/goldberg/rand_net/rand_net40-60-1.shuffled.cnf
23 UNSAT /sat2002/goldberg/rand_net/rand_net40-60-5.shuffled.cnf
478 UNSAT /sat2002/goldberg/rand_net/rand_net40-60-10.shuffled.cnf
3 UNSAT /sat2002/goldberg/rand_net/rand_net50-25-1.shuffled.cnf
43 UNSAT /sat2002/goldberg/rand_net/rand_net50-25-5.shuffled.cnf
40 UNSAT /sat2002/goldberg/rand_net/rand_net50-25-10.shuffled.cnf
1 UNSAT /sat2002/goldberg/rand_net/rand_net50-30-1.shuffled.cnf
345 UNSAT /sat2002/goldberg/rand_net/rand_net50-30-5.shuffled.cnf
204 UNSAT /sat2002/goldberg/rand_net/rand_net50-30-10.shuffled.cnf
1 UNSAT /sat2002/goldberg/rand_net/rand_net50-40-1.shuffled.cnf
230 UNSAT /sat2002/goldberg/rand_net/rand_net50-40-5.shuffled.cnf
404 UNSAT /sat2002/goldberg/rand_net/rand_net50-40-10.shuffled.cnf
1 UNSAT /sat2002/goldberg/rand_net/rand_net50-60-1.shuffled.cnf
301 UNSAT /sat2002/goldberg/rand_net/rand_net50-60-5.shuffled.cnf
690 UNSAT /sat2002/goldberg/rand_net/rand_net50-60-10.shuffled.cnf
7 UNSAT /sat2002/goldberg/rand_net/rand_net60-25-1.shuffled.cnf
277 UNSAT /sat2002/goldberg/rand_net/rand_net60-25-5.shuffled.cnf
203 UNSAT /sat2002/goldberg/rand_net/rand_net60-25-10.shuffled.cnf
1 UNSAT /sat2002/goldberg/rand_net/rand_net60-30-1.shuffled.cnf
166 UNSAT /sat2002/goldberg/rand_net/rand_net60-30-5.shuffled.cnf
142 UNSAT /sat2002/goldberg/rand_net/rand_net60-30-10.shuffled.cnf
10 UNSAT /sat2002/goldberg/rand_net/rand_net60-40-1.shuffled.cnf
640 UNSAT /sat2002/goldberg/rand_net/rand_net60-40-5.shuffled.cnf
523 UNSAT /sat2002/goldberg/rand_net/rand_net60-40-10.shuffled.cnf
4 UNSAT /sat2002/goldberg/rand_net/rand_net60-60-1.shuffled.cnf
864 UNSAT /sat2002/goldberg/rand_net/rand_net60-60-5.shuffled.cnf
915 UNSAT /sat2002/goldberg/rand_net/rand_net60-60-10.shuffled.cnf
46 UNSAT /sat2002/goldberg/rand_net/rand_net70-25-1.shuffled.cnf
372 UNSAT /sat2002/goldberg/rand_net/rand_net70-25-5.shuffled.cnf
142 UNSAT /sat2002/goldberg/rand_net/rand_net70-25-10.shuffled.cnf
5 UNSAT /sat2002/goldberg/rand_net/rand_net70-30-1.shuffled.cnf
349 UNSAT /sat2002/goldberg/rand_net/rand_net70-30-5.shuffled.cnf
314 UNSAT /sat2002/goldberg/rand_net/rand_net70-30-10.shuffled.cnf
6 UNSAT /sat2002/goldberg/rand_net/rand_net70-40-1.shuffled.cnf
504 UNSAT /sat2002/goldberg/rand_net/rand_net70-40-5.shuffled.cnf
510 UNSAT /sat2002/goldberg/rand_net/rand_net70-40-10.shuffled.cnf
6 UNSAT /sat2002/goldberg/rand_net/rand_net70-60-1.shuffled.cnf
642 UNSAT /sat2002/goldberg/rand_net/rand_net70-60-5.shuffled.cnf
1220 UNSAT /sat2002/goldberg/rand_net/rand_net70-60-10.shuffled.cnf
1 UNSAT /sat2002/biere/cmpadd/ca002.shuffled.cnf
1 UNSAT /sat2002/biere/cmpadd/ca004.shuffled.cnf
1 UNSAT /sat2002/biere/cmpadd/ca008.shuffled.cnf
1 UNSAT /sat2002/biere/cmpadd/ca016.shuffled.cnf
1 UNSAT /sat2002/biere/cmpadd/ca032.shuffled.cnf
1 UNSAT /sat2002/biere/cmpadd/ca064.shuffled.cnf
1 UNSAT /sat2002/biere/cmpadd/ca128.shuffled.cnf
2 UNSAT /sat2002/biere/cmpadd/ca256.shuffled.cnf
1 UNSAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k1.cnf
1 UNSAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k10.cnf
1 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k15.cnf
1 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k20.cnf
5 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k25.cnf
1 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k30.cnf
26 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k35.cnf
46 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k40.cnf
2 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k45.cnf
189 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k50.cnf
370 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k55.cnf
2 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k60.cnf
742 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k65.cnf
245 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k70.cnf
406 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k75.cnf
382 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k80.cnf
1185 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k85.cnf
1260 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k90.cnf
1319 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k95.cnf
538 SAT /zarpas/IBM_FV_2002_01_rule/SAT_dat.k100.cnf
1 UNSAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k1.cnf
1 UNSAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k10.cnf
1 UNSAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k15.cnf
1 UNSAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k20.cnf
1 UNSAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k25.cnf
1 UNSAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k30.cnf
8 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k35.cnf
14 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k40.cnf
43 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k45.cnf
66 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k50.cnf
94 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k55.cnf
144 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k60.cnf
140 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k65.cnf
180 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k70.cnf
395 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k75.cnf
456 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k80.cnf
1325 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k85.cnf
1529 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k90.cnf
1647 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k95.cnf
2133 SAT /zarpas/IBM_FV_2002_03_rule/SAT_dat.k100.cnf
1 UNSAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k1.cnf
1 UNSAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k10.cnf
1 UNSAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k15.cnf
1 UNSAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k20.cnf
2 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k25.cnf
3 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k30.cnf
13 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k35.cnf
26 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k40.cnf
46 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k45.cnf
76 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k50.cnf
230 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k55.cnf
291 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k60.cnf
272 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k65.cnf
433 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k70.cnf
947 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k75.cnf
535 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k80.cnf
414 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k85.cnf
818 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k90.cnf
1223 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k95.cnf
476 SAT /zarpas/IBM_FV_2002_04_rule/SAT_dat.k100.cnf
1 UNSAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k1.cnf
1 UNSAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k10.cnf
1 UNSAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k15.cnf
1 UNSAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k20.cnf
1 UNSAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k25.cnf
3 UNSAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k30.cnf
8 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k35.cnf
22 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k40.cnf
37 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k45.cnf
60 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k50.cnf
142 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k55.cnf
151 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k60.cnf
219 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k65.cnf
249 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k70.cnf
506 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k75.cnf
559 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k80.cnf
538 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k85.cnf
1162 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k90.cnf
852 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k95.cnf
1110 SAT /zarpas/IBM_FV_2002_05_rule/SAT_dat.k100.cnf
1 UNSAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k1.cnf
1 UNSAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k10.cnf
1 UNSAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k15.cnf
1 UNSAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k20.cnf
1 UNSAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k25.cnf
10 UNSAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k30.cnf
7 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k35.cnf
5 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k40.cnf
52 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k45.cnf
62 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k50.cnf
99 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k55.cnf
83 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k60.cnf
232 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k65.cnf
206 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k70.cnf
144 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k75.cnf
216 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k80.cnf
309 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k85.cnf
867 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k90.cnf
347 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k95.cnf
1062 SAT /zarpas/IBM_FV_2002_06_rule/SAT_dat.k100.cnf
1 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k1.cnf
18 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k10.cnf
5 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k15.cnf
6 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k20.cnf
7 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k25.cnf
7 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k30.cnf
7 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k35.cnf
8 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k40.cnf
7 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k45.cnf
10 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k50.cnf
11 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k55.cnf
8 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k60.cnf
8 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k65.cnf
8 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k70.cnf
10 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k75.cnf
9 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k80.cnf
10 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k85.cnf
10 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k90.cnf
8 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k95.cnf
12 UNSAT /zarpas/IBM_FV_2002_07_rule/SAT_dat.k100.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k1.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k10.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k15.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k20.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k25.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k30.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k35.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k40.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k45.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k50.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k55.cnf
6 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k60.cnf
9 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k65.cnf
6 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k70.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k75.cnf
14 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k80.cnf
2 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k85.cnf
2 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k90.cnf
12 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k95.cnf
1 UNSAT /zarpas/IBM_FV_2002_09_rule/SAT_dat.k100.cnf
1 UNSAT /velev/pipe_unsat_1.0/2pipe_k.cnf
1 UNSAT /velev/pipe_unsat_1.0/3pipe_k.cnf
6 UNSAT /velev/pipe_unsat_1.0/4pipe_k.cnf
18 UNSAT /velev/pipe_unsat_1.0/5pipe_k.cnf
11 UNSAT /velev/pipe_unsat_1.0/6pipe_k.cnf
81 UNSAT /velev/pipe_unsat_1.0/7pipe_k.cnf
188 UNSAT /velev/pipe_unsat_1.0/8pipe_k.cnf
157 UNSAT /velev/pipe_unsat_1.0/9pipe_k.cnf
1103 UNSAT /velev/pipe_unsat_1.0/10pipe_k.cnf
1651 UNSAT /velev/pipe_unsat_1.0/11pipe_k.cnf
4441 UNSAT /velev/pipe_unsat_1.0/12pipe_k.cnf
6883 UNSAT /velev/pipe_unsat_1.0/13pipe_k.cnf
14538 UNSAT /velev/pipe_unsat_1.0/14pipe_k.cnf
1 UNSAT /velev/pipe_unsat_1.1/2pipe_q0_k.cnf
1 UNSAT /velev/pipe_unsat_1.1/3pipe_q0_k.cnf
5 UNSAT /velev/pipe_unsat_1.1/4pipe_q0_k.cnf
15 UNSAT /velev/pipe_unsat_1.1/5pipe_q0_k.cnf
9 UNSAT /velev/pipe_unsat_1.1/6pipe_q0_k.cnf
58 UNSAT /velev/pipe_unsat_1.1/7pipe_q0_k.cnf
123 UNSAT /velev/pipe_unsat_1.1/8pipe_q0_k.cnf
103 UNSAT /velev/pipe_unsat_1.1/9pipe_q0_k.cnf
419 UNSAT /velev/pipe_unsat_1.1/10pipe_q0_k.cnf
769 UNSAT /velev/pipe_unsat_1.1/11pipe_q0_k.cnf
1356 UNSAT /velev/pipe_unsat_1.1/12pipe_q0_k.cnf
2446 UNSAT /velev/pipe_unsat_1.1/13pipe_q0_k.cnf
4260 UNSAT /velev/pipe_unsat_1.1/14pipe_q0_k.cnf
7780 UNSAT /velev/pipe_unsat_1.1/15pipe_q0_k.cnf
1909 SAT /velev/pipe_sat_1.0/12pipe_bug1.cnf ::::::::
902 SAT /velev/pipe_sat_1.0/12pipe_bug2.cnf ::::::::
120 SAT /velev/pipe_sat_1.0/12pipe_bug3.cnf ::::::::
484 SAT /velev/pipe_sat_1.0/12pipe_bug4.cnf ::::::::
1540 SAT /velev/pipe_sat_1.0/12pipe_bug5.cnf ::::::::
1773 SAT /velev/pipe_sat_1.0/12pipe_bug6.cnf ::::::::
952 SAT /velev/pipe_sat_1.0/12pipe_bug7.cnf ::::::::
39 SAT /velev/pipe_sat_1.0/12pipe_bug8.cnf ::::::::
704 SAT /velev/pipe_sat_1.0/12pipe_bug9.cnf ::::::::
928 SAT /velev/pipe_sat_1.0/12pipe_bug10.cnf ::::::: v3 outperforms v4 on
1330 SAT /velev/pipe_sat_1.1/12pipe_bug1_q0.cnf ::::: this pair of suites.
344 SAT /velev/pipe_sat_1.1/12pipe_bug2_q0.cnf :::::
1148 SAT /velev/pipe_sat_1.1/12pipe_bug3_q0.cnf :::::
41 SAT /velev/pipe_sat_1.1/12pipe_bug4_q0.cnf :::::
906 SAT /velev/pipe_sat_1.1/12pipe_bug5_q0.cnf :::::
113 SAT /velev/pipe_sat_1.1/12pipe_bug6_q0.cnf :::::
1186 SAT /velev/pipe_sat_1.1/12pipe_bug7_q0.cnf :::::
30 SAT /velev/pipe_sat_1.1/12pipe_bug8_q0.cnf :::::
922 SAT /velev/pipe_sat_1.1/12pipe_bug9_q0.cnf :::::
1693 SAT /velev/pipe_sat_1.1/12pipe_bug10_q0.cnf ::::
1 UNSAT /velev/pipe_ooo_unsat_1.0/2pipe_2_ooo.cnf
2 UNSAT /velev/pipe_ooo_unsat_1.0/3pipe_3_ooo.cnf
9 UNSAT /velev/pipe_ooo_unsat_1.0/4pipe_4_ooo.cnf
23 UNSAT /velev/pipe_ooo_unsat_1.0/5pipe_5_ooo.cnf
90 UNSAT /velev/pipe_ooo_unsat_1.0/6pipe_6_ooo.cnf
227 UNSAT /velev/pipe_ooo_unsat_1.0/7pipe_7_ooo.cnf
773 UNSAT /velev/pipe_ooo_unsat_1.0/8pipe_8_ooo.cnf
2117 UNSAT /velev/pipe_ooo_unsat_1.0/9pipe_9_ooo.cnf
15669 UNSAT /velev/pipe_ooo_unsat_1.0/10pipe_10_ooo.cnf
? /velev/pipe_ooo_unsat_1.0/11pipe_11_ooo.cnf
? /velev/pipe_ooo_unsat_1.0/12pipe_12_ooo.cnf
? /velev/pipe_ooo_unsat_1.0/13pipe_13_ooo.cnf
? /velev/pipe_ooo_unsat_1.0/14pipe_14_ooo.cnf
? /velev/pipe_ooo_unsat_1.0/15pipe_15_ooo.cnf
? /velev/pipe_ooo_unsat_1.0/16pipe_16_ooo.cnf
1 UNSAT /velev/pipe_ooo_unsat_1.1/2pipe_2_ooo_q0_T0.cnf
2 UNSAT /velev/pipe_ooo_unsat_1.1/3pipe_3_ooo_q0_T0.cnf
5 UNSAT /velev/pipe_ooo_unsat_1.1/4pipe_4_ooo_q0_T0.cnf
16 UNSAT /velev/pipe_ooo_unsat_1.1/5pipe_5_ooo_q0_T0.cnf
48 UNSAT /velev/pipe_ooo_unsat_1.1/6pipe_6_ooo_q0_T0.cnf
130 UNSAT /velev/pipe_ooo_unsat_1.1/7pipe_7_ooo_q0_T0.cnf
302 UNSAT /velev/pipe_ooo_unsat_1.1/8pipe_8_ooo_q0_T0.cnf
656 UNSAT /velev/pipe_ooo_unsat_1.1/9pipe_9_ooo_q0_T0.cnf
2958 UNSAT /velev/pipe_ooo_unsat_1.1/10pipe_10_ooo_q0_T0.cnf
12110 UNSAT /velev/pipe_ooo_unsat_1.1/11pipe_11_ooo_q0_T0.cnf
45994 UNSAT /velev/pipe_ooo_unsat_1.1/12pipe_12_ooo_q0_T0.cnf
? /velev/pipe_ooo_unsat_1.1/13pipe_13_ooo_q0_T0.cnf
? /velev/pipe_ooo_unsat_1.1/14pipe_14_ooo_q0_T0.cnf
? /velev/pipe_ooo_unsat_1.1/15pipe_15_ooo_q0_T0.cnf
5779 UNSAT /velev/vliw_unsat_3.0/9dlx_vliw_at_b_iq8_I3_C24.cnf
4921 UNSAT /velev/vliw_unsat_3.0/9dlx_vliw_at_b_iq8_I3_C24_D.cnf
1 UNSAT /cmu/barrel3.dimacs
1 UNSAT /cmu/barrel4.dimacs
1 UNSAT /cmu/barrel5.dimacs
4 UNSAT /cmu/barrel6.dimacs
16 UNSAT /cmu/barrel7.dimacs
97 UNSAT /cmu/barrel8.dimacs
32 UNSAT /cmu/barrel9.dimacs
1 UNSAT /cmu/longmult1.dimacs
1 UNSAT /cmu/longmult2.dimacs
1 UNSAT /cmu/longmult3.dimacs
1 UNSAT /cmu/longmult4.dimacs
1 UNSAT /cmu/longmult5.dimacs
1 UNSAT /cmu/longmult6.dimacs
5 UNSAT /cmu/longmult7.dimacs
26 UNSAT /cmu/longmult8.dimacs
70 UNSAT /cmu/longmult9.dimacs
168 UNSAT /cmu/longmult10.dimacs
220 UNSAT /cmu/longmult11.dimacs
316 UNSAT /cmu/longmult12.dimacs
338 UNSAT /cmu/longmult13.dimacs
322 UNSAT /cmu/longmult14.dimacs
210 UNSAT /cmu/longmult15.dimacs
1 UNSAT /cmu/queueinvar4.dimacs
1 UNSAT /cmu/queueinvar6.dimacs
1 UNSAT /cmu/queueinvar8.dimacs
1 UNSAT /cmu/queueinvar10.dimacs
1 UNSAT /cmu/queueinvar12.dimacs
1 UNSAT /cmu/queueinvar14.dimacs
1 UNSAT /cmu/queueinvar16.dimacs
1 UNSAT /cmu/queueinvar18.dimacs
1 UNSAT /cmu/queueinvar20.dimacs
2 SAT /bejing/e0ddr2-10-by-5-1.cnf
1 SAT /bejing/e0ddr2-10-by-5-4.cnf
1 SAT /bejing/enddr2-10-by-5-1.cnf
1 SAT /bejing/enddr2-10-by-5-8.cnf
1 SAT /bejing/ewddr2-10-by-5-1.cnf
1 SAT /bejing/ewddr2-10-by-5-8.cnf
589 UNSAT /bejing/2bitadd_10.cnf
1 SAT /bejing/2bitadd_11.cnf
1 SAT /bejing/2bitadd_12.cnf
1 SAT /bejing/2bitcomp_5.cnf
1 SAT /bejing/2bitmax_6.cnf
135 SAT /bejing/3bitadd_31.cnf
11 SAT /bejing/3bitadd_32.cnf
1 SAT /bejing/3blocks.cnf
1 SAT /bejing/4blocksb.cnf
1 SAT /bejing/4blocks.cnf
476 UNSAT /sat2003/industrial/schuppan/l2s/abp1-1-k31-unsat.shuffled-as.sat03-402.cnf
620 UNSAT /sat2003/industrial/schuppan/l2s/abp4-1-k31-unsat.shuffled-as.sat03-403.cnf
r /sat2003/industrial/schuppan/l2s/bc56-sensors-1-k391-unsat.shuffled-as.sat03-404.cnf
r /sat2003/industrial/schuppan/l2s/bc56-sensors-2-k592-unsat.shuffled-as.sat03-405.cnf
45654 UNSAT /sat2003/industrial/schuppan/l2s/bc57-sensors-1-k303-unsat.shuffled-as.sat03-406.cnf
? /sat2003/industrial/schuppan/l2s/dme-03-1-k247-unsat.shuffled-as.sat03-407.cnf
4049 UNSAT /sat2003/industrial/schuppan/l2s/guidance-1-k56-unsat.shuffled-as.sat03-408.cnf
r /sat2003/industrial/schuppan/l2s/motors-stuck-1-k407-unsat.shuffled-as.sat03-409.cnf
31316 UNSAT /sat2003/industrial/schuppan/l2s/motors-stuck-2-k314-unsat.shuffled-as.sat03-410.cnf
33576 SAT /sat2003/industrial/schuppan/l2s/motors-stuck-2-k315-sat.shuffled-as.sat03-411.cnf
r /sat2003/industrial/schuppan/l2s/valves-gates-1-k617-unsat.shuffled-as.sat03-412.cnf
...more to come.