search

meelgroup / arjun

CNF minimizer and minimal independent set calculator
Other
15 stars 3 forks source link

Sometimes, we produce worse output than B+E #6

Closed msoos closed 1 year ago

msoos commented 1 year ago

Without --xorgate 0 --orgate 0 --itegate 0 --irreggate 0 --sort 10 we get:

./bpluse-compare.sh faster_with_be/wage_circuit_div.t1.i18.777adaa9.stp.cnf
Running on CNF file faster_with_be/wage_circuit_div.t1.i18.777adaa9.stp.cnf
Running Arjun...
1.88user 0.01system 0:01.89elapsed 99%CPU (0avgtext+0avgdata 28372maxresident)k
0inputs+168outputs (0major+6320minor)pagefaults 0swaps
Running BPE (new, compiled)
0.89user 0.00system 0:00.89elapsed 99%CPU (0avgtext+0avgdata 16364maxresident)k
0inputs+944outputs (0major+2603minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars      839     num (non-set) vars      774
num cls                4365     num cls                3810
num bin cls             285     num bin cls             184
max cl size              20     max cl size              36
avg non-bin cl sz      4.1      avg non-bin cl sz      4.5
num (non-unit) lits   21600     num (non-unit) lits   20342

With --xorgate 0 --orgate 0 --itegate 0 --irreggate 0 --sort 10 we get:

 ./bpluse-compare.sh faster_with_be/wage_circuit_div.t1.i18.777adaa9.stp.cnf
Running on CNF file faster_with_be/wage_circuit_div.t1.i18.777adaa9.stp.cnf
Running Arjun...
1.30user 0.00system 0:01.30elapsed 99%CPU (0avgtext+0avgdata 21156maxresident)k
0inputs+136outputs (0major+3534minor)pagefaults 0swaps
Running BPE (new, compiled)
0.90user 0.00system 0:00.90elapsed 100%CPU (0avgtext+0avgdata 14556maxresident)k
0inputs+944outputs (0major+3344minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars      765     num (non-set) vars      774
num cls                3723     num cls                3810
num bin cls             202     num bin cls             184
max cl size              20     max cl size              36
avg non-bin cl sz      3.8      avg non-bin cl sz      4.5
num (non-unit) lits   17669     num (non-unit) lits   20342

Pinging @arijitsh since he reported the issue. This issue on GitHub is to make sure the issue is not lost.

Likely fix:

maxzinkus commented 1 year ago

wage_circuit_div oh I’m so happy to see my benchmarks are showing up in perf tests!!

msoos commented 1 year ago

Thanks :) These files have been very helpful!

amm-hhk2008-2.c issues

It seems like the above set of options fixes almost all issues, but we are still left with the file amm-hhk2008-2.c. Below is a partial analysis of this file with Arjun/BPE.

Arjun (with new options) time:

c [arjun] final set size:           98 percent of original: 0.2076 %
c [arjun] of which empty occs:       0 percent of original: 0.0000 %
c [arjun] finished T: 91.21         [[projection set calc]]
[...simplification here.......]
c [arjun] Done dumping. T: 164.6130 [[total, projection+simp]]

(this was actually with --fastb 0 but that's very similar, just somewhat slower, 1st number should be about 74 seconds instead)

BPE total time:

        Command being timed: "./BiPe -preproc faster_with_be/amm-hhk2008-2.c.stp.cnf"
        User time (seconds): 219.37
        Maximum resident set size (kbytes): 310388

So we are approx the same time for projection set calculation (74s with --fastb 1 vs below BPE number of 72.830734s for bipartition calc), and faster overall. However, BPE calculates a bipartition of size 68(!!) versus our 98. This seems to lead to a SIGNIFICANTLY worse final simplified CNF. See below.

Arjun simplification CNF output:

num (non-set) vars    12267
num cls              126622
num bin cls           39867
max cl size              20
avg non-bin cl sz      8.0
num (non-unit) lits  900876

BPE simplification CNF output:

num (non-set) vars     3400
num cls               50058
num bin cls           34967
max cl size             504
avg non-bin cl sz     60.9
num (non-unit) lits 1038966

Intermediate output from BPE:

c Number of input variables computed: 65
c Time to compute the bi-partition: 72.830734
c
c Number of variables forgotten: 43817
c Number of iterations: 5
c
c Vivification, total time: 21.465217
c Vivification, number of clauses removed: 17088
c Vivification, number of literals removed: 11451
c
c Occurrence Elimination, total time: 0.000000
c Occurrence Elimination, number of literals removed: 0
c Time used for the preprocessing step: 33.691124
msoos commented 1 year ago

I can now get the file faster_with_be/amm-hhk2008-2.c.stp.cnf have the same number of independent variables as BPE. Using d770ebba59f95e1bd7b3cb987309d47159c44c03 this only requires 

./arjun --sort 10 faster_with_be/amm-hhk2008-2.c.stp.cnf --maxc 5000 --empty 1 
[...]
c [arjun] final set size:           67 percent of original: 0.1419 %
c [arjun] of which empty occs:       1 percent of original: 0.0021 %
c [arjun] finished T: 83.54

Notice that's missing --gates 0. With --gates 0 we get:

./arjun --sort 10 faster_with_be/amm-hhk2008-2.c.stp.cnf --maxc 5000 --empty 1  --gates 0
[...]
c [arjun] final set size:           88 percent of original: 0.1864 %
c [arjun] of which empty occs:       1 percent of original: 0.0021 %
c [arjun] finished T: 68.60

So this is quite OK. The BPE output for the same part is:

c Time to sort the selector: 0.050546
c The number of computed gates is: 0
c Number of input variables computed: 65
c Time to compute the bi-partition: 72.341808

So especially with --gates 1 we get quite close to this, only 3 variables off.

However, the minimized instance is still WAAAAY worse:

Arjun                      vs             BPE
num (non-set) vars    12003     num (non-set) vars     3400
num cls              167245     num cls               50058
num bin cls           38414     num bin cls           34967
max cl size              20     max cl size             504
avg non-bin cl sz      6.7      avg non-bin cl sz     60.9
num (non-unit) lits 1109142     num (non-unit) lits 1038966

(this is with --gates 0)

The --gates 0 and wage_circuit_div.t1.i18.777adaa9.stp.cnf files

Unfortunately, --gates 0 breaks faster_with_be/wage_circuit_div.t1.i18.777adaa9.stp.cnf:

./arjun --sort 10 faster_with_be/wage_circuit_div.t1.i18.777adaa9.stp.cnf --maxc 5000 --empty 1    
c [arjun] final set size:          227 percent of original: 10.9874 %
c [arjun] of which empty occs:       1 percent of original: 0.0484 %

vs

./arjun --sort 10 faster_with_be/wage_circuit_div.t1.i18.777adaa9.stp.cnf --maxc 5000 --empty 1 --gates 0
[...]
c [arjun] final set size:          181 percent of original: 8.7609 %
c [arjun] of which empty occs:       1 percent of original: 0.0484 %
msoos commented 1 year ago

Curiously enough, if I take the original CNF, faster_with_be/amm-hhk2008-2.c.stp.cnf, add the computed c ind, and push that through ./arjun tmp.cnf --backward 0 out4 (disabling independent variable computing), I'm getting a way smaller CNF:

./count_literals.py out4
num (non-set) vars     4546
num cls               60853
num bin cls           30089
max cl size              20
avg non-bin cl sz      7.4
num (non-unit) lits  348311

Not quite BPE level, but close. I have a feeling this is some weird interaction with the solver or something.

msoos commented 1 year ago

I now took the c ind generated with --empty 1 --gates 1:

$ diff tmp.cnf faster_with_be/amm-hhk2008-2.c.stp.cnf
3d2
< c ind 1 3049 3050 47552 47553 47554 47555 47556 47587 47524 47586 47589 47621 47585 47526 47558 47584 47591 47623 47615 47645 47643 47641 47639 47637 47635 47633 47631 47629 47627 47625 47624 47562 47580 47578 47576 47574 47572 47570 47568 47566 47564 47582 47592 47550 47549 47548 47547 47546 47545 47544 47543 47542 47541 47540 47539 47538 47537 47536 47535 47534 47533 47532 47531 47530 47529 47583 0

and plugged it back into Arjun. The independent vars is not much lower, however...

./arjun tmp.cnf out4 --maxc 5000 --empty 1 --gates 0
c [arjun] Done dumping. T: 102.5970
[...]
c [arjun] final set size:           66 percent of original: 98.5075 %
c [arjun] of which empty occs:       1 percent of original: 1.4925 %
c [arjun] finished T: 3.27
c [arjun] Done dumping. T: 102.5970
$ ./count_literals.py out4
num (non-set) vars     2689
num cls               32104
num bin cls           17930
max cl size              20
avg non-bin cl sz      6.0
num (non-unit) lits  153499

So there is something really off. With --gates 1 I can get here (note that the c ind was created with --gates 1):

$ ./arjun tmp.cnf --backward 0 out3 --empty 1
[...]
c [arjun] final set size:           67 percent of original: 100.0000 %
c [arjun] of which empty occs:       1 percent of original: 1.4925 %
c [arjun] finished T: 2.12
[...]
c [arjun] Done dumping. T: 116.5244
$ ./count_literals.py out3
num (non-set) vars     3769
num cls               50102
num bin cls           28899
max cl size              20
avg non-bin cl sz      6.6
num (non-unit) lits  248357

My guess right now is that during backwards we inadvertently simplify the problem and that leads to a much worse final CNF. We need to disable simplifications during backwards maybe?

msoos commented 1 year ago

OK, we are good now, with bcdc4a7aeb860cdd7370302635a38fffc8678f80

./bpluse-compare.sh amm-hhk2008-2.c.stp.cnf
Running on CNF file amm-hhk2008-2.c.stp.cnf
Running Arjun...
Executing: ./arjun  amm-hhk2008-2.c.stp.cnf-noind amm-hhk2008-2.c.stp.cnf-noind-simplified-arjun
190.56user 0.29system 3:10.97elapsed 99%CPU (0avgtext+0avgdata 612000maxresident)k
0inputs+2328outputs (0major+163996minor)pagefaults 0swaps
Running BPE (new, compiled)
216.75user 0.18system 3:37.10elapsed 99%CPU (0avgtext+0avgdata 310480maxresident)k
0inputs+16144outputs (0major+29051minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars     3675     num (non-set) vars     3400
num cls               45122     num cls               50058
num bin cls           27050     num bin cls           34967
max cl size              20     max cl size             504
avg non-bin cl sz      7.5      avg non-bin cl sz     60.9
num (non-unit) lits  235409     num (non-unit) lits 1038966

Notice that while we have about 8% more varaibles, we have less than 1/4 of the number of literals. The number of literals substantially affects the performance of the system, and should result in our system being FAR faster with GANAK.

We have also retained our performance on wage_circuit..., see:

./bpluse-compare.sh wage_circuit_div.t1.i18.777adaa9.stp.cnf          
Running on CNF file wage_circuit_div.t1.i18.777adaa9.stp.cnf
Running Arjun...
Executing: ./arjun  wage_circuit_div.t1.i18.777adaa9.stp.cnf-noind wage_circuit_div.t1.i18.777adaa9.stp.cnf-noind-simplified-arjun
1.31user 0.00system 0:01.31elapsed 99%CPU (0avgtext+0avgdata 20932maxresident)k
0inputs+208outputs (0major+4379minor)pagefaults 0swaps
Running BPE (new, compiled)
0.94user 0.00system 0:00.94elapsed 99%CPU (0avgtext+0avgdata 16508maxresident)k
0inputs+280outputs (0major+3099minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars      760     num (non-set) vars      774
num cls                3726     num cls                3810
num bin cls             193     num bin cls             184
max cl size              20     max cl size              36
avg non-bin cl sz      3.9      avg non-bin cl sz      4.5
num (non-unit) lits   17808     num (non-unit) lits   20342

All other interesting CNFs are also correctly minimized:

./bpluse-compare.sh pollard.cnf
Running on CNF file pollard.cnf
Running Arjun...
Executing: ./arjun  pollard.cnf-noind pollard.cnf-noind-simplified-arjun
19.32user 0.01system 0:19.35elapsed 99%CPU (0avgtext+0avgdata 59632maxresident)k
0inputs+200outputs (0major+14022minor)pagefaults 0swaps
Running BPE (new, compiled)
3.69user 0.00system 0:03.70elapsed 99%CPU (0avgtext+0avgdata 22520maxresident)k
0inputs+944outputs (0major+3898minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars      511     num (non-set) vars      595
num cls                3210     num cls                6737
num bin cls             562     num bin cls            1664
max cl size              20     max cl size              54
avg non-bin cl sz      4.4      avg non-bin cl sz     11.6
num (non-unit) lits   15875     num (non-unit) lits   68992

./bpluse-compare.sh ProcessBean.cnf                                ✔ 
Running on CNF file ProcessBean.cnf
Running Arjun...
Executing: ./arjun  ProcessBean.cnf-noind ProcessBean.cnf-noind-simplified-arjun
0.45user 0.00system 0:00.45elapsed 99%CPU (0avgtext+0avgdata 21132maxresident)k
0inputs+104outputs (0major+3869minor)pagefaults 0swaps
Running BPE (new, compiled)
0.63user 0.01system 0:00.64elapsed 100%CPU (0avgtext+0avgdata 9760maxresident)k
0inputs+216outputs (0major+1688minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars      339     num (non-set) vars      399
num cls                1156     num cls                1408
num bin cls             560     num bin cls             696
max cl size              16     max cl size              17
avg non-bin cl sz      5.0      avg non-bin cl sz      5.3
num (non-unit) lits    5256     num (non-unit) lits    6549
./bpluse-compare.sh track1_116.mcc2020_cnf                         ✔ 

Running on CNF file track1_116.mcc2020_cnf
Running Arjun...
Executing: ./arjun  track1_116.mcc2020_cnf-noind track1_116.mcc2020_cnf-noind-simplified-arjun
19.34user 0.02system 0:19.38elapsed 99%CPU (0avgtext+0avgdata 52536maxresident)k
0inputs+264outputs (0major+15910minor)pagefaults 0swaps
Running BPE (new, compiled)
3.24user 0.00system 0:03.24elapsed 99%CPU (0avgtext+0avgdata 33372maxresident)k
0inputs+616outputs (0major+6164minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars     1166     num (non-set) vars     1572
num cls                5785     num cls                9055
num bin cls            1032     num bin cls            1470
max cl size              35     max cl size              35
avg non-bin cl sz      3.6      avg non-bin cl sz      4.2
num (non-unit) lits   25172     num (non-unit) lits   43970
./bpluse-compare.sh blasted_TR_b14_even3_linear.cnf.gz.no_w.cnf    ✔  23s 
Running on CNF file blasted_TR_b14_even3_linear.cnf.gz.no_w.cnf
Running Arjun...
Executing: ./arjun  blasted_TR_b14_even3_linear.cnf.gz.no_w.cnf-noind blasted_TR_b14_even3_linear.cnf.gz.no_w.cnf-noind-simplified-arjun
7.58user 0.01system 0:07.61elapsed 99%CPU (0avgtext+0avgdata 74400maxresident)k
0inputs+464outputs (0major+18646minor)pagefaults 0swaps
Running BPE (new, compiled)
9.08user 0.02system 0:09.11elapsed 99%CPU (0avgtext+0avgdata 30084maxresident)k
0inputs+968outputs (0major+6923minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars     1651     num (non-set) vars     1859
num cls                9799     num cls               10615
num bin cls            1132     num bin cls            1880
max cl size              20     max cl size              49
avg non-bin cl sz      4.3      avg non-bin cl sz      5.4
num (non-unit) lits   49087     num (non-unit) lits   61382
msoos commented 1 year ago

OK, I have now slightly improved all relevant CNF's performance. We sometimes have higher number of variables, but substantially less literals, or slightly higher number of literals, but substantially less variables. So overall, this should be better.

./bpluse-compare.sh amm-hhk2008-2.c.stp.cnf --sort 1            ✔ 
Running on CNF file amm-hhk2008-2.c.stp.cnf
Running Arjun...
Executing: ./arjun --sort 1 amm-hhk2008-2.c.stp.cnf-noind amm-hhk2008-2.c.stp.cnf-noind-simplified-arjun
191.15user 0.25system 3:11.56elapsed 99%CPU (0avgtext+0avgdata 614384maxresident)k
0inputs+2232outputs (0major+157994minor)pagefaults 0swaps
Running BPE (new, compiled)
217.85user 0.16system 3:38.26elapsed 99%CPU (0avgtext+0avgdata 310556maxresident)k
0inputs+16144outputs (0major+27358minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars     3694     num (non-set) vars     3400
num cls               44683     num cls               50058
num bin cls           27685     num bin cls           34967
max cl size              20     max cl size             504
avg non-bin cl sz      7.4      avg non-bin cl sz     60.9
num (non-unit) lits  225384     num (non-unit) lits 1038966
./bpluse-compare.sh wage_circuit_div.t1.i18.777adaa9.stp.cnf --sort 1
Running on CNF file wage_circuit_div.t1.i18.777adaa9.stp.cnf
Running Arjun...
Executing: ./arjun --sort 1 wage_circuit_div.t1.i18.777adaa9.stp.cnf-noind wage_circuit_div.t1.i18.777adaa9.stp.cnf-noind-simplified-arjun
1.35user 0.00system 0:01.35elapsed 99%CPU (0avgtext+0avgdata 21428maxresident)k
0inputs+200outputs (0major+4532minor)pagefaults 0swaps
Running BPE (new, compiled)
0.95user 0.00system 0:00.96elapsed 99%CPU (0avgtext+0avgdata 16700maxresident)k
0inputs+280outputs (0major+3164minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars      757     num (non-set) vars      774
num cls                3714     num cls                3810
num bin cls             193     num bin cls             184
max cl size              20     max cl size              36
avg non-bin cl sz      3.9      avg non-bin cl sz      4.5
num (non-unit) lits   17760     num (non-unit) lits   20342
./bpluse-compare.sh pollard.cnf --sort 1                        ✔ 
Running on CNF file pollard.cnf
Running Arjun...
Executing: ./arjun --sort 1 pollard.cnf-noind pollard.cnf-noind-simplified-arjun
17.55user 0.01system 0:17.58elapsed 99%CPU (0avgtext+0avgdata 74096maxresident)k
0inputs+192outputs (0major+14613minor)pagefaults 0swaps
Running BPE (new, compiled)
3.69user 0.01system 0:03.70elapsed 99%CPU (0avgtext+0avgdata 21800maxresident)k
0inputs+944outputs (0major+4230minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars      445     num (non-set) vars      595
num cls                2987     num cls                6737
num bin cls             420     num bin cls            1664
max cl size              20     max cl size              54
avg non-bin cl sz      4.4      avg non-bin cl sz     11.6
num (non-unit) lits   15106     num (non-unit) lits   68992

./bpluse-compare.sh ProcessBean.cnf --sort 1                         INT ✘ 
Running on CNF file ProcessBean.cnf
Running Arjun...
Executing: ./arjun --sort 1 ProcessBean.cnf-noind ProcessBean.cnf-noind-simplified-arjun
0.48user 0.01system 0:00.49elapsed 100%CPU (0avgtext+0avgdata 21352maxresident)k
0inputs+104outputs (0major+3953minor)pagefaults 0swaps
Running BPE (new, compiled)
0.63user 0.00system 0:00.64elapsed 99%CPU (0avgtext+0avgdata 11920maxresident)k
0inputs+216outputs (0major+1652minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars      327     num (non-set) vars      399
num cls                1147     num cls                1408
num bin cls             521     num bin cls             696
max cl size              16     max cl size              17
avg non-bin cl sz      4.7      avg non-bin cl sz      5.3
num (non-unit) lits    5161     num (non-unit) lits    6549
./bpluse-compare.sh track1_116.mcc2020_cnf --sort 1                ✔  20s 
Running on CNF file track1_116.mcc2020_cnf
Running Arjun...
Executing: ./arjun --sort 1 track1_116.mcc2020_cnf-noind track1_116.mcc2020_cnf-noind-simplified-arjun
15.79user 0.05system 0:15.85elapsed 99%CPU (0avgtext+0avgdata 51672maxresident)k
0inputs+264outputs (0major+105456minor)pagefaults 0swaps
Running BPE (new, compiled)
3.22user 0.00system 0:03.24elapsed 99%CPU (0avgtext+0avgdata 33108maxresident)k
0inputs+608outputs (0major+5530minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars     1162     num (non-set) vars     1572
num cls                5777     num cls                9055
num bin cls            1029     num bin cls            1470
max cl size              35     max cl size              35
avg non-bin cl sz      3.7      avg non-bin cl sz      4.2
num (non-unit) lits   25187     num (non-unit) lits   43970
./bpluse-compare.sh blasted_TR_b14_even3_linear.cnf.gz.no_w.cnf --sort 1
Running on CNF file blasted_TR_b14_even3_linear.cnf.gz.no_w.cnf
Running Arjun...
Executing: ./arjun --sort 1 blasted_TR_b14_even3_linear.cnf.gz.no_w.cnf-noind blasted_TR_b14_even3_linear.cnf.gz.no_w.cnf-noind-simplified-arjun
7.42user 0.01system 0:07.44elapsed 99%CPU (0avgtext+0avgdata 75152maxresident)k
0inputs+480outputs (0major+18101minor)pagefaults 0swaps
Running BPE (new, compiled)
9.29user 0.01system 0:09.31elapsed 99%CPU (0avgtext+0avgdata 28504maxresident)k
0inputs+968outputs (0major+7097minor)pagefaults 0swaps
ARJUN vs BPE (new, compiled)
num (non-set) vars     1510     num (non-set) vars     1859
num cls                9373     num cls               10615
num bin cls            1127     num bin cls            1880
max cl size              20     max cl size              49
avg non-bin cl sz      4.9      avg non-bin cl sz      5.4
num (non-unit) lits   52349     num (non-unit) lits   61382