Rocksolid Light

Welcome to Rocksolid Light

mail  files  register  newsreader  groups  login

Message-ID:  

"How do I love thee? My accumulator overflows."

devel / comp.theory / Re: benchmarks for model counting

SubjectAuthor
* benchmarks for model countingDaniel Pehoushek
`* benchmarks for model countingJeffrey Rubard
 `* benchmarks for model countingDaniel Pehoushek
  `* benchmarks for model countingJeffrey Rubard
   `* benchmarks for model countingDaniel Pehoushek
    `* benchmarks for model countingJeffrey Rubard
     `- benchmarks for model countingJeffrey Rubard

1
benchmarks for model counting

<c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com>

  copy mid

https://news.novabbs.org/devel/article-flat.php?id=48857&group=comp.theory#48857

  copy link   Newsgroups: comp.theory
X-Received: by 2002:a05:620a:2048:b0:76d:be21:5074 with SMTP id d8-20020a05620a204800b0076dbe215074mr127021qka.7.1694712903031;
Thu, 14 Sep 2023 10:35:03 -0700 (PDT)
X-Received: by 2002:a05:6870:5b19:b0:1d5:8fad:fb03 with SMTP id
ds25-20020a0568705b1900b001d58fadfb03mr862598oab.4.1694712902860; Thu, 14 Sep
2023 10:35:02 -0700 (PDT)
Path: i2pn2.org!i2pn.org!news.niel.me!glou.org!news.glou.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Thu, 14 Sep 2023 10:35:02 -0700 (PDT)
Injection-Info: google-groups.googlegroups.com; posting-host=2600:2b00:774c:5000:d141:40ef:bd11:ed2a;
posting-account=wr2KGQoAAADwR6kcaFpOhQvlGldc1Uke
NNTP-Posting-Host: 2600:2b00:774c:5000:d141:40ef:bd11:ed2a
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com>
Subject: benchmarks for model counting
From: pehoushek1@gmail.com (Daniel Pehoushek)
Injection-Date: Thu, 14 Sep 2023 17:35:03 +0000
Content-Type: text/plain; charset="UTF-8"
 by: Daniel Pehoushek - Thu, 14 Sep 2023 17:35 UTC

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)]

Re: benchmarks for model counting

<608b20b8-4a27-47ee-b5c6-ba3cf440a760n@googlegroups.com>

  copy mid

https://news.novabbs.org/devel/article-flat.php?id=48861&group=comp.theory#48861

  copy link   Newsgroups: comp.theory
X-Received: by 2002:a05:622a:190b:b0:417:b540:53c0 with SMTP id w11-20020a05622a190b00b00417b54053c0mr2616qtc.0.1695405888308;
Fri, 22 Sep 2023 11:04:48 -0700 (PDT)
X-Received: by 2002:a05:6808:18a7:b0:3a7:b648:f0a7 with SMTP id
bi39-20020a05680818a700b003a7b648f0a7mr253484oib.0.1695405887889; Fri, 22 Sep
2023 11:04:47 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!border-2.nntp.ord.giganews.com!nntp.giganews.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Fri, 22 Sep 2023 11:04:47 -0700 (PDT)
In-Reply-To: <c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=198.236.192.210; posting-account=0pheVgoAAACKj674Kl3qdRoiYysIz_ok
NNTP-Posting-Host: 198.236.192.210
References: <c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <608b20b8-4a27-47ee-b5c6-ba3cf440a760n@googlegroups.com>
Subject: Re: benchmarks for model counting
From: jeffreydanielrubard@gmail.com (Jeffrey Rubard)
Injection-Date: Fri, 22 Sep 2023 18:04:48 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Lines: 105
 by: Jeffrey Rubard - Fri, 22 Sep 2023 18:04 UTC

On Thursday, September 14, 2023 at 10:35:04 AM UTC-7, Daniel Pehoushek wrote:
> 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)]

"Intellectual deception or chicanery".

Re: benchmarks for model counting

<478d661f-34af-482c-bbd8-8da4a193c84dn@googlegroups.com>

  copy mid

https://news.novabbs.org/devel/article-flat.php?id=48870&group=comp.theory#48870

  copy link   Newsgroups: comp.theory
X-Received: by 2002:a05:620a:4881:b0:76f:1b38:e73d with SMTP id ea1-20020a05620a488100b0076f1b38e73dmr35117qkb.10.1696434499738;
Wed, 04 Oct 2023 08:48:19 -0700 (PDT)
X-Received: by 2002:a05:6830:4aa:b0:6c7:aab5:6b60 with SMTP id
l10-20020a05683004aa00b006c7aab56b60mr1299541otd.2.1696434499556; Wed, 04 Oct
2023 08:48:19 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!panix!usenet.blueworldhosting.com!diablo1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Wed, 4 Oct 2023 08:48:19 -0700 (PDT)
In-Reply-To: <608b20b8-4a27-47ee-b5c6-ba3cf440a760n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=2600:2b00:774c:5000:2083:6196:3823:805;
posting-account=wr2KGQoAAADwR6kcaFpOhQvlGldc1Uke
NNTP-Posting-Host: 2600:2b00:774c:5000:2083:6196:3823:805
References: <c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com> <608b20b8-4a27-47ee-b5c6-ba3cf440a760n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <478d661f-34af-482c-bbd8-8da4a193c84dn@googlegroups.com>
Subject: Re: benchmarks for model counting
From: pehoushek1@gmail.com (Daniel Pehoushek)
Injection-Date: Wed, 04 Oct 2023 15:48:19 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 6674
 by: Daniel Pehoushek - Wed, 4 Oct 2023 15:48 UTC

On Friday, September 22, 2023 at 2:04:49 PM UTC-4, Jeffrey Rubard wrote:
> On Thursday, September 14, 2023 at 10:35:04 AM UTC-7, Daniel Pehoushek wrote:
> > 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)]
> "Intellectual deception or chicanery".
i have worked for thirty years on satisfiability.
my program runs well on modest sizes of formulas.
avoid negation and prosper with truth.
daniel2380+++

Re: benchmarks for model counting

<4583875e-e90e-428a-8d51-4dd79f13d003n@googlegroups.com>

  copy mid

https://news.novabbs.org/devel/article-flat.php?id=48871&group=comp.theory#48871

  copy link   Newsgroups: comp.theory
X-Received: by 2002:ac8:7e82:0:b0:419:55b6:758b with SMTP id w2-20020ac87e82000000b0041955b6758bmr47864qtj.7.1696446264524;
Wed, 04 Oct 2023 12:04:24 -0700 (PDT)
X-Received: by 2002:a05:6808:1782:b0:3a7:3488:bc37 with SMTP id
bg2-20020a056808178200b003a73488bc37mr1772876oib.9.1696446264309; Wed, 04 Oct
2023 12:04:24 -0700 (PDT)
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Wed, 4 Oct 2023 12:04:24 -0700 (PDT)
In-Reply-To: <478d661f-34af-482c-bbd8-8da4a193c84dn@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=198.236.192.210; posting-account=iACVhwoAAAAxCNRb5QwwB44b3nqFpEM1
NNTP-Posting-Host: 198.236.192.210
References: <c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com>
<608b20b8-4a27-47ee-b5c6-ba3cf440a760n@googlegroups.com> <478d661f-34af-482c-bbd8-8da4a193c84dn@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4583875e-e90e-428a-8d51-4dd79f13d003n@googlegroups.com>
Subject: Re: benchmarks for model counting
From: theleasthappyfella@gmail.com (Jeffrey Rubard)
Injection-Date: Wed, 04 Oct 2023 19:04:24 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
 by: Jeffrey Rubard - Wed, 4 Oct 2023 19:04 UTC

On Wednesday, October 4, 2023 at 8:48:21 AM UTC-7, Daniel Pehoushek wrote:
> On Friday, September 22, 2023 at 2:04:49 PM UTC-4, Jeffrey Rubard wrote:
> > On Thursday, September 14, 2023 at 10:35:04 AM UTC-7, Daniel Pehoushek wrote:
> > > 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)]
> > "Intellectual deception or chicanery".
> i have worked for thirty years on satisfiability.
> my program runs well on modest sizes of formulas.
> avoid negation and prosper with truth.
> daniel2380+++

"Clap, clap, clap." #nowispnporwhat

Re: benchmarks for model counting

<f9f545f5-695c-45c3-92ef-41acec4cd921n@googlegroups.com>

  copy mid

https://news.novabbs.org/devel/article-flat.php?id=48872&group=comp.theory#48872

  copy link   Newsgroups: comp.theory
X-Received: by 2002:a05:620a:84d:b0:775:74da:8c4f with SMTP id u13-20020a05620a084d00b0077574da8c4fmr51519qku.5.1696484055446;
Wed, 04 Oct 2023 22:34:15 -0700 (PDT)
X-Received: by 2002:a05:6808:1b23:b0:3ad:f838:d02b with SMTP id
bx35-20020a0568081b2300b003adf838d02bmr2348598oib.0.1696484055199; Wed, 04
Oct 2023 22:34:15 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!feeder.erje.net!fdn.fr!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Wed, 4 Oct 2023 22:34:14 -0700 (PDT)
In-Reply-To: <4583875e-e90e-428a-8d51-4dd79f13d003n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=2600:2b00:774c:5000:38b7:e62c:5daf:17d6;
posting-account=wr2KGQoAAADwR6kcaFpOhQvlGldc1Uke
NNTP-Posting-Host: 2600:2b00:774c:5000:38b7:e62c:5daf:17d6
References: <c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com>
<608b20b8-4a27-47ee-b5c6-ba3cf440a760n@googlegroups.com> <478d661f-34af-482c-bbd8-8da4a193c84dn@googlegroups.com>
<4583875e-e90e-428a-8d51-4dd79f13d003n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <f9f545f5-695c-45c3-92ef-41acec4cd921n@googlegroups.com>
Subject: Re: benchmarks for model counting
From: pehoushek1@gmail.com (Daniel Pehoushek)
Injection-Date: Thu, 05 Oct 2023 05:34:15 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
 by: Daniel Pehoushek - Thu, 5 Oct 2023 05:34 UTC

On Wednesday, October 4, 2023 at 3:04:26 PM UTC-4, Jeffrey Rubard wrote:
> On Wednesday, October 4, 2023 at 8:48:21 AM UTC-7, Daniel Pehoushek wrote:
> > On Friday, September 22, 2023 at 2:04:49 PM UTC-4, Jeffrey Rubard wrote:
> > > On Thursday, September 14, 2023 at 10:35:04 AM UTC-7, Daniel Pehoushek wrote:
> > > > 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)]
> > > "Intellectual deception or chicanery".
> > i have worked for thirty years on satisfiability.
> > my program runs well on modest sizes of formulas.
> > avoid negation and prosper with truth.
> > daniel2380+++
> "Clap, clap, clap." #nowispnporwhat
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+++

Re: benchmarks for model counting

<6fc23e03-9d3b-482b-bbd6-3b7a1ed58640n@googlegroups.com>

  copy mid

https://news.novabbs.org/devel/article-flat.php?id=48873&group=comp.theory#48873

  copy link   Newsgroups: comp.theory
X-Received: by 2002:ad4:5982:0:b0:65e:3aba:a155 with SMTP id ek2-20020ad45982000000b0065e3abaa155mr80082qvb.8.1696529350048;
Thu, 05 Oct 2023 11:09:10 -0700 (PDT)
X-Received: by 2002:a05:6808:19a9:b0:3ae:61f:335e with SMTP id
bj41-20020a05680819a900b003ae061f335emr3188188oib.5.1696529349822; Thu, 05
Oct 2023 11:09:09 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!feeder.erje.net!fdn.fr!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Thu, 5 Oct 2023 11:09:09 -0700 (PDT)
In-Reply-To: <f9f545f5-695c-45c3-92ef-41acec4cd921n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=198.236.192.210; posting-account=iACVhwoAAAAxCNRb5QwwB44b3nqFpEM1
NNTP-Posting-Host: 198.236.192.210
References: <c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com>
<608b20b8-4a27-47ee-b5c6-ba3cf440a760n@googlegroups.com> <478d661f-34af-482c-bbd8-8da4a193c84dn@googlegroups.com>
<4583875e-e90e-428a-8d51-4dd79f13d003n@googlegroups.com> <f9f545f5-695c-45c3-92ef-41acec4cd921n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <6fc23e03-9d3b-482b-bbd6-3b7a1ed58640n@googlegroups.com>
Subject: Re: benchmarks for model counting
From: theleasthappyfella@gmail.com (Jeffrey Rubard)
Injection-Date: Thu, 05 Oct 2023 18:09:10 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
 by: Jeffrey Rubard - Thu, 5 Oct 2023 18:09 UTC

On Wednesday, October 4, 2023 at 10:34:17 PM UTC-7, Daniel Pehoushek wrote:
> On Wednesday, October 4, 2023 at 3:04:26 PM UTC-4, Jeffrey Rubard wrote:
> > On Wednesday, October 4, 2023 at 8:48:21 AM UTC-7, Daniel Pehoushek wrote:
> > > On Friday, September 22, 2023 at 2:04:49 PM UTC-4, Jeffrey Rubard wrote:
> > > > On Thursday, September 14, 2023 at 10:35:04 AM UTC-7, Daniel Pehoushek wrote:
> > > > > 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)]
> > > > "Intellectual deception or chicanery".
> > > i have worked for thirty years on satisfiability.
> > > my program runs well on modest sizes of formulas.
> > > avoid negation and prosper with truth.
> > > daniel2380+++
> > "Clap, clap, clap." #nowispnporwhat
> 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+++

"That's pretty special." #everyonesays

Re: benchmarks for model counting

<06350f9e-63f6-40c2-8848-05ea80c15652n@googlegroups.com>

  copy mid

https://news.novabbs.org/devel/article-flat.php?id=48874&group=comp.theory#48874

  copy link   Newsgroups: comp.theory
X-Received: by 2002:a05:620a:cc1:b0:76f:6e2:8bea with SMTP id b1-20020a05620a0cc100b0076f06e28beamr74824qkj.12.1696529400632;
Thu, 05 Oct 2023 11:10:00 -0700 (PDT)
X-Received: by 2002:a05:6871:6a99:b0:1dc:34ea:1a6a with SMTP id
zf25-20020a0568716a9900b001dc34ea1a6amr2281616oab.6.1696529400309; Thu, 05
Oct 2023 11:10:00 -0700 (PDT)
Path: i2pn2.org!i2pn.org!news.hispagatos.org!news.nntp4.net!usenet.goja.nl.eu.org!3.eu.feeder.erje.net!feeder.erje.net!fdn.fr!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.theory
Date: Thu, 5 Oct 2023 11:10:00 -0700 (PDT)
In-Reply-To: <6fc23e03-9d3b-482b-bbd6-3b7a1ed58640n@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=198.236.192.210; posting-account=iACVhwoAAAAxCNRb5QwwB44b3nqFpEM1
NNTP-Posting-Host: 198.236.192.210
References: <c08ef751-3844-41c4-984e-fd0f84d824ben@googlegroups.com>
<608b20b8-4a27-47ee-b5c6-ba3cf440a760n@googlegroups.com> <478d661f-34af-482c-bbd8-8da4a193c84dn@googlegroups.com>
<4583875e-e90e-428a-8d51-4dd79f13d003n@googlegroups.com> <f9f545f5-695c-45c3-92ef-41acec4cd921n@googlegroups.com>
<6fc23e03-9d3b-482b-bbd6-3b7a1ed58640n@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <06350f9e-63f6-40c2-8848-05ea80c15652n@googlegroups.com>
Subject: Re: benchmarks for model counting
From: theleasthappyfella@gmail.com (Jeffrey Rubard)
Injection-Date: Thu, 05 Oct 2023 18:10:00 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
 by: Jeffrey Rubard - Thu, 5 Oct 2023 18:10 UTC

On Thursday, October 5, 2023 at 11:09:12 AM UTC-7, Jeffrey Rubard wrote:
> On Wednesday, October 4, 2023 at 10:34:17 PM UTC-7, Daniel Pehoushek wrote:
> > On Wednesday, October 4, 2023 at 3:04:26 PM UTC-4, Jeffrey Rubard wrote:
> > > On Wednesday, October 4, 2023 at 8:48:21 AM UTC-7, Daniel Pehoushek wrote:
> > > > On Friday, September 22, 2023 at 2:04:49 PM UTC-4, Jeffrey Rubard wrote:
> > > > > On Thursday, September 14, 2023 at 10:35:04 AM UTC-7, Daniel Pehoushek wrote:
> > > > > > 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)]
> > > > > "Intellectual deception or chicanery".
> > > > i have worked for thirty years on satisfiability.
> > > > my program runs well on modest sizes of formulas.
> > > > avoid negation and prosper with truth.
> > > > daniel2380+++
> > > "Clap, clap, clap." #nowispnporwhat
> > 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+++
> "That's pretty special." #everyonesays

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

1
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor