-
Notifications
You must be signed in to change notification settings - Fork 7
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Tie-break heuristic overflow #5
Comments
Yeah, that makes sense. However, I just tried this change out on a branch and it is very detrimental to the instance you mentioned (5 sec CaDiCaL on master 22668af, ... more than 120 sec CaDiCaL on
Here? I think I agree, it should already be in Lines 826 to 830 in 22668af
|
Changing to So, as you said, maybe for this given instance the heuristic is detrimental. I think it would be interesting to have different tie-breaking heuristics (a portfolio), however it is difficult to judge which reduced formula is better, the number of deleted clauses ? Launching a solver for each and see who advances faster ? I tested with local search, but the randomness makes the conclusion not reliable.
Yes, I was talking about this code. I apologize, I forgot to cite it. I think that this loop should have already added the variable in question since we delete clauses containing it.
|
Hello, first of all I'd like to congratulate you on your excellent work. I'm currently studying your implementation to integrate it into the Painless framework and I've noted some remarks that I'd like your opinion on. While testing with the instance "0336f81b60baac5b8f481dd3c32861a5-mod4block_2vars_10gates_u2_autoenc-sc2009" of the SAT2023 competition I noticed that the calculation of the tie-break heuristic value overflows to the negative numbers. It would make more sense to use an
unsigned
(maybe aulong
to less likely hit 0) as the return type, wouldn't it?On another note, I'd like to know if the addition of the current variable is redundant given that it is surely present in the
listUpdate
set.That's it, normally I've covered everything I wanted your opinion on.
Best regards.
The text was updated successfully, but these errors were encountered: