Commits

Alexandru Moșoi  committed e0b0806

vsids: tests several literals before deciding.

  • Participants
  • Parent commits bf63847

Comments (0)

Files changed (1)

File lib/vsids.go

 	"flag"
 	"fmt"
 	"sort"
+	"math"
 )
 
 var gvsidsscale = flag.Float64("gvsidsscale", 1.05, "how much to scale scores conflict")
+var gvsidschecks = flag.Int("gvsidschecks", 4, "how many unassigned literals to test")
 
 type VSIDS struct {
 	NumDecisions int
 // Finds first unassigned.
 func (v *VSIDS) Decide(ls LiteralSet) Literal {
 	v.NumDecisions++
+
+	checked := *gvsidschecks
+	bestPos := -1
+	bestScore := float32(-math.MaxFloat32)
+
 	for i, literal := range v.literals {
 		if ls.IsAssigned(literal) {
 			continue
 			continue
 		}
 
-		v.literals[0], v.literals[i] = v.literals[i], v.literals[0]
-		v.literals[0] = literal
-		return literal
+		if v.scores[literal.Var()] > bestScore {
+			bestScore = v.scores[literal.Var()]
+			bestPos = i
+		}
+
+		if checked--; checked == 0 {
+			break
+		}
 	}
-	panic("nothing to branch on")
+
+	if bestPos == -1 {
+		panic("nothing to branch on")
+	}
+
+	v.literals[0], v.literals[bestPos] = v.literals[bestPos], v.literals[0]
+	return v.literals[0]
 }
 
 // Implements the sort interface.