deprecate sumBit, since sumBits is better

[jwaldmann]

The sumBits function computes the sum of a list of binary numbers. If all numbers have just one bit, then this computes the number of bits that are set to true. Then, there is sumBit which claims to be an improved implementation for this special case.

(relevant source code: https://hackage.haskell.org/package/ersatz-0.3.1/docs/src/Ersatz.Bits.html#sumBits )

I observed that

• sumBit does produce somewhat smaller formulas than sumBits
• but they are much harder to solve (for minisat)

and I conclude that

• sumBit should not be used.

Here is a test case: https://github.com/jwaldmann/ersatz/blob/sumbits-example/examples/DominatingSet.hs where we are looking for a small dominating set on the knight's graph on a chess board.

sumBit  10 16  (SAT)  90 sec        sumBits 10 16  (SAT)   3 sec
sumBit  10 15 (UNSAT)  9 min        sumBits 10 15 (UNSAT) 17 sec

unrelated to this test case, here are the DAGs for the formulas built (with w=4) for

do xs <- replicateM (2^w) exists ; return $ encode (2^(w-1)) === sumBit (xs::[Bit])

with sumBits:

with sumBit:

[jwaldmann]

some more ideas:

• this claim ("... is better") should be re-checked for current solvers, in particular, kissat
• sumBit constructs a minimal-depth circuit (a Wallace tree?) by walking the sub-additions in level order (breadth-first) but we could as well use depth-first. Same formula size, perhaps different propagation behaviour.