diff options
Diffstat (limited to 'src/sat/proof/stats.txt')
| -rw-r--r-- | src/sat/proof/stats.txt | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/src/sat/proof/stats.txt b/src/sat/proof/stats.txt new file mode 100644 index 00000000..470b1630 --- /dev/null +++ b/src/sat/proof/stats.txt @@ -0,0 +1,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
\ No newline at end of file |