features I'd like to see ...

[mattginsberg]

int ipasir_failed(void * solver, int lit);
current behavior: considers literals that contributed to a proof of unsatisfiability and returns 1 or 0 depending on whether or not the given literal was in the set

suggested behavior: if lit was in the set, return lit. If -lit was in the set, return -lit. Otherwise, return 0.

Suggested addition:

void ipasir_reset(void * solver);

Put the solver in a state where it can be called again (perhaps assumptions changed, new clause added, whatever). For cadical, this would mean clearing the unsat flag and also the failed field of all of the Flags. Other solves may obviously be different. Does not clear the X set (see below) but does clear any indication of the associated nogood.

Hoped-for addition:

void ipasir_setx(void * solver, unsigned var);
void ipasir_clearx(void * solver, unsigned var);

The solver is expected to maintain a set X of variables. If at any point a nogood is derived that consists only of variables in the X set, the prover is expected to stop early and return failure, with ipasir_failed then usable to find the actual nogood. This turns out to be very useful in a variety of situations. Very easy modification for every solver that I understand.

bool ipasir_supportsx(void *solver);
Returns true if the above functionality is supported and false if it is not.

void ipasir_log (void * solver, bool doit);
to allow the user to turn logging on and off, however the solver supports that, if at all?

[Udopia]

Thanks for reaching out! You suggest a lot of things, so I would like to respond point by point:

• ipasir_reset(): There is no need for such a method. IPASIR is an API for incremental solvers, so the specification already takes into account adding clauses and changing assumptions between solve() calls (e.g. state transition from UNSAT to INPUT). This already works in cadical, which implements IPASIR.

• ipasir_setx(), ipasir_clearx(), ipasir_supportsx: This functionality is subsumed by ipasir2_export. Whenever, a nogood is learned, and the export callback is set, the nogood can be analyzed in the export callback (e.g. whether it is a subset of X) and then the solver can potentially be interrupted with the terminate callback.

• ipasir_log(): This looks more like a possible addition to the ipasir2 options.

• ipasir_failed(): Interesting suggestion, I tend to include this (one way or another) in the specification of ipasir2_failed().

Thanks again. Let me know if you need help using the export callback to observe nogood variables.

[mattginsberg]

Hi Markus: That all makes sense, although I needed to write ipasir_reset() for my current stuff because various fields *weren't* being reset by solve(). Maybe I was supposed to call terminate() and didn't know it? I can certainly look at the code and see. Meanwhile, is it possible for someone to let me know when there is a stable version of cadical that supports ipasir2? I don't check often, and cadical conflicts with Google's coding standards in a variety of annoying ways (i.e., Google has pretty much turned LOG into a keyword, uses .cc instead of .cpp, etc). So I'll want to only upgrade to the new cadical once! Thanks so much -- Matt

…

On Tue, Oct 10, 2023 at 1:19 AM Markus Iser ***@***.***> wrote: Dear Matt, thanks for reaching out! You suggest a lot of things, so I would like to respond point by point: - ipasir_reset(): There is no need for such a method. IPASIR is an API for incremental solvers, so the specification already takes into account adding clauses and changing assumptions between solve() calls (e.g. state transition from UNSAT to INPUT). This already works in cadical, which implements IPASIR. - ipasir_setx(), ipasir_clearx(), ipasir_supportsx: This functionality is subsumed by ipasir2_export. Whenever, a nogood is learned, and the export callback is set, the nogood can be analyzed in the export callback (e.g. whether it is a subset of X) and then the solver can potentially be interrupted with the terminate callback. - ipasir_log(): This looks more like a possible addition to the ipasir2 options. - ipasir_failed(): Interesting suggestion, I tend to include this (one way or another) in the specification of ipasir2_failed(). Thanks again. Let me know if you need help using the export callback to observe nogood variables. — Reply to this email directly, view it on GitHub <#36 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFKAGHMBEZN4HYUPJV7EH3DX6UAHJAVCNFSM6AAAAAA5Y4Z2QWVHI2DSMVQWIX3LMV43SRDJONRXK43TNFXW4Q3PNVWWK3TUHM3TEMZYGI2DK> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[Udopia]

Dear Matt,
afaik, Cadical comes with a solid implementation of IPASIR. If there are any issues with fields not being reset that should be reset, please contact the authors of Cadical, they are probably happy to get informed. Regarding IPASIR-2, let us just polish the specification, and then after the next SAT competition, I hope to see several implementations of IPASIR-2.
All the best,
Markus

[mattginsberg]

Sounds good. Thanks! Matt

…

On Wed, Oct 11, 2023 at 1:34 AM Markus Iser ***@***.***> wrote: Dear Matt, afaik, Cadical comes with a solid implementation of IPASIR. If there are any issues with fields not being reset that should be reset, please contact the authors of Cadical, they are probably happy to get informed. Regarding IPASIR-2, let us just polish the specification, and then after the next SAT competition, I hope to see several implementations of IPASIR-2. All the best, Markus — Reply to this email directly, view it on GitHub <#36 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFKAGHMICBZKRWQ43E2OHLLX6ZKY7ANCNFSM6AAAAAA5Y4Z2QU> . You are receiving this because you authored the thread.Message ID: ***@***.***>