output simplified formula

[marijnheule]

It would be great if kissat could emit the simplified formula after setting some limit, such as --conflicts, similar to CaDiCAL's -o option.

[arminbiere]

This is now available with '-o' in the 4.0.x releases.

[srogatch]

Can you output the formula still when kissat -o is terminated by Ctrl+C?

[arminbiere]

In principle the search (and all the inprocessors) whould be able to gracefully terminate as soon the solver is flagged to terminate. But as they might be in an inconsistent state, they might stillneed some additional time to fix things up. So it will be not immediate termination of the solve call but close, maybe with the exception of huge formulas. This part is even tested (with coverage checking). But due to the delay and it is unclear what the user wants "interrupt and kill the process completely" or "interrupt and still write" I think one would need some additional options to force writing, even under control-c. Another option would be to always write it the process receives another signal (like SIG_USR1). Can you elaborate on the scenario where you want to use it, so that I could design the correct approach?

[srogatch]

Thanks for looking into this. I think instead of a different signal, it's much easier to use flag e.g. -oo instead of plain -o. The scenario is as follow:

• I manually monitor the progress of kissat, or with a script parsing kissat ouput
• As soon as the unsolved %% fall below a certain threshold (e.g. 47%), I want to write the simplified formula
• So either myself or with a script I send normal signal (SIGTERM) e.g. by pressing Ctrl+C
• Kissat should write the simplified formula before exiting

The stop conditions may vary, e.g. no output from kissat for 30 seconds, number of vars remaining is below a threshold, %% below threshold, etc.
Please, let me know if I can provide more info.