Skip to content

CoreSMTSolver: sticky polarities #10

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.

Sign up for GitHub

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

Closed
aehyvari wants to merge 2 commits into from
Closed

CoreSMTSolver: sticky polarities #10

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
879f57a
CoreSMTSolver: sticky polarities
aehyvari Apr 4, 2022
fa2481f
CoreSMTSolver: Sticky polarities without inverse
aehyvari Apr 5, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion src/smtsolvers/CoreSMTSolver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -236,6 +236,7 @@ Var CoreSMTSolver::newVar(bool sign, bool dvar)
trail .capacity(v+1);
setDecisionVar(v, dvar);
polarity .push((char)sign);
saved_polar.push(true);

#if CACHE_POLARITY
prev_polarity.push(toInt(l_Undef));
Expand Down Expand Up @@ -406,6 +407,12 @@ void CoreSMTSolver::cancelUntil(int level)
{
if (decisionLevel() > level)
{
if (trail.size() > longest_trail) {
for (auto p : trail) {
saved_polar[var(p)] = not sign(p);
Copy link
Contributor

@blishko blishko Apr 5, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@msoos msoos Apr 5, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Owner Author

@aehyvari aehyvari Apr 5, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

}
longest_trail = trail.size();
}
for (int c = trail.size()-1; c >= trail_lim[level]; c--)
{
Var x = var(trail[c]);
Expand Down Expand Up @@ -570,7 +577,8 @@ Lit CoreSMTSolver::choosePolarity(Var next) {
}
switch ( polarity_mode ) {
case polarity_true:
sign = false;
// sign = false;
sign = saved_polar[next];
break;
case polarity_false:
sign = true;
Expand Down
2 changes: 2 additions & 0 deletions src/smtsolvers/CoreSMTSolver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -319,6 +319,8 @@ class CoreSMTSolver
double var_inc; // Amount to bump next variable with.
OccLists<Lit, vec<Watcher>, WatcherDeleted> watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<lbool> assigns; // The current assignments (lbool:s stored as char:s).
vec<bool> saved_polar;
int longest_trail = 0;
vec<bool> var_seen;
vec<char> polarity; // The preferred polarity of each variable.
vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
Expand Down