search

kperun / SATPrakPDW

Interval Constraint Propagation strategy implementation for SMTRAT
MIT License
2 stars 0 forks source link

Choosing the splitting variable: Look at unsatisfied constraints #43

Closed Verdict7 closed 7 years ago

Verdict7 commented 7 years ago

Maybe instead of taking the variable with the largest interval as splitting candidate, we should look at the guessed solution using current intervals (that we create anyway before splitting) and choose a variable from a condition that is not yet satisfied.

kperun commented 7 years ago

@Verdict7 so, you propose a system where we select the splitting candidate not according to the biggest interval, but if it sat or not? I think it is worth a try, but here it would be even better to combine both techniques: select from all UNSAT variables the one with the biggest interval. What do you think?

kperun commented 7 years ago

@Verdict7 issue has been solved. Now, whenever we have to find the best split candidate, we first check which variables are currently not satisfied (here we guess a solution). For all variables which are part of a not satisfied constraint, we select the one with the biggest interval as the best split candidate.