missing simplification/propagation for assert $ (x + y :: Bits) <=? 1

[jwaldmann]

I am asserting that the sum of two (long) numbers (represented by Ersatz.Bits) is small (zero, one). This uses operator (<=?) with one known argument. Ersatz' simplifier will eliminate all constants (while building the formula) so I hoped that it will detect that most bits must be zero. This does not work. Can we do something about this?

In these examples, xs = Bits[2,3], ys = Bits [4,5]

runSAT' $ do ~[xs,ys] <- replicateM 2 $ replicateM 2 exists; assert $ Bits xs + Bits ys === 0
-- correct answer: 2 = 3 = 4 = 5 = false
((),SAT 11 ((1) & (-6 | -4 | -2) & (-6 | 2 | 4) & (-2 | 4 | 6) & (-4 | 2 | 6) & (-6) & (-8 | -5 | -3) & (-8 | 3 | 5) & (-3 | 5 | 8) & (-5 | 3 | 8) & (-4 | -2 | 9) & (-9 | 2) & (-9 | 4) & (-9 | -8 | -7) & (-7 | 8 | 9) & (-8 | 7 | 9) & (-9 | 7 | 8) & (-7) & (-5 | -3 | 10) & (-10 | 3) & (-10 | 5) & (-10) & (-8 | -4 | -2 | 11) & (-11 | 8) & (-11 | 2) & (-11 | 4) & (-11)) mempty)

runSAT' $ do ~[xs,ys] <- replicateM 2 $ replicateM 2 exists; assert $ Bits xs + Bits ys <=? 0
-- correct answer: 2 = 3 = 4 = 5 = false
((),SAT 11 ((1) & (-6 | -4 | -2) & (-6 | 2 | 4) & (-2 | 4 | 6) & (-4 | 2 | 6) & (-6) & (-8 | -5 | -3) & (-8 | 3 | 5) & (-3 | 5 | 8) & (-5 | 3 | 8) & (-4 | -2 | 9) & (-9 | 2) & (-9 | 4) & (-9 | -8 | -7) & (-7 | 8 | 9) & (-8 | 7 | 9) & (-9 | 7 | 8) & (-7) & (-5 | -3 | 10) & (-10 | 3) & (-10 | 5) & (-10) & (-8 | -4 | -2 | 11) & (-11 | 8) & (-11 | 2) & (-11 | 4) & (-11)) mempty)

runSAT' $ do ~[xs,ys] <- replicateM 2 $ replicateM 2 exists; assert $ Bits xs + Bits ys <=? 1
-- correct answer:  (-2 | -4)  and  3 = 5 = false
((),SAT 12 ((1) & (-7 | -4 | -2) & (-7 | 2 | 4) & (-2 | 4 | 7) & (-4 | 2 | 7) & (-7 | 6 | 7) & (-7 | -6) & (-6 | 7) & (-6) & (-9 | -5 | -3) & (-9 | 3 | 5) & (-3 | 5 | 9) & (-5 | 3 | 9) & (-4 | -2 | 10) & (-10 | 2) & (-10 | 4) & (-10 | -9 | -8) & (-8 | 9 | 10) & (-9 | 8 | 10) & (-10 | 8 | 9) & (-8) & (-5 | -3 | 11) & (-11 | 3) & (-11 | 5) & (-11) & (-9 | -4 | -2 | 12) & (-12 | 9) & (-12 | 2) & (-12 | 4) & (-12)) mempty)

The formula for Bits xs + Bits ys <=? 1 should be nand (2,4) but actually (drawing with #86 ) is this:

Note: this circuit contains the formula we want. How to remove the other nodes?

We can avoid generating nand (x, not x), see in #56 (change in Ersatz.Bits, better orderHelper). There is some extra work in that commit (fixed width numbers with overflow detection) but I hoped to avoid this.

Perhaps we can live with some useless nodes - if the SAT solver is able to do the simplification that Ersatz missed. That's why I printed the CNF as well. I don't think we can unit-propagate much here.

[jwaldmann]

similarly, Bits xs + Bits ys >=? 0 should simplify to true, and Bits xs + Bits ys >? 0 is equivalent to or (xs <> ys), but the actual formulas are huge and don't look propagatable.

[jwaldmann]

detailed analysis for Bits xs + Bits ys === 0:

 (-6 | -4 | -2) & (-6 | 2 | 4) & (-2 | 4 | 6) & (-4 | 2 | 6) & (-6) 
  -- since -6 is unit, simplify to (-2 | 4) & (-4 | 2)`
  -- if the solver could now infer that  2 = 4, then ...
& (-4 | -2 | 9) & (-9 | 2) & (-9 | 4) 
  -- simplifies to (-2 | 9) & (-9 | 2), infer 2 = 9  
& (-9 | -8 | -7) & (-7 | 8 | 9) & (-8 | 7 | 9) & (-9 | 7 | 8) & (-7)
  -- -7 is unit, simplify to (-8 | 9) & (-9 | 8),   infer  8 = 9
& (-8 | -4 | -2 | 11) & (-11 | 8) & (-11 | 2) & (-11 | 4) & (-11)
 -- -11 is unit, simplify to (-8 | -4 | -2), all these are equal, so, must be true, then ...
& (-8 | -5 | -3) & (-8 | 3 | 5) & (-3 | 5 | 8) & (-5 | 3 | 8) 
  -- -8 is unit, simplify to (-3 | 5) & (-5 | 3), infer 3 = 5
& (-5 | -3 | 10) & (-10 | 3) & (-10 | 5) & (-10) 
  -- -10 is unit, implies (-5 | -3), since they are equal, must be true

So: the (only) satisfying assignment can be inferred by detecting equalences, and unit propagation.

[jwaldmann]

analysis for Bits xs + Bits ys <=? 1: it's better to write Bits xs + Bits ys <? 2, then we get

the corresponding CNF

& (-4 | -2 | 8) & (-8 | 2) & (-8 | 4)     -- 8  = and (2,4)
& (-7 | -5 | -3) & (-7 | 3 | 5) & (-3 | 5 | 7) & (-5 | 3 | 7)    -- 7 = xor(3,5)
& (-8 | -7 | -6) & (-6 | 7 | 8) & (-7 | 6 | 8) & (-8 | 6 | 7)   -- 6 = xor (7,8)
& (-6)     -- implies  7 = 8
& (-5 | -3 | 9) & (-9 | 3) & (-9 | 5) --  9 = and (3,5) 
& (-9)   -- implies (-5 | -3)
& (-7 | -4 | -2 | 10) & (-10 | 7) & (-10 | 2) & (-10 | 4)   -- 10 = and(2,4,7)
& (-10)) -- implies (-7 | -4 | -2)