search

arminbiere / kissat

MIT License
452 stars 85 forks source link

kissat 4.0.0 doesn't compile with `--compact` flag #54

Closed firefighterduck closed 1 month ago

firefighterduck commented 1 month ago

The new version 4.0.0 that was submitted to this years SAT competition (btw. congratulations on the amazing win) does not compile if the --compact flag is enabled (also if --extreme or --ultimate are enabled). To be more precise the new factor.c file contains two occurrences where the SIZE_STACK macro is used on watches, which does not work in the case of the compact representation.

https://github.com/arminbiere/kissat/blob/faa674e324b76c3348b34f40beaa0b9d821b84c2/src/factor.c#L273 https://github.com/arminbiere/kissat/blob/faa674e324b76c3348b34f40beaa0b9d821b84c2/src/factor.c#L562

arminbiere commented 1 month ago

Thanks for spotting this. I have not been using '--compact' much lately since it seems to limit the capacity of the solver too much. This is a non-default configuration parameter anyhow used to reduce memory usage a bit, even though Kissat is anyhow much more compact than other solvers (2-4 more compact than CaDiCaL for instance). I will check whether this feature is necessary still.

arminbiere commented 1 month ago

BTW, for this year' competition the '--competition' configuration forces only '--no-options' and '--quiet'.

firefighterduck commented 1 month ago

Tbh I don't know whether the --compact flag makes any difference/sense for my use case of kissat, I just used the --ultimate flag, since it sounds like the best option out-of-the-box.

arminbiere commented 1 month ago

Probably should reevaluate and drop those if they are not useful actually (as I expect). Having them is obviously misleading.

Armin

FireFighterDuck @.***> schrieb am Mi., 11. Sept. 2024, 13:05:

Tbh I don't know whether the --compact flag makes any difference/sense for my use case of kissat, I just used the --ultimate flag, since it sounds like the best option out-of-the-box.

— Reply to this email directly, view it on GitHub https://github.com/arminbiere/kissat/issues/54#issuecomment-2343327748, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFA2SAKHLV5XQU7L5JVYT23ZWAPWNAVCNFSM6AAAAABOANHFVWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNBTGMZDONZUHA . You are receiving this because you commented.Message ID: @.***>

arminbiere commented 1 month ago

Fixed in release 4.0.1.