cnf simplification problem with double equations about bosphorus

[msoos]

Hi,

Sorry, I don't understand. What kind of improvement are we missing? You are trying to simplify:

x1 ⊕ x2 ⊕ x5 = 0
x1 * x2 ⊕ x3 ⊕ x4 ⊕ x6 = 0

As far as I can see, these don't have any common larger-than-1 monomials, and none of them are 2-long or 1-long. They don't share significant parts of their (any-sized) monomials, either. What simplification are we missing here?

You mention: When I use other [CNF] equation simplification tools -- which ones, and what do these do? And what do you give them as input? Given the CNF, it seems like they managed to remove exactly one clause (15 vs 16)? And they removed zero variables (7 vs 7). In fact, the only difference is:

@@ -2,7 +2,6 @@
 -2 -3 -4 5 -7 0
 -2 -3 4 -5 -7 0
 -2 -3 4 5 7 0
--2 -3 -6 0
 -2 3 6 0
 2 -3 6 0
 2 3 -6 0
@@ -10,7 +9,7 @@
 2 -4 5 7 0
 2 4 -5 7 0
 2 4 5 -7 0
-3 -4 -5 -7 0
-3 -4 5 7 0
-3 4 -5 7 0
-3 4 5 -7 0
+-4 -5 -6 -7 0
+-4 5 -6 7 0
+4 -5 -6 7 0
+4 5 -6 -7 0

Which seems minor, and perhaps also incorrect -- are you 100% sure the clause it removed, -2 -3 -6 0 can be removed without affecting the number of solutions? We output a CNF that is guaranteed to have as many solutions over the inputs as the original ANF. Maybe removing that clause is possible to preserve equisatisfiability, but are you sure it can be removed and preserve the number of solutions?

All in all, your bug report is either misunderstood by me or incomplete. Can you please be more precise, and in particular, can you please let me know why diff above is correct?

[vilvuss]

The other simplification tool in question is the use of the wolframalpha site which offers a logical equation conversion and minimisation program, here is how I went about obtaining the simplified CNF formula for the double equation:

first of all I had to adapt the double equation to the format supported by wolframalpha, reduce the double equation to a single equation:

- initial equations:

x1 ⊕ x2 ⊕ x5 <=> 0
x1 * x2 ⊕ x3 ⊕ x4 ⊕ x6 <=> 0

- ANF format :

x1 + x2 + x5 <=> 0
x1 * x2 + x3 + x4 + x6 <=> 0

- add parentheses respecting the operator priority rules:

(x1 + x2 + x5) <=> 0
((x1 * x2) + x3 + x4 + x6) <=> 0

- replacement of the variables x(n) by the variables (a, b, c, d, e, f) :

(a + b + e) <=> 0
((a * b) + c + d + f) <=> 0

- link equations by an AND operator to form a single equation:

(((a + b + e) <=> 0) * (((a * b) + c + d + f) <=> 0)) <=> 1 

- equivalence at 0 :

((((a + b + e) <=> 0) * (((a * b) + c + d + f) <=> 0)) + 1) <=> 0

- change the syntax of the operators:

((((a xor b xor e) <=> 0) and (((a and b) xor c xor d xor f) <=> 0)) xor 1) <=> 0

- result of the CNF conversion and simplification on the Wolframalpha site:

https://www.wolframalpha.com/input?i2d=true&i=CNF+%5C%2840%29%5C%2840%29%5C%2840%29%5C%2840%29a+xor+b+xor+e%5C%2841%29+%3C%3D%3E+0%5C%2841%29+and+%5C%2840%29%5C%2840%29%5C%2840%29a+and+b%5C%2841%29+xor+c+xor+d+xor+f%5C%2841%29+%3C%3D%3E+0%5C%2841%29%5C%2841%29+xor+1%5C%2841%29+%3C%3D%3E+0

(¬ a ∨ ¬ b ∨ ¬ c ∨ ¬ d ∨ f) ∧ 
(¬ a ∨ ¬ b ∨ ¬ c ∨ d ∨ ¬ f) ∧ 
(¬ a ∨ ¬ b ∨ c ∨ ¬ d ∨ ¬ f) ∧ 
(¬ a ∨ ¬ b ∨ c ∨ d ∨ f) ∧ 
(¬ a ∨ b ∨ e) ∧ 
(a ∨ ¬ b ∨ e) ∧ 
(a ∨ b ∨ ¬ e) ∧ 
(a ∨ ¬ c ∨ ¬ d ∨ ¬ f) ∧ 
(a ∨ ¬ c ∨ d ∨ f) ∧ 
(a ∨ c ∨ ¬ d ∨ f) ∧ 
(a ∨ c ∨ d ∨ ¬ f) ∧ 
(¬ c ∨ ¬ d ∨ ¬ e ∨ ¬ f) ∧ 
(¬ c ∨ d ∨ ¬ e ∨ f) ∧ 
(c ∨ ¬ d ∨ ¬ e ∨ f) ∧ 
(c ∨ d ∨ ¬ e ∨ ¬ f)

DIMACS cnf format of the solution :

p cnf 7 15
-2 -3 -4 -5 7 0
-2 -3 -4 5 -7 0
-2 -3 4 -5 -7 0
-2 -3 4 5 7 0
-2 3 6 0
2 -3 6 0
2 3 -6 0
2 -4 -5 -7 0
2 -4 5 7 0
2 4 -5 7 0
2 4 5 -7 0
-4 -5 -6 -7 0
-4 5 -6 7 0
4 -5 -6 7 0
4 5 -6 -7 0

I am not sure that the simplification of wolframalpha preserves all solutions which explains the CNF output formula proposed by the site.

I am still learning the domain, I am sorry I did not assimilate this feature which preserves the number of solutions, I understand now why the CNF formulas of Bosphorus are different.

However, why would you want to preserve all possible combinations of solutions if only one combination of solutions is sufficient to satisfy the CNF equation?

Is there a configuration of the Bosphorus that avoids having a CNF formula that preserves all solutions as on wolframalpha?

thank you for your help and your work

[msoos]

However, why would you want to preserve all possible combinations of solutions if only one combination of solutions is sufficient to satisfy the CNF equation? -- because many use-cases require the user to be able to count the solutions. For example, to calculate propbabilities.

Is there a configuration of the Bosphorus that avoids having a CNF formula that preserves all solutions as on wolframalpha? -- no. However, the difference is minor, and will not affect the performance at all. It is extremely likely that the transformation used by Wolfram Alpha is nowhere near as sophisticated on complicated examples as Bosphorus. I would strongly suggest checking out a much more complicated equation set. The difference will almost surely be in favour of Bosphorus, by a large margin.

I am closing, because I don't see any issue here, we are doing exactly as we should. The difference is minor, and on larger instances we are almost surely way better. However, if you find an large formula where we are measurably worse, please let us know, and we'll look into it. However, a single clause on a tiny example is simply not a good indicator.