benchmarks for model counting

[Daniel Pehoushek]

book of the middle by daniel
forty fifth degree problems each with 500 variables
n variables m clauses #c components answer length in bits #a assumptions #p model count
the problems took ten trillion inferences to solve.
thirty years of work on satisfiability
avoid negation and prosper
daniel2380+++
[c3d5N250_0.veg 1]
1 (n 500 m 2125) #c14327716 answerlen = 29 #a 60327026 #P=#Q=#p=#q= 276870906
2 (n 500 m 2125) #c7201625 answerlen = 27 #a 33474491 #P=#Q=#p=#q= 82372362
3 (n 500 m 2125) #c33498671 answerlen = 31 #a 116160763 #P=#Q=#p=#q= 1919566692
4 (n 500 m 2125) #c20305056 answerlen = 33 #a 76354981 #P=#Q=#p=#q= 4493221842
5 (n 500 m 2125) #c11025227 answerlen = 29 #a 44244213 #P=#Q=#p=#q= 404720046
6 (n 500 m 2125) #c74556402 answerlen = 34 #a 235350600 #P=#Q=#p=#q= 14469143238
7 (n 500 m 2125) #c23635006 answerlen = 32 #a 80756088 #P=#Q=#p=#q= 2408011860
8 (n 500 m 2125) #c10436784 answerlen = 28 #a 44760254 #P=#Q=#p=#q= 212882886
9 (n 500 m 2125) #c135433744 answerlen = 37 #a 336467772 #P=#Q=#p=#q= 70552088382
10 (n 500 m 2125) #c12187445 answerlen = 28 #a 49987332 #P=#Q=#p=#q= 168531204
[c3d5N250_0.veg 10 (t 94987409418 z 0)(work 1077883520 3019 846866338)] n 10 avg 34260767 variance 1317
[c3d5N250_1.veg 2]
1 (n 500 m 2125) #c27158374 answerlen = 33 #a 87589141 #P=#Q=#p=#q= 6543711900
2 (n 500 m 2125) #c12055132 answerlen = 29 #a 51623724 #P=#Q=#p=#q= 358628304
3 (n 500 m 2125) #c10934428 answerlen = 30 #a 43104465 #P=#Q=#p=#q= 581583036
4 (n 500 m 2125) #c6977593 answerlen = 25 #a 34603282 #P=#Q=#p=#q= 16896648
5 (n 500 m 2125) #c20813847 answerlen = 32 #a 69157664 #P=#Q=#p=#q= 2400574686
6 (n 500 m 2125) #c63790488 answerlen = 34 #a 184367001 #P=#Q=#p=#q= 15292967628
7 (n 500 m 2125) #c5810679 answerlen = 26 #a 28426068 #P=#Q=#p=#q= 41391696
8 (n 500 m 2125) #c8101675 answerlen = 27 #a 36104050 #P=#Q=#p=#q= 108706524
9 (n 500 m 2125) #c13415016 answerlen = 28 #a 59740466 #P=#Q=#p=#q= 174495312
10 (n 500 m 2125) #c37197878 answerlen = 34 #a 132682567 #P=#Q=#p=#q= 8620620264
[c3d5N250_1.veg 10 (t 34139575998 z 0)(work 727398428 2327 329263662)] n 20 avg 27443139 variance 1355
[c3d5N250_2.veg 3]
1 (n 500 m 2125) #c10794233 answerlen = 30 #a 44806515 #P=#Q=#p=#q= 754742646
2 (n 500 m 2125) #c12745695 answerlen = 28 #a 53511599 #P=#Q=#p=#q= 217669890
3 (n 500 m 2125) #c13130047 answerlen = 30 #a 47242144 #P=#Q=#p=#q= 871224288
4 (n 500 m 2125) #c22827118 answerlen = 32 #a 78389929 #P=#Q=#p=#q= 3072434004
5 (n 500 m 2125) #c9455508 answerlen = 27 #a 44005641 #P=#Q=#p=#q= 121038054
6 (n 500 m 2125) #c14606821 answerlen = 31 #a 55577844 #P=#Q=#p=#q= 1218900282
7 (n 500 m 2125) #c31116228 answerlen = 33 #a 106722699 #P=#Q=#p=#q= 6183758628
8 (n 500 m 2125) #c28770410 answerlen = 33 #a 98477816 #P=#Q=#p=#q= 5751222708
9 (n 500 m 2125) #c38441603 answerlen = 34 #a 117151866 #P=#Q=#p=#q= 11175709164
10 (n 500 m 2125) #c7189080 answerlen = 26 #a 32579492 #P=#Q=#p=#q= 44751414
[c3d5N250_2.veg 10 (t 29411451078 z 0)(work 678465545 2276 843449656)] n 30 avg 24597984 variance 1365
[c3d5N250_3.veg 4]
1 (n 500 m 2125) #c21979611 answerlen = 30 #a 87538820 #P=#Q=#p=#q= 626541876
2 (n 500 m 2125) #c9173907 answerlen = 25 #a 44242236 #P=#Q=#p=#q= 32506698
3 (n 500 m 2125) #c6577801 answerlen = 26 #a 30296676 #P=#Q=#p=#q= 36089250
4 (n 500 m 2125) #c11703700 answerlen = 27 #a 53819131 #P=#Q=#p=#q= 67402830
5 (n 500 m 2125) #c22861120 answerlen = 31 #a 73670314 #P=#Q=#p=#q= 1675123278
6 (n 500 m 2125) #c20047079 answerlen = 31 #a 76641830 #P=#Q=#p=#q= 1088610372
7 (n 500 m 2125) #c21701255 answerlen = 30 #a 83731996 #P=#Q=#p=#q= 881277810
8 (n 500 m 2125) #c14117378 answerlen = 31 #a 48351669 #P=#Q=#p=#q= 1681925628
9 (n 500 m 2125) #c8226371 answerlen = 25 #a 40020954 #P=#Q=#p=#q= 30645936
10 (n 500 m 2125) #c8030624 answerlen = 26 #a 35295573 #P=#Q=#p=#q= 39162528
[c3d5N250_3.veg 10 (t 6159286206 z 0)(work 573609199 2116 831548232)] n 40 avg 22058959 variance 1365
[bigsums (tfiles 4 tforms 40) (numberp 164697722700 zeromos 0)(retros 3057356692 bigoh 9740 billion 851127888)]

[Jeffrey Rubard]

"Intellectual deception or chicanery".

[Daniel Pehoushek]

i have worked for thirty years on satisfiability.
my program runs well on modest sizes of formulas.
avoid negation and prosper with truth.
daniel2380+++

[Jeffrey Rubard]

"Clap, clap, clap." #nowispnporwhat

[Daniel Pehoushek]

for modest sizes satisfiability is solvable.
there is the Big Equality:
coNP=NP=Pspace=#P=#Q=Qspace

and for modest sizes that equality includes P.
in general though the equality includes Exp.

avoid negation and prosper in truth,
daniel2380+++

[Jeffrey Rubard]

"That's pretty special." #everyonesays

[Jeffrey Rubard]

It would be the sort of thing you "mocked" other people for writing, etc.