Single or multiple instances

[Hao Zheng]

I implemented Bradley's IC3 model checking algorithms based on Minisat. In my implementation, I use multiple minisat instances, one for each frame. My implementation is quite slow compared to the original ic3, which uses a single instance for all frames. My question is which option is better, using single instance or multiple instances in in an incremental solving process such as the IC3 model checking, and why.

I really appreciate your response.

Hao

[John Backes]

Hi Hao,

The Berkeley ABC implementation of IC3 (referred to as PDR) uses Minisat
and is much faster than the original implementation of IC3. The
implementation of PDR has the option of using a monolithic SAT instance,
but by default uses different SAT instances for each time frame. Part
of the reason for this is to only include logic relevant for proving a
proof obligation (or the property) in each frame. Most of the power of
PDR (IC3) comes from how well the generalization step is performed.
Perhaps there are some optimizations in your implementation that you are
not using? e.g., ternary valued simulation, generalization by MUC
inspection, restarting the instances corresponding to each from when the
number of learned clauses reaches a threshold, etc ...?

- John

[Niklas Een]

The performance difference between the single-SAT and multi-SAT versions
of IC3 is very small in my experience. I think something else is missing
in your implementation.

// N.

[Hao Zheng]

Thank you Very much for your responses. So one of my concerns is removed, and I can focus on other part of the implementation to look for problems.

Hao