Parallelize DIMACS formula printing

[srogatch]

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[martin-cs]

Thanks for this PR. Adding threads to CBMC would be quite a big architectural step. It is not out of the question but I think it would need quite a significant use-case. Can you talk a little more about why you need this functionality and how it works in a wider context? Printing dimacs is not normally a particularly time-critical step, esp. compared with solving. Does having multiple threads really give a significant speed up over, say, outputting to a file on a RAM disk?

[martin-cs]

Please don't add asserts, use the various variants of INVARIANT.

[srogatch]

Thanks for this PR. Adding threads to CBMC would be quite a big architectural step. It is not out of the question but I think it would need quite a significant use-case. Can you talk a little more about why you need this functionality and how it works in a wider context? Printing dimacs is not normally a particularly time-critical step, esp. compared with solving. Does having multiple threads really give a significant speed up over, say, outputting to a file on a RAM disk?

Sure, thanks for taking a look! DIMACS printing indeed takes a considerable time: CBMC converts my program into a boolean formula in ~200 seconds, then something else is going on (don't remember for how much - I think it's converting to SSA taking ~70 seconds), then 12GB of the formula are written to disk at the speed of ~50MBytes per second on a super-fast SSD with a single thread. So that takes ~240 seconds. Then kissat solves the formula in ~600 seconds (because the formula is easy and has probable solutions with a random assignment of some variables). So DIMACS printing in a single thread takes as much as the rest of the processing (except the solver), and it is not bound by the SSD speed (SSD is PCIE-4.0 with up to 7GBytes per second transfers, 1 million IOPS). The printing is bound by C++ stream speed (conversion from binary values to text). With multithreading, on a 128 logical core CPU (Ryzen Threadripper 3990X) I get the speed of writing to the disk about 4GBytes/second, so the formula gets saved in a few seconds.

[martin-cs]

Sure, thanks for taking a look! DIMACS printing indeed takes a considerable time: CBMC converts my program into a boolean formula in ~200 seconds, then something else is going on (don't remember for how much - I think it's converting to SSA taking ~70 seconds),

The option `--timestamp monotonic` can help for this kind of application level profiling.

then 12GB of the formula are written to disk at the speed of ~50MBytes per second on a super-fast SSD with a single thread. So that takes ~240 seconds. Then kissat solves the formula in ~600 seconds (because the formula is easy and has probable solutions with a random assignment of some variables).

OK; thanks for the timings, that really helps with the context.

So DIMACS printing in a single thread takes as much as the rest of the processing (except the solver), and it is not bound by the SSD speed (SSD is PCIE-4.0 with up to 7GBytes per second transfers, 1 million IOPS). The printing is bound by C++ stream speed (conversion from binary values to text). On a 128 logical thread CPU (Ryzen Threadripper 3990X) I get the speed of writing to the disk about 4GBytes/second, so the formula gets saved in a few seconds.

At the risk of sounding ungrateful, have you considered: 1. Profiling the printing part of the code and seeing if we can optimise it at all? If we could remove the bottleneck it might be better than adding more compute to it. 2. Integrating Kissat as a SAT back-end so that the output to DIMACS is not needed at all? I think @natasha-jeppu was using kissat ( #5494 ) so I think it can be done.

[martin-cs]

#6439 is an example of adding support for a new SAT solver.

[srogatch]

At the risk of sounding ungrateful, have you considered: 1. Profiling the printing part of the code and seeing if we can optimise it at all? If we could remove the bottleneck it might be better than adding more compute to it. 2. Integrating Kissat as a SAT back-end so that the output to DIMACS is not needed at all? I think @natasha-jeppu was using kissat ( #5494 ) so I think it can be done.

1. I didn't profile it, but I know from experience that streams in C++ (and even C) are extremely slow. Only a custom printing routine could help, that would convert integers to strings in an efficient way. Still I think this routine will not achieve the speed of multiple cores.
2. In that PR the author used kissat via DIMACS formula printing. kissat is not yet ready for integration: not all the API is exposed.