CoreSMTSolver: sticky polarities #10
Conversation
src/smtsolvers/CoreSMTSolver.cc
Outdated
| { | ||
| if (trail.size() > longest_trail) { | ||
| for (auto p : trail) { | ||
| saved_polar[var(p)] = not sign(p); |
There was a problem hiding this comment.
Why do you save negation of sign here? I thought the idea was to save the discovered polarity and use that, not it's negation.
There was a problem hiding this comment.
Funnily enough, both can be useful(!?), it's weird. Going for its negation can help with UNSAT. However, you are right, the initial intuition is to not negate it... but either can work(!). Strange. Paper:
http://fmv.jku.at/papers/BiereFleury-POS20.pdf
Note phase ‘I', i.e. the inverted phase. However, likely we should try it without inversion, too.
There was a problem hiding this comment.
Yes, I think we got a slightly better result yesterday for our one test instance with the negated polarity, and it's the version that was on my disk, so I ran that. I'll check the "intuitive" version quickly as well.
|
Can you also try #11 maybe? It's a bit of a more hackish hack 😆 Mate |
Experiments on sticky polarities.
With negation, against master in
QF_UFWithout negation, against master in
QF_UF