blob: 470b16307edcbc41bdb15e59eb6f122e01f58e6d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
UC Berkeley, ABC 1.01 (compiled Jan 20 2007 16:47:34)
abc.rc: No such file or directory
Loaded "abc.rc" from the parent directory.
abc 01> test
Found last conflict after adding unit clause number 10229!
Roots = 7184. Learned = 3047. Total = 10231. Steps = 196361. Ave = 62.09. Used = 2224. Ratio = 0.73.
Runtime stats:
Reading = 0.03 sec
BCP = 0.32 sec
Trace = 0.06 sec
TOTAL = 0.43 sec
abc 01> test
Found last conflict after adding unit clause number 7676!
Roots = 6605. Learned = 1073. Total = 7678. Steps = 52402. Ave = 42.68. Used = 1011. Ratio = 0.94.
Runtime stats:
Reading = 0.01 sec
BCP = 0.02 sec
Trace = 0.02 sec
TOTAL = 0.06 sec
abc 01> test
Found last conflict after adding unit clause number 37868!
Roots = 15443. Learned = 22427. Total = 37870. Steps = 2365472. Ave = 104.79. Used = 19763. Ratio = 0.88.
Runtime stats:
Reading = 0.20 sec
BCP = 14.67 sec
Trace = 0.56 sec
TOTAL = 15.74 sec
abc 01>
abc 05> wb ibm_bmc/len25u_renc.blif
abc 05> ps
(no name) : i/o = 348/ 1 lat = 0 nd = 3648 bdd = 15522 lev = 246
abc 05> sat -v
==================================[MINISAT]===================================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Clauses Literals | Limit Clauses Literals Lit/Cl | |
==============================================================================
| 0 | 17413 54996 | 5804 0 0 0.0 | 0.000 % |
| 100 | 17413 54996 | 6384 100 606 6.1 | 0.417 % |
| 250 | 17413 54996 | 7023 250 1586 6.3 | 0.417 % |
| 476 | 17413 54996 | 7725 476 3288 6.9 | 0.417 % |
| 813 | 17413 54996 | 8498 813 7586 9.3 | 0.417 % |
| 1319 | 17403 54970 | 9347 1318 14848 11.3 | 0.442 % |
| 2078 | 17403 54970 | 10282 2076 40186 19.4 | 0.466 % |
| 3217 | 17397 54948 | 11310 3208 99402 31.0 | 0.466 % |
| 4926 | 17392 54930 | 12441 4911 131848 26.8 | 0.491 % |
| 7489 | 17392 54930 | 13686 7474 204217 27.3 | 0.491 % |
| 11336 | 17357 54829 | 15054 11310 332863 29.4 | 0.638 % |
| 17103 | 17346 54794 | 16559 9130 203029 22.2 | 0.687 % |
| 25752 | 17288 54606 | 18215 9083 176982 19.5 | 0.834 % |
| 38727 | 17266 54536 | 20037 12674 278949 22.0 | 0.883 % |
| 58188 | 17240 54453 | 22041 11905 255255 21.4 | 0.957 % |
==============================================================================
Start = 15. Conf = 79435. Dec = 130967. Prop = 24083434. Insp = 136774586.
Total runtime = 18.66 sec. Var select = 0.00 sec. Var update = 0.00 sec.
UNSATISFIABLE Time = 18.69 sec
abc 05>
abc 05> test
Found last conflict after adding unit clause number 96902!
Roots = 17469. Learned = 79435. Total = 96904. Steps = 9700042. Ave = 121.89. Used = 57072. Ratio = 0.72.
Runtime stats:
Reading = 1.26 sec
BCP = 204.99 sec
Trace = 2.85 sec
TOTAL = 209.85 sec
|
