search

arminbiere / kissat

MIT License
452 stars 85 forks source link

kissat is using CPU time (not wall time) for stats? #22

Closed jwaldmann closed 2 years ago

jwaldmann commented 2 years ago

I am running several kissat solver instances concurrently, via IPASIR, from one (Haskell) main program. When I switch on verbose logging, the seconds column of kissat output increases (much) faster than real time.

Could it be that kissat uses CPU time for this? Should it be wall time?

Is this number used elsewhere besides logging? Perhaps for time-out?

Example: a long-running such process, containing 10 kissat instances, main programm killed, prints

...
c ? 85843.06 630 87 100 1172 93920 2 27281595 222077 48% 37 24901 1204 15%
c } 85841.94 596 86 102 1202 97658 2 28347427 235795 49% 37 24841 1197 15%
c ? 85841.94 596 86 102 1202 97658 2 28347427 235795 49% 37 24841 1197 15%
c ] 85842.67 560 82 107 1287 106876 1 31360910 252378 51% 34 24725 1178 14%
c ? 85842.67 560 86 107 1287 106876 2 31360910 252378 48% 38 24725 1178 14%

real    144m21.859s
user    1427m6.330s
sys     3m38.234s

note that 1427 min (user time) is 85620 seconds (roughly what's in the log)

arminbiere commented 2 years ago

Thanks for bringing this up. I have just released the SC2022 competition versions and now have time to take on some of recent issues. For CaDiCaL an (industrial) user reported exactly the same issue, i.e., what type of time 'wall-clock' or 'real-time' should be used for statistics and reporting and after some back-and-forth we came to the conclusion that 'it depends'. Therefore I have added a '--realtime' option to CaDiCaL which lets the user choose and in addition am careful when reporting time to also tell the user which of the two are actually used. For Kissat I was too lazy to port this solution, but if you really need it, I can add this option too (and quality appropriately messages which talk about 'time'). Otherwise this first column in those 'report' message (see 'report.c' for more information) is just fixed to use 'kissat_time' which then is fixed to 'kissat_process_time' at this point. Would you like this option?

jwaldmann commented 2 years ago

Hi. Thanks for explaining. I was just confused by the output. I don't use kissat's time information programmatically, so there's no need to change anything. I only wrote the report because it might have been a bug.

arminbiere commented 2 years ago

Ok, then I close this (for now).