2020-04-15 16:2:49 (GMT)
I have been trying to process strored data for HOUnif,
and I realized that old (?) solves the most unique problems
2020-04-15 16:3:10 (GMT)
after thinking a bit about it, it amkes perfect sense, since the other configurations that are better solve more or less the same problems
2020-04-15 16:3:34 (GMT)
But then when I checked which are those problems on which old is better, I realized new configurations now solve them all!
2020-04-15 16:3:51 (GMT)
SO I will need to reevaluate all the results
2020-04-15 16:4:14 (GMT)
@Jasmin Blanchette this is OK for the camera ready version, right?
We have done something like that before I think.
2020-04-15 16:4:16 (GMT)
What is "old"?
2020-04-15 16:4:26 (GMT)
your old implementation of JP
2020-04-15 16:4:36 (GMT)
this is how we call the configuration...
2020-04-15 16:4:57 (GMT)
and all of them are solved after 7+ seconds, which says it is only about the order in whcih clauses are returned
2020-04-15 16:6:31 (GMT)
So the new configurations that solve them all are not in the paper currently?
2020-04-15 16:8:5 (GMT)
What probably happened is that in the mean time the prover changed enough
2020-04-15 16:8:14 (GMT)
so that the effects that made old prove this problem were removed
2020-04-15 16:8:30 (GMT)
because I really suspect this is due to some clause order problem
2020-04-15 16:8:42 (GMT)
and I have been playing with the streams in the mean time
2020-04-15 16:9:44 (GMT)
ok, sure. I don't think this is a problem for the camera ready version. We can inform the chairs about it, but I think most people wouldn't even do that.
2020-04-15 16:9:57 (GMT)
Sure
2020-04-15 19:24:58 (GMT)
Answering Petar: Sure. You could tell the chairs if you have cold feet but in my experience they don't care and will say "go!"