kperun / SATPrakPDW

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

Improve getBestSplitVariable #29

Closed DavidWz closed 7 years ago

DavidWz commented 7 years ago

If you run the solver on the polypaver example, you will see it splits the biggest interval of the slack variable a lot of times.

Maybe we can improve this behavior by choosing the biggest interval of original variables. Should we even split slack variable bounds?

This needs testing.

Verdict7 commented 7 years ago

@kperun Last commit did not compile, there was a "{" missing after the if. Also: Contraction should still be possible with slack variables, only splitting should prefer original variables.