Strash index was always calculated at 0, leading to 100% collisions

[ecordell]

This is how the structural hash in gini is computed:

gini/logic/c.go

Line 379 in a1a5030

return uint32((a << 13) * b)

But when it’s used, it’s used “mod capacity” of the nodes - which are always multiples of 2. The index into the strash array is always a*2^13*b % 2^n which is 0 for n<13:

gini/logic/c.go

Lines 268 to 271 in a1a5030

	c := strashCode(a, b)
	l := uint32(cap(p.nodes))
	i := c % l
	si := p.strash[i]

gini/logic/c.go

Lines 285 to 287 in a1a5030

	k := c % uint32(cap(p.nodes))
	m.n = p.strash[k]
	p.strash[k] = j

and leads to 100% collisions on the table - it will always try to store in index 0 and have to walk back through the node links.

To fix this, I changed the index calculation to strash % (cap - 1)

I added a small benchmark that uses the existing sudoku example as a sanity check:

// before
BenchmarkSudoku-12    	     894	   1752632 ns/op
// after
BenchmarkSudoku-12    	     741	   1467374 ns/op

which is a ~15% speedup.

(I'm sure there are much better ways to check this; it seems like the bench command would work)

It's also entirely possible I'm not understanding what is supposed to be happening, please enlighten me if that's the case!

---

This change is 

[scott-cotton]

Eric, thanks much for your PR. Indeed the hash was colliding. However, the sudoku test isn't really affected, nor is any solving inside this project (or it would have been noticed earlier).

logic.C is used for creating formulas before sending them to the solver. Since the solving time dominates on interesting problems, this went unnoticed.

But, a small variation on your change:

--- a/logic/c.go
+++ b/logic/c.go
@@ -376,5 +376,5 @@ func (p *C) grow() {
 }

 func strashCode(a, b z.Lit) uint32 {
-       return uint32((a << 13) * b)
+       return uint32(^(a << 13) * b)
 }

gives a huge speedup on constructing logic formulas.

I added this bench:

+type cAdder struct {
+       c   *logic.C
+       f   z.Lit
+       buf []z.Lit
+}
+
+func (a *cAdder) Add(m z.Lit) {
+       if m != z.LitNull {
+               a.buf = append(a.buf, m)
+               return
+       }
+       clause := a.c.F
+       for _, m := range a.buf {
+               clause = a.c.Or(clause, m)
+       }
+       a.buf = a.buf[:0]
+       a.f = a.c.And(a.f, clause)
+}
+
+func BenchmarkStrash(b *testing.B) {
+
+       for i := 0; i < b.N; i++ {
+               circuit := logic.NewC()
+               ca := &cAdder{
+                       c: circuit,
+                       f: circuit.T}
+               gen.Rand3Cnf(ca, 100, 300)
+       }
+}

to test for it and got this:

scott@pavillion gini % go test -bench=. ./logic # with change
BenchmarkStrash-8   	   42534	     27721 ns/op
PASS
ok  	github.com/go-air/gini/logic	2.130s

scott@pavillion gini % go test -bench=. ./logic # without change

BenchmarkStrash-8   	    1322	    899904 ns/op
PASS
ok  	github.com/go-air/gini/logic	1.762s

Would you like to submit something along these lines?

[scott-cotton]

(I think this will help https://github.com/go-air/reach a lot)

[scott-cotton]

Upon reflection, the lits are 32bit so overflow happens a lot on bigger problems, and where there is overflow the hash is distributed. But a huge improvement for the smaller problems.

Reviewable status: 0 of 2 files reviewed, all discussions resolved

[scott-cotton]

Reviewable status: 0 of 2 files reviewed, 2 unresolved discussions (waiting on @ecordell)

---

sudoku_test.go, line 13 at r1 (raw file):

Quoted 5 lines of code…

	for i := 0; i < b.N; i++ {
		Example_sudoku()
	}
}

Please see alternate test in the discussion

---

logic/c.go, line 379 at r1 (raw file):

func strashCode(a, b z.Lit) uint32 {
	return uint32((a << 13) * b)

I think
return uint32(^(a<<13) * b)
is preferable because the change is in one place, preserving the idea of the strashCode, and it uses all the capacity.

[scott-cotton]

well not quite "overflow", but more evenly distributed for larger problems.

Reviewable status: 0 of 2 files reviewed, 2 unresolved discussions (waiting on @ecordell)

[scott-cotton]

Evan, Thanks a lot for the PR.

In the interest of time, I went ahead and submitted the alternative in the review and cut a new release. (contributor agreement and not sure of your level of interest).

Please feel free to follow up in any way.

[ecordell]

Thanks @scott-cotton! Your reasoning makes sense