Ipasir solve final

[conp-solutions]

This is an RFC. I am happy to discuss whether there is another way to allow people to use simplification of solvers like MiniSat or Glucose without modifying those solvers.

In this example, only minisat220 can be used with the modified genipasat example binary. Before merging, the other solver backends should be extended accordingly.

[biotomas]

Hi Norbert, I understand your motivation to allow ipasir users to benefit from simplification techniques, however, I don't think this is the right way to do it. Here are my reasons:

I cannot think of any application of incremental SAT where solve_final would be useful because all applications I can think of fall into one of these e categories: 1, you do not know ahead which solve call is gonna be your final solve call (Planning, MaxSat, ...) 2, when you know ahead how many solves you will need, the last one is not expected to be harder than the average, so the performance benefit would be minimal 3, you only need one solve call, but that is not really an incremental application an you should just use a regular not incremental SAT solver.

However, I do not know about all the applications of incremental SAT, so if you can provide me with some examples where solve_final would be useful, I would be happy to learn about it.

A perhaps better approach would be to introduce something similar to Armin's freeze/unfreeze variables technique but that is also not ideal.

What would be ideal and what we should strive for is to do simplification in such a way that interface/user does not need to know about it all. So for example if simplification removes some variables at the first solve call and some clauses or assumptions are added that contain removed variables, the solver should be able to deal with it (for example by reverting the simplification to some degree or whatever else).

[conp-solutions]

I agree that in an ideal world, SAT solvers should be able to hide simplification from users. If I remember correctly, there are only 2 or 3 systems around that can actually do that. All MiniSat based solvers are not capable of doing that, and since 2014 nothing happened on that front, to the best of my knowledge.

What I would like to achieve by adding this function is to make simplification available for a subset of possible use cases. IPASIR enabled solvers can be used as a backend for any tool, incremental or non-incremental does not matter. However, those users can currently not benefit from simplification (for most systems), because the usual interface does not allow to enable the currently available simplification in general.

The new function targets exactly these use cases where the caller knows exactly that the solver is called once; and where the caller still wants to be able to easily switch and test SAT back ends. While that does not cover Maxsat or MUS, model checking and SMT might be covered. To me it feels more effective to enable some people quickly and boost their use cases, in comparison to waiting for the more difficult changes to be implemented in many SAT solvers.

[conp-solutions]

To make backwards compatibility a thing, have you thought about how to support solvers that implement only "older" functions of the ipasir interface?

[biotomas]

There is no doubt it would be convenient and useful for the single solve call applications but there are so many other convenient and useful features and if we keep changing the interface too often it will be hard for SAT solvers to support.

If we update the IPASIR interface it should be done at most once a year and connected to some event (like the SAT competition) so that everyone notices. It should also be done in agreement with the community. Perhaps we should create some kind of survey and ask which features the users would like to see and which features would the solver authors be willing to implement.

I don't know how to make backwards compatibility work with a C header file. Do you have any idea?

[biotomas]

Backwards compatibility could be perhaps done via macros? something like

ifdef IPASIR_SOLVE_FINAL

int ipasir_solve_final();

endif

[conp-solutions]

I have updated the commits, and added one that introduces a macro IPASIR_VERSION, which then allows to easily specify the needs of an application (v1 without learned clause sharing, v2 with learn sharing, v3 with solve_final).

I do not use IPASIR for incremental search only, but also to allow integrating another SAT solver into some application easily. These applications, e.g. CBMC as submitted to last years incremental track, actually call the solver only once. The application is also aware of this, and hence, should be allowed to tell the solver, so that the solver could make the most out of it.

Again, I agree, in an ideal world, each solver would be capable of running simplification during incremental calls. However, that's not reality. To allow to use what is currently there, I therefore recommend to extend the interface definition.

With respect to the speed of changing the interface: I am not inclined to wait for competitions to update the version. This year, there was none, and nobody can give guarantees for next year. What should be done is to announce changes, e.g. via satlive. Having several people that steer where to go with the interface is a good idea, but only if the process is quick and simple. Those people should come from both SAT development as well as applications. I am happy to have discussions about the current extension, but actually feel the need of applications being able to use the preprocessor today.

Best, Norbert