search

kperun / SATPrakPDW

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

No longer contract all candidates to find the bestContractionCandidate #58

Open Verdict7 opened 7 years ago

Verdict7 commented 7 years ago

This is probably one of the main reasons why big problems are extremely slow. Implementation ideas: Save contraction candidates in a priority queue (that is created once in the beginning) sorted by history/ some random factor/ other ideas?/... Only contract variables in the queue until one is found that is above the gainThreshold (or some other thresholds) and ignore the rest (for now. Later maybe with best of three, or look at a fixed relative number of candidates). Update the queue by removing the best candidate, recalculating the history value, and inserting it again.

DavidWz commented 7 years ago

Pseudo code to clarify: CC* getBestCC(priority_queue<CC*>& activeCCs) { CC* best = activeCCs.pop(); IntervalT newInterval = best.getContractedInterval(); best.updateHistory(newInterval); activeCCs.insert(best); return best; }

kperun commented 7 years ago

@DavidWz This has been implemented in the experimental branch. Please take a look at it, since I am not really sure if the behaves as intended.

Verdict7 commented 7 years ago

Update after dddcb5d1f0c16668adfbb16487c552a636eca5d7: There was a severe bug in the comparator (it always returned truthy...), this was fixed and the best of 5 method implemented. It seems to work quite well. Todo: