More incrementality features?

[alexeyignatiev]

Hi Armin,

Are there chances that kissat will have a basic "assumptions" interface and be able to report unsatisfiable cores?

Best,
Alexey

[arminbiere]

Incremental solving is one of the next features I consider to add, but I will first add a model based tester which is also useful for better testing and debugging in the first place. Both will take quite some time though and I do not expect it to happen before fall.

[alexeyignatiev]

Great, thank you!

[danielsn]

+1

[whaaswijk]

+1

[MontyThibault]

+1

[wangdongxuking61]

+1

[arminbiere]

This is still pending, but one of the main motivations version 'sc2022-light' which is the last version submitted to the competition on the main branch, is to reduce features as much as possible, i.e., removing code, in order to simplify supporting incremental reasoning. But all still on the TODO stack right now without ETA.

[Geremia]

@arminbiere What's the current status of IPASIR implementation?

[arminbiere]

As discussed before, getting Kissat incremental requires a major effort. I do not see this to happen soon. If you rely on incremental solving I would suggest to use CaDiCaL instead.

[Geremia]

@arminbiere Thanks. I'll try CaDiCaL. Is that the currently best incremental solver?