CNF Benchmark Suite: PIPE-SAT.1.1
======================================
Description: Satisfiable variants of the pipe benchmarks, generated in a new way [1]
# of instances: 10
Author: Miroslav N. Velev (mvelev@ece.cmu.edu)
http://www.ece.cmu.edu/~mvelev
Date: August 24, 2003
CNF Formula Size [Bytes] Variables Clauses Literals Avg. Literals/Clause
--------------------------------------------------------------------------------------------
12pipe_bug1_q0 100677465 138917 4678756 13900208 2.970920
12pipe_bug2_q0 100676033 138918 4678718 13900094 2.970919
12pipe_bug3_q0 100678042 138917 4678757 13900213 2.970920
12pipe_bug4_q0 100557545 138563 4675040 13889090 2.970903
12pipe_bug5_q0 100677045 138918 4678760 13900220 2.970920
12pipe_bug6_q0 100539888 138795 4671352 13877998 2.970874
12pipe_bug7_q0 100677045 138918 4678760 13900220 2.970920
12pipe_bug8_q0 100812466 138711 4688614 13929700 2.970963
12pipe_bug9_q0 100627621 138916 4676007 13891965 2.970903
12pipe_bug10_q0 100677045 138918 4678760 13900220 2.970920
References:
[1] M.N. Velev, "Automatic Abstraction of Equations in a Logic of Equality,"
TABLEAUX'03, LNAI, Springer-Verlag, September 2003.
output of md5sum:
--------------------------------------------------------------------------------------------
3c06742a0f52b1c3cc96856908e90bad 12pipe_bug1_q0.cnf
8afd2c931b241c210764e56e8c468329 12pipe_bug2_q0.cnf
aece0791e9f6339d6eafded4c5220bd3 12pipe_bug3_q0.cnf
353cbce069afb7654a0a33c62dd11149 12pipe_bug4_q0.cnf
08a4bb2dad0aa220a8506c7ff70b8885 12pipe_bug5_q0.cnf
1576b2e291afe2889389d4b20ac16137 12pipe_bug6_q0.cnf
f248736a511ed8b647373d234bab8d53 12pipe_bug7_q0.cnf
4f8b79b4649c1b5d164965f85c8fc69d 12pipe_bug8_q0.cnf
e18e9fa51e17ebce8e7d4716e627c5b4 12pipe_bug9_q0.cnf
04cbd09538ef5216422d0ed990812a22 12pipe_bug10_q0.cnf