CNF Benchmark Suite: PIPE-UNSAT.1.1
======================================
Description: Bigger variants of the pipe benchmarks, generated in a new way [1]
# of instances: 14
Author: Miroslav N. Velev (mvelev@ece.cmu.edu)
http://www.ece.cmu.edu/~mvelev
Date: August 1, 2003
CNF Formula Size [Bytes] Variables Clauses Literals Avg. Literals/Clause
--------------------------------------------------------------------------------------------
2pipe_q0_k 91834 873 6457 18211 2.820350
3pipe_q0_k 402055 2476 25181 72337 2.872682
4pipe_q0_k 1178618 5380 69072 200460 2.902189
5pipe_q0_k 2714191 10026 154409 451029 2.921002
6pipe_q0_k 5824780 16775 315960 927596 2.935802
7pipe_q0_k 10234980 26512 536414 1578920 2.943473
8pipe_q0_k 17414545 39434 887706 2619334 2.950677
9pipe_q0_k 29200738 55996 1468197 4342389 2.957634
10pipe_q0_k 42632265 77639 2082017 6164595 2.960876
11pipe_qo_k 62225540 104244 3007883 8917203 2.964611
12pipe_q0_k 89289882 136800 4216460 12513320 2.967731
13pipe_q0_k 124236186 176066 5761591 17114087 2.970375
14pipe_qo_k 168298622 222845 7702617 22897135 2.972644
15pipe_qo_k 223677519 277976 10103924 30055234 2.974610
References:
[1] M.N. Velev, "Automatic Abstraction of Equations in a Logic of Equality,"
TABLEAUX'03, LNAI, Springer-Verlag, September 2003.