2020-07-19 13:48:58 (GMT)
@Hans-Jörg could you run your standard SMT benchmarks on the add-pos-saving-and-update-blit branch and compare it to the master branch? I implemented the scan-index optimisation (http://smt-workshop.cs.uiowa.edu/2020/paper_4.pdf) and I am curious if it makes any difference (the path of the SAT solver changes, so expect differences in the result)
2020-07-19 13:52:21 (GMT)
Do you know if the conflict minimization was ever implemented in veriT (http://fmv.jku.at/papers/SoerenssonBiere-SAT09.pdf)? I would expect that it helps for SMT too, but I am not certain…
2020-07-19 14:1:41 (GMT)
2020-07-20 10:15:59 (GMT)
Minimization is implemented and it does indeed significantly help.
2020-07-20 10:17:38 (GMT)
Then I must have missed it. Thanks!
2020-07-22 15:26:29 (GMT)
I'll put that on my todo list.
2020-07-23 14:27:49 (GMT)
I did some benchmarks (30s timeout). It looks like your changes have a clear benefit :octopus:. Results are here: https://schurr.io/sat-mathias/sat-mathias.html (https://schurr.io/sat-mathias/sat-mathias.tar.gz for the raw data)
2020-07-23 14:55:26 (GMT)
I don't see any difference in the curve "instances solved over time", but it solves more problems :octopus:
2020-07-23 14:57:50 (GMT)
Yeah that curve is often not useful.
2020-07-23 14:59:2 (GMT)
I wonder what happens in the QF_LIA/bofill-scheduling benchmarks
2020-07-23 15:4:32 (GMT)
I will have a look, but I guess that the SAT solver produces different models, so it takes longer to find the right model (that is also a model of the whole formula)
2020-07-23 15:11:13 (GMT)
Thanks, Mathias, for trying that out!
2020-07-24 15:34:48 (GMT)
@Hans-Jörg Am I doing something wrong? I expected to see some numbers, not how to format numbers in C...
./veriT -v -s /mnt/doc/repos/QF_LIA/bofill-scheduling/SMT_real_LIA/ex9700_2400_100.smt2
veriT-rmx (5fe72ca) - the SMT-solver veriT (UFRN/LORIA).
sat
STAT_FORM: lemmas/totality: %9d
STAT_FORM: insts/time: %7.2f
2020-07-27 8:17:58 (GMT)
This is surprising. Normally you should get three lists, one after another: A list of stat names with format strings (much longer than just two), then a list of stat names with a human readable description, and then the actual list. On my machine I got this. Which configure options are you using?
2020-07-27 9:5:51 (GMT)
Ahhh, I did not check that far… now I see the thing with the three lists (although I expected to see the number of SAT calls). Anyway, it is a weird format, but thanks
2020-07-27 9:12:10 (GMT)
yeah I'm not sure what the intention was when this was implemented. I assume it's to make it tool-readable, but then everything just uses the same format.
2020-07-27 19:8:51 (GMT)
I updated the results, now they are very odd https://schurr.io/sat-mathias/sat-mathias.html (https://schurr.io/sat-mathias/sat-mathias.tar.gz for the raw data). If you look at the raw data you can see that your version actually solves more, I'm not sure what the "min. timeout" means.
2020-07-28 4:40:9 (GMT)
I am a little confused… Column B is the last commit on the branch, but on my machine
$ time ./veriT -s QF_LIA/cut_lemmas/20-vars/cut_lemma_02_016.smt2
veriT-rmx (6dc114a) - the SMT-solver veriT (UFRN/LORIA).
unsat
./veriT -s /mnt/doc/repos/QF_LIA/cut_lemmas/20-vars/cut_lemma_02_016.smt2 0,41s user 0,00s system 99% cpu 0,414 total
(in debug mode!), while the output marks it as failed. valgrind does not complain about anything either. Any idea what is happening here?
2020-07-28 4:51:5 (GMT)
I can imagine my computer being faster and having more memory, but I cannot imagine that a deterministic SAT solver goes from 0.41 to more than 30s. And what is the timeout?
CPU limit : 30s
....
AUFLIA/20170829-Rodin/smt4311391195430732252.smt2
45.19 0 False
AUFLIA/20170829-Rodin/smt8553632888267276852.smt Failed 218.12 --- 0 --- False
UF/20170428-Barrett/cdt-cade2015/nada/afp/bindag/x2015_09_10_16_52_58_059_1025230.smt_in.smt Failed 346.58 --- 0 --- False
seem contradictory to me! This seem to happen only on the newer version for some reason.
2020-07-28 5:9:8 (GMT)
The timing is a different issue, but I don't think I have changed anything related to timers... At least not directly -- As far as I can see, the SAT solver is not interrupted during propagations, but that was already the case before. I am going to need help to reproduce that and to know what is the right behaviour. I cannot imagine that there is SAT operations taking real_time - timeout = 218.12s - 30s to happen, but who knows…
2020-07-28 7:49:2 (GMT)
gnah disregard this, I accidentally ran the experiment with the wrong solver path.
2020-07-28 7:54:1 (GMT)
that does not explain the timeout issue, right?
2020-07-28 13:6:20 (GMT)
it does a bit: the timeout setup doesn't really work reliably when the scheduler script is present and the wrong solver part used that
2020-07-30 13:20:34 (GMT)
So after the last changes this seems to not hurt and help a tiny bit so I merged it and ported it to mainline veriT.