Incremental interface

[vedadux]

Hi,

I have a project where I want to use ApproxMC to count the number of satisfying assignments. However, I have to make many, many such calls for very similar formulas. It is not feasible to create a new solver object, or write that many files to the file system. Would it be possible to extend ApproxMC with an incremental interface that supports assumptions, similar to the one used in SAT solvers?

Best regards , Vedad

[msoos]

Hi!

First of all, thanks for your request. You mention "similar" formulas. Can you elaborate? We first of all need to know if all you want to do is to add constraints, or also remove them, using assumptions. In other words, will the assumptions need to work? If not, I believe this may be easier to do.

Another question is how much overhead do you have to add the clauses to a new solver? Normally, the overhead to add clauses to a solver is minimal, so I'd like to know what's the ratio of adding the clauses vs counting solutions. Reading from files is almost always 100x-1000x slower for small/simple formulas, so I'm surprised you mention that. Have you tried using the C++ interface? Because taking the lower end, i.e. 100x speedup for small formulas, using the C++ interface may solve your issue, making the counting the most expensive part, and significantly improving your performance.

Note that formulas that are similar, but different enough, adding an incremental interface may help little, if any. This has been observed by e.g. Intel engineers about which they gave a presentation at the SAT Conference at Trento. So one must be careful -- only because a problem is similar doesn't mean that sharing the SAT solver will bring speed benefits. There are also downsides to sharing a common SAT solver, e.g. polluting the heuristics and retaining learnt clauses that may not be useful to a different CNF.

Looking forward to helping you out,

Mate

[vedadux]

Hi,

thanks for the reply! Essentially, I have one very large formula, where I need to perform model counting for certain subformulas it contains. To clarify this, imagine an adder circuit, where I need to do model counting for each of the gates in that circuit, given some assumptions.

What I used to do in another project is to add clauses that have an additional activation variable and then just activate them with an assumption when needed, and letting the SAT solver trivially satisfy them otherwise. I imagine, I will have to do something similar here.

Regarding the overhead: I am still at the start of the project and figuring out stuff as I go. With the current setup, I would have to create a new instance of the whole adder, or at least a cone of the gates required for one of the model counting tests.

For now, I think I will try some smaller examples with the expensive method and C++ interface and then report back to you, after some profiling.

Thank you, Vedad

[msoos]

Hi,

Thanks for the clarification! Please get back to us with the performance numbers. In our experience, counting is quite expensive (it's way more expensive than solving, as expected by theory). Creating a new instance of the whole adder may not be such a huge overhead in comparison, but it depends. Please get back to us so we understand the impact!

Thanks and looking forward to helping,

Mate

[msoos]

Closing because original reporter unfortunately did not come back with performance numbers :(