fusing `And` nodes prevents propagation in the solver?

[jwaldmann]

The example is from #87. I am not quite sure whether to following analysis is correct.

Ersatz will fuse And [And [x,y], z] into And [x,y,z]. This reduces the number of Tseitin variables (and of clauses). But - if a fused sub-expression was shared, then this information is lost - while it might have been helpful for inference (in the solver).

Example: Bits xs + Bits ys <? 2: we get the following graph (with black and red edges)

if the root is asserted, then I think we can't propagate much. But - after we apply the following equivalence transformation: remove red edges, add blue edge, we can:

• Tseitin transform makes clauses -P => R, -Q => R, R => (-P | -Q),
• we assert R, obtain (-P | -Q)
• xor(P,Q) must be false, so P = Q (if the solver recognizes equivalences from binary clauses)
• then (-P|-Q) simplifies to -P, is unit (P must be false)
• since xor(3,5) = P = false, infer 3 = 5
• since true = nand(3,5), simplify to not (3), is unit, so 3 = false

Comment: perhaps And [And [x,y], z] is fine. It's a larger CNF, but everything that can be inferred, can be inferred by unit propagation, and the SAT solver is good at this.

I will patch a version of Ersatz without And fusion, and compare.