Which header files are required for incremental solving? (Also, how to extract unsat cores?)

[realharryhero]

Hello,

In the CaDiCaL solver, a header file gives an API to incrementally add and remove variables. I would like to add and remove variables similarly to the CaDiCaL solver, but there doesn't seem to be a specific file which does this, or a clear example as how it would be done. How could I do so, with an API similar to CaDiCaL?

The idea for this would be to use this incremental solving to replace the CaDiCaL component in the EvalMaxSAT solver by replacing the cadicalinterface.h file (in which the mentioned header file is often used) with an interface for ParaFROST to create a MaxSAT GPU solver. Thank you!

(Also, any advice on how to extract unsat cores when the SAT problem is found unsatisfiable through ParaFROST?)

[muhos]

Hello,

Thanks for the message!

I see. In ParaFROST, you could do something similar using the IPASIR standard interface. The API is given here: ipasir.hpp.

After inspecting cadicalinterface.h, looks like the goal was to provide something similar to MiniSAT interface. However, IPASIR is richer and should work with every solver in the community.

Currently, extracting UNSAT cores is only possible though function table simplification method which is limited to a subset of variables/clauses. I'm planning to provide this feature soon on the input formula level (all clauses).