1package solver23const (4 nbMaxRecent = 50 // How many recent LBD values we consider; "X" in papers about LBD.5 triggerRestartK = 0.86 nbMaxTrail = 5_000 // How many elements in queueTrail we consider; "Y" in papers about LBD.7 postponeRestartT = 1.48)910type queueData struct {11 totalNb int // Current total nb of values considered12 totalSum int // Sum of all values so far13 nbRecent int // NB of values used in the array14 ptr int // current index of oldest value in the array15 recentAvg float64 // Average value16}1718// lbdStats is a structure dealing with recent LBD evolutions.19type lbdStats struct {20 lbdData queueData21 trailData queueData22 recentVals [nbMaxRecent]int // Last LBD values23 recentTrails [nbMaxTrail]int // Last trail lengths24}2526// mustRestart is true iff recent LBDs are much smaller on average than average of all LBDs.27func (l *lbdStats) mustRestart() bool {28 if l.lbdData.nbRecent < nbMaxRecent {29 return false30 }31 return l.lbdData.recentAvg*triggerRestartK > float64(l.lbdData.totalSum)/float64(l.lbdData.totalNb)32}3334// addConflict adds information about a conflict that just happened.35func (l *lbdStats) addConflict(trailSz int) {36 td := &l.trailData37 td.totalNb++38 td.totalSum += trailSz39 if td.nbRecent < nbMaxTrail {40 l.recentTrails[td.nbRecent] = trailSz41 old := float64(td.nbRecent)42 new := old + 143 td.recentAvg = (td.recentAvg*old)/new + float64(trailSz)/new44 td.nbRecent++45 } else {46 old := l.recentTrails[td.ptr]47 l.recentTrails[td.ptr] = trailSz48 td.ptr++49 if td.ptr == nbMaxTrail {50 td.ptr = 051 }52 td.recentAvg = td.recentAvg - float64(old)/nbMaxTrail + float64(trailSz)/nbMaxTrail53 }54 if td.nbRecent == nbMaxTrail && l.lbdData.nbRecent == nbMaxRecent && trailSz > int(postponeRestartT*td.recentAvg) {55 // Too many good assignments: postpone restart56 l.clear()57 }5859}6061// addLbd adds information about a recent learned clause's LBD.62// TODO: this is very close to addConflicts's code, this should probably be rewritten/merged.63func (l *lbdStats) addLbd(lbd int) {64 ld := &l.lbdData65 ld.totalNb++66 ld.totalSum += lbd67 if ld.nbRecent < nbMaxRecent {68 l.recentVals[ld.nbRecent] = lbd69 old := float64(ld.nbRecent)70 new := old + 171 ld.recentAvg = (ld.recentAvg*old)/new + float64(lbd)/new72 ld.nbRecent++73 } else {74 old := l.recentVals[ld.ptr]75 l.recentVals[ld.ptr] = lbd76 ld.ptr++77 if ld.ptr == nbMaxRecent {78 ld.ptr = 079 }80 ld.recentAvg = ld.recentAvg - float64(old)/nbMaxRecent + float64(lbd)/nbMaxRecent81 }82}8384// clear clears last values. It should be called after a restart.85func (l *lbdStats) clear() {86 l.lbdData.ptr = 087 l.lbdData.nbRecent = 088 l.lbdData.recentAvg = 0.089}