kperun / SATPrakPDW

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

Try to guess a solution before performing a manual split #38

Closed DavidWz closed 7 years ago

DavidWz commented 7 years ago

In many cases we will split a variable because the gain is too small, but all diameters are still too large. In this case, the reason might simply be that the solution space is very large for that problem. We might detect this by trying to guess a solution before we apply a manual split. And only perform the split if we could not find a solution.

kperun commented 7 years ago

@DavidWz Enhancement implemented. Now, whenever a split has to occur, we first try to guess a solution and if a model is found, we just terminate and assign the model to the corresponding attribute, otherwise we just resume as before and perform a split.