meelgroup / arjun

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

In case there are many independent variables the --backbone 0 doesn't help #1

Closed msoos closed 2 years ago

msoos commented 4 years ago

In particular, ./arjun min_broken.cnf --xor 0 gives:

c [mis] Start unknown size: 4833
c [mis] iter:   160 T/F/U: 161/0/0    by:   1 U:    4672 I:     161 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:   321 T/F/U: 161/0/0    by:   1 U:    4511 I:     322 N:       0 backb avg:    0.0 backb max:      0 T: 0.18
c [mis] iter:   482 T/F/U: 161/0/0    by:   1 U:    4350 I:     483 N:       0 backb avg:    0.0 backb max:      0 T: 0.18
c [mis] iter:   643 T/F/U: 161/0/0    by:   1 U:    4189 I:     644 N:       0 backb avg:    0.0 backb max:      0 T: 0.18
c [mis] iter:   804 T/F/U: 161/0/0    by:   1 U:    4028 I:     805 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:   965 T/F/U: 161/0/0    by:   1 U:    3867 I:     966 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  1126 T/F/U: 161/0/0    by:   1 U:    3706 I:    1127 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  1287 T/F/U: 161/0/0    by:   1 U:    3545 I:    1288 N:       0 backb avg:    0.0 backb max:      0 T: 0.18
c [mis] iter:  1448 T/F/U: 161/0/0    by:   1 U:    3384 I:    1449 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  1609 T/F/U: 161/0/0    by:   1 U:    3223 I:    1610 N:       0 backb avg:    0.0 backb max:      0 T: 0.18
c [mis] iter:  1770 T/F/U: 161/0/0    by:   1 U:    3062 I:    1771 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  1931 T/F/U: 161/0/0    by:   1 U:    2901 I:    1932 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  2092 T/F/U: 161/0/0    by:   1 U:    2740 I:    2093 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  2253 T/F/U: 161/0/0    by:   1 U:    2579 I:    2254 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  2414 T/F/U: 161/0/0    by:   1 U:    2418 I:    2415 N:       0 backb avg:    0.0 backb max:      0 T: 0.20
c [mis] iter:  2575 T/F/U: 161/0/0    by:   1 U:    2257 I:    2576 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  2736 T/F/U: 161/0/0    by:   1 U:    2096 I:    2737 N:       0 backb avg:    0.0 backb max:      0 T: 0.18
c [mis] iter:  2897 T/F/U: 161/0/0    by:   1 U:    1935 I:    2898 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  3058 T/F/U: 161/0/0    by:   1 U:    1774 I:    3059 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  3219 T/F/U: 161/0/0    by:   1 U:    1613 I:    3220 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  3380 T/F/U: 161/0/0    by:   1 U:    1452 I:    3381 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  3541 T/F/U: 161/0/0    by:   1 U:    1291 I:    3542 N:       0 backb avg:    0.0 backb max:      0 T: 0.19
c [mis] iter:  3702 T/F/U: 161/0/0    by:   1 U:    1130 I:    3703 N:       0 backb avg:    0.0 backb max:      0 T: 0.20
c [mis] iter:  3863 T/F/U: 161/0/0    by:   1 U:     483 I:    3864 N:     486 backb avg:    3.0 backb max:     98 T: 0.23
c [mis] iter:  4024 T/F/U: 161/0/0    by:   1 U:      26 I:    4025 N:     782 backb avg:    1.8 backb max:     99 T: 0.23
c [mis] backward round finished T: 4.81

Check out the backb max being 0 for a long while. That makes backb ineffective, and forces us to pass a huge vector every time, copying it, etc. That slows us down by a factor of 1.5x

msoos commented 2 years ago

Stale issue, closing.