Extracting statistics from the solver

[m-fleury]

Currently IPASIR gives a generic way to set options, but no way to actually read statistics (number of conflicts, number of decisions, minimized clauses, ...). Should there be such an interface? This is the kind of things that might be useful for example during parallel solving to see if some configuration is doing something strange.

(This was requested for CaDiCaL arminbiere/cadical#50)

[Udopia]

Access to statistics is also on the wish list for IPASIR-2. The specification of a statistics interface did not make it into the final draft because we tried to keep the implementation effort small and not introduce too much new stuff. Therefore, we have chosen only three items, of which the configuration interface is the most extensive change and at the same time offers the greatest variety of possible applications.

We expect the specification of a statistics interface to be similarly extensive as that of the configuration interface. I'm not sure what the mood is among solver authors right now to deal with even more specification. In the end, we probably all want the new IPASIR_E_UNSUPPORTED error code to be used as rarely as possible.

[m-fleury]

I like the concern for all the people implementing that. But I think that I would prefer that you define the function with a name and a type than let everyone who needs it come up with a new (subtly incompatible) function.

But: I do not see how IPASIR2_E_UNSUPPORTED solves any problem here... If it is a value you cannot distinguish it from a valid numeric value.

[Udopia]

All ipasir2 methods return an error code, and IPASIR2_E_UNSUPPORTED is here to allow solver implementers to postpone implementation of methods which do not belong to a core set of methods (will be specified). Any other return values are returned by output parameters, so no distinction based on value ranges is required.

I'm curious how other SAT solver developers think about adding a statistics interface. Personally, I would defer this to a later extension of ipasir2.