Generate full Dimacs files

[fabian-kruse]

Hello,
I am using cadical on a series of very similar formulas with the goal of proving them unsatisfiable. For this I use the IPASIR interface of cadical. Generally, I have two questions:

1. Since I try to solve similar formulas, I read in the part of the formula that is the same for all of them using the add(int lit) function of the IPASIR interface. Then I use the the assume(int lit) function to include a set of literals in the next solve() call. For the next call I then assume a different set of cubes. My problem here is, that I would like to generate a drat proof file for every call of the solve() function, but cadical requires me to pass a single file after initilizing the solver. Is there a way to generate individual files? If not, I would need to parse the larger part of the formula for every call, which would disallow the advantage of an incremental solver.

2. Secondly, I would like to very the generated drat proof with drat trim. However, drat trim also requires the original dimacs formula as an additional input. Since I used the IPASIR interface, I never actually generated the formulas as individual files and preferably would like to do so with the help of cadical. Cadical has a funcion write_dimacs() which generates a simplified formula (which is great), but since my formulas should be unsatisfiable the simplified formulas consist of an empty formula. Is there a way to generate the initial formula?

Kind regards

[arminbiere]

Sorry for the late answer, but I did not see this until now. Combining proofs with incremental solving is not officially supported yet as several design issues are unsolved, i.e., how to use extension variables and also, what you seemed to be interested, how to stitch together pieces of DRAT proofs, even though I learned that there is a TACAS'23 paper coming up with Marijn Heule as co-author, which faced and solved similar issues in the context of generating proofs for distributed SAT solving with CaDiCaL.