solving ( A && ( B || C )) in stages?

[Johannes Waldmann]

Dear all,

I want a satisfying assignment
of a formula ( A && ( B || C ))
where A, B, C are CNFs that share variables,
but B and C are independent in the sense that
the common variables of B and C already occur in A.

The plan is to run minisat on A && B first,
and if this turns out to be unsat (or takes too much time),
then on A && C.

Is there a way (using Minisat API)
to pre-process A (e.g., learn some clauses),
save the resulting solver state S,
so it can be used as a starting poing
for solving both A && B and A && C ?

One could even imagine to run two minisat instances
for these two, both starting in S
but working independently from then on.

Best regards, J.W.

[a_tom]

if you want to utilize the assignment for some variables you can always pass them as assumptions. but in your case I think it'd be valid only of the common set of variables exist as identical clauses in both of the formulas.