Large Performance Overhead during Initialization

[SimonKlx]

Hello,

i am using CaDiCal as a backend for the Bitwuzla SMT solver.
Currently i am benchmarking my program and trying to optimize it for runtime.
When generating a flame graph i realized that the majority of the time that bitwuzla is running is spend in the initialization step of CaDiCal.
I am by no means an expert in memory management or very low level C, but judging from the functions that the time is spend in and looking at the code it feels like there is a lot of resizing happening whenever a new variable is initialized leading to a lot of costly memory operations.

This might be some kind of niche problem, since we are checking very many, but relatively easy to solve queries.
However it feels wrong that the initialization takes more time than the actual solving.
When i think about this problem, i would iterate over the whole Term an then allocate the vector size that i need only once.
Am i missing something?

Just by briefly looking at the code i was not able to understand everything, but maybe you can tell whether this is a hard problem to solve or if you have thought about this before.

I attached two screenshots from the flamegraph showing the time spend in each function.

Thanks,

Simon

[m-fleury]

If you already know how many variables you need or have an estimate, you could use the reserve function (https://github.com/arminbiere/cadical/blob/master/src/cadical.hpp#L522) to bypass the resizing that is currently done (using std::vector::resize whenever new variables are added).

[arminbiere]

To avoid this memory thrashing is one of the reasons I actually started Kissat with a completely new memory layout. Porting this improved memory handling back to CaDiCaL is impossible, so I fear you have to go for reserve.

[mpreiner]

@SimonKlx Can you share the benchmark you are using to produce this flame graph? I want to have a look whether we can improve this on the Bitwuzla side.

[arminbiere]

We are also discussing a non-determinism introduced by the use of reserve (different behavior with and without) which could be considered a fix for this issue (on the user side).

The proposal at least would be to rename reserve to resize in case we can not get rid of this nondeterminism (due to pushing variables on the decision queue during the current variant).