improve documentation of Ersatz.Counting

[jwaldmann]

(I will do this) The functions in this module are trivial

exactly :: Int -> [ Bit ] -> Bit
exactly k bs = encode (fromIntegral k) === sumBit bs
atmost :: Int -> [ Bit ] -> Bit
atmost k bs = encode (fromIntegral k) >=? sumBits bs
atleast :: Int -> [ Bit ] -> Bit
atleast k bs = encode (fromIntegral k) <=? sumBits bs

There is a cottage industry of atmost-k (and similar) encodings, cf. https://www.it.uu.se/research/group/astra/ModRef10/papers/Jingchao%20Chen.%20A%20New%20SAT%20Encoding%20of%20the%20At-Most-One%20Constraint%20-%20ModRef%202010.pdf http://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf

Some of these are not directly applicable: in Ersatz, we want a function (a circuit), while these papers construct a CNF that asserts that the output of this function is true, and they sometimes use extra (guessed) variables. In Ersatz formulas, we have implicit extra variables but they are deterministic.

We could offer special cases for some arguments, as in

exactly_one_naive xs = or xs
  && and ( do x : ys <- tails xs ; y <- ys ; return $ not (x&&y) )

exactly_one_binary = snd . one

-- | (exactly zero, exactly one)
one :: [Bit] -> (Bit,Bit)
one [] = (true,false)
one [x] = (not x,x)
one xs =
  let (ys,zs) = splitAt (div (length xs) 2) xs
      (yzero,yone) = one ys
      (zzero,zone) = one zs
  in  (yzero && zzero, yone && zzero || yzero && zone)

but I found that it's rarely worth it. E.g., this one function is very similar to computing the binary sum of bits, in a representation that has the lowest bit, and overflow.

Anyway the module should

• describe what the functions do, and
• state the method (binary)
• and the resulting complexity (formula size).

[jwaldmann]

See 4b58336d916d160225ff4ad73c31d294926249b8

[jwaldmann]

While atmost 1 is fine now, atmost 2 looks convoluted.

runSAT' (do xs <- replicateM 4 exists ; assert $ atmost 2 xs; return xs )

([Var 2,Var 3,Var 4,Var 5],SAT 13 ((1)
& (-7 | -3 | -2) & (-7 | 2 | 3) & (-2 | 3 | 7) & (-3 | 2 | 7)
& (-8 | -5 | -4) & (-8 | 4 | 5) & (-4 | 5 | 8) & (-5 | 4 | 8) 
& (-8 | -7 | -6) & (-6 | 7 | 8) & (-7 | 6 | 8) & (-8 | 6 | 7) 
& (-3 | -2 | 11) & (-11 | 2) & (-11 | 3) 
& (-5 | -4 | 12) & (-12 | 4) & (-12 | 5) 
& (-12 | -11 | -10) & (-10 | 11 | 12) & (-11 | 10 | 12) & (-12 | 10 | 11) 
& (-8 | -7 | 13) & (-13 | 7) & (-13 | 8) 
& (-13 | -10 | -9) & (-9 | 10 | 13) & (-10 | 9 | 13) & (-13 | 9 | 10) 
& (-9 | -6) 
& (-5 | -4 | -3 | -2) & (-10 | -8 | -7)) mempty)

clearly we can do better: use unary numbers (fixed width, with overflow check) for counting.

NB: this formatting should be automated - perhaps group by highest variable in clause?

[jwaldmann]

with unary numbers - looks much nicer:

runSAT' (do xs <- replicateM 4 exists ; assert $ atmost 2 xs; return xs )

([Var 2,Var 3,Var 4,Var 5],SAT 7 ((1) 
& (-6 | -3) & (-6 | -2) & (-5 | -4 | 6) 
& (-7 | -5) & (-7 | -4) & (-3 | -2 | 7)) 
mempty)

this is in aa2d2221b52e56ccba41ecd9bb197d50755763ad