BUGFIX-66

Bug 59: Who Watches The Watcher?

This is a rudimentary Boolean satisfiability (SAT) solver that watches one literal per clause.
The algorithm is nearly the same as Algorithm 7.2.2.2B from The Art of Computer Programming.
A Boolean formula is provided in conjunctive normal form. Its variables are numbered 0, 1, ..., nvar-1.
Literals are integers: The least-significant bit encodes the polarity; higher bits encode the variable.
A literal with polarity bit 1 is negated. Such a literal is true if and only if its variable is false.
Clauses are numbered 0, 1, ..., len(locs)-2. Each clause has one or more consecutive literals in lits.
The first literal of clause i is lits[locs[i]] and the last literal of clause i is lits[locs[i+1]-1].
The solver backtracks through partial assignments, rejecting any assignment that falsifies a clause.
A satisfying assignment is returned as a slice of nvar integers, each integer 0 (false) or 1 (true).
A nil slice is returned if and only if the formula is unsatisfiable.

Fix The Tiny Bug In This Go Code:

func sat(nvar int, lits, locs []int) []int { var ( assn = make([]int, nvar) head = make([]int, nvar*2) ncls = len(locs) - 1 tail = make([]int, ncls) ) for lit := range head { head[lit] = -1 } for cls, first := range locs[:ncls] { lit := lits[first] tail[cls] = head[lit] head[lit] = cls } for var1 := 0; var1 < nvar; var1++ { falseLit := var1 * 2 if head[falseLit] >= 0 && head[falseLit+1] < 0 { assn[var1] = 1 falseLit++ } for cls := head[falseLit]; ; { if cls < 0 { head[falseLit] = cls break } var ( first = locs[cls] past = locs[cls+1] ) for at := first; ; { if at++; at < past { var ( lit = lits[at] var2 = lit >> 1 ) if var2 <= var1 && (assn[var2]^lit)&1 != 0 { continue } lits[at] = falseLit lits[first] = lit next := tail[cls] tail[cls] = head[lit] head[lit] = cls cls = next break } head[falseLit] = cls was := assn[var1] for ; was >= 2; was = assn[var1] { assn[var1] = 0 if var1--; var1 < 0 { return nil } } assn[var1] = was ^ 3 falseLit = var1*2 + 1 - was cls = head[falseLit] break } } } for var1 := range assn { assn[var1] &= 1 } return assn }

To receive a hint, submit unfixed code.