CMS 3.x: Use "c ########### cls for eliminated var x ### start" as hint for new run?

[capiman]

In irred file there is a section for eliminated variables and blockedClauses. Would it be helpful to parse "c ########### cls for eliminated var x ### start" as hint for a new run?

Information would not be very big (e.g. my current example CNF had 178 variable eliminated). At startup this info can be used once to put collected blocked clauses due to eliminated variables back to Simplifier::blockedClauses

[msoos]

It would be fund, but it won't be robust to do that. I'd rather just re-eliminate them. It's fast to do it, max a couple of seconds. Whereas reading it back and filling the datastructures is a LOT of hassle, at least a 100 lines of code with of course at least 3-4 bugs. I'd rather not introduce one more complexity into the system. It's complicated enough already (almost 30K lines of code)

[capiman]

In my cases (with bigger and more difficult CNFs) it takes hours to reach the same point again. But if it is too difficult and problematic due to errors, let's forget it. It was only an idea which came to my mind during testing.

[capiman]

Just to give an example, perhaps i interpret the logfile wrong:

First run:

I start with (starts with 16807 of 17056 total variables)

c 1 302 16807 75K 2266 11874K 78.6 300 1 0 509.0 c new bins since last SCC: 11874725 free vars %:70653.45 c [clean] T: 0.3900 s c SCC new: 0 T: 0.14 s c 9 1103 16807 75K 2266 11874K 78.6 1086 4 1 610.1 c 14 1904 16807 75K 2266 11874K 78.6 1877 7 1 761.6 c 15 2705 16807 75K 2266 11874K 78.6 2666 8 1 820.0 c 19 3506 16807 75K 2266 11874K 78.6 3453 11 2 877.8 ... c #var-elim: 37 c #var-elim: 3 c #var-elim: 4 c #var-elim: 3 c #var-elim: 3 c #var-elim: 3 c #var-elim: 3 c #var-elim: 4 c #var-elim: 1 c #var-elim: 1 c #var-elim: 2 c #var-elim: 2

Then I abort the run. This is the display just before end of run and exporting of red/irred files:

c 17376 3284K 16741 75K 2263 11813K 80.0 536K 2176 16141 1507.9 c 17382 3285K 16741 75K 2263 11813K 80.0 537K 2176 16141 1509.3

New I take the irred file and start again: (starts again with 16807 of 17056 total variables)

c 1 302 16807 75K 2265 11867K 78.4 300 1 0 442.3 c new bins since last SCC: 11867039 free vars %:70607.72 c [clean] T: 0.3750 s c SCC new: 0 T: 0.12 s c 8 1103 16807 75K 2265 11867K 78.4 1094 3 0 705.5 c 13 1904 16807 75K 2265 11867K 78.4 1886 4 2 796.8 c 16 2705 16807 75K 2265 11867K 78.4 2680 4 2 772.1 ... c #var-elim: 37 // same as above c #var-elim: 3 // same as above c #var-elim: 4 // same as above c #var-elim: 3 // same as above c #var-elim: 4 // The last 4 is 1 better than in previous run, there we had a 3 ... c 1413 290K 16756 78K 2265 11831K 81.0 30K 462 8431 394.8 c 1420 290K 16756 78K 2265 11831K 81.0 30K 462 8431 419.9

(This is at timestamp ~ 15 Minutes)

I had assumed a more or less big fast jump to 16741, instead of slowly going to 16756.