1package solver23import "sort"45// clauseSorter is a structure to facilitate the sorting of lits in a learned clause6// according to their respective decision levels.7type clauseSorter struct {8 lits []Lit9 model Model10}1112func (cs *clauseSorter) Len() int { return len(cs.lits) }13func (cs *clauseSorter) Less(i, j int) bool {14 return abs(cs.model[cs.lits[i].Var()]) > abs(cs.model[cs.lits[j].Var()])15}16func (cs *clauseSorter) Swap(i, j int) { cs.lits[i], cs.lits[j] = cs.lits[j], cs.lits[i] }1718// sortLiterals sorts the literals depending on the decision level they were bound19// i.e. abs(model[lits[i]]) <= abs(model[lits[i+1]]).20func sortLiterals(lits []Lit, model []decLevel) {21 cs := &clauseSorter{lits, model}22 sort.Sort(cs)23}