search

meelgroup / bosphorus

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter
Other
65 stars 18 forks source link

Unexpected behavior on a factored system #23

Closed espitau closed 3 years ago

espitau commented 3 years ago

I tried to solve the following system which is not in ANF (ternary factorized system):

(x1*x4 + x0*x5)*x8 + (x3*x4 + x0*x7)*x9 + (x3*x6 + x2*x7)*x10 + (x2*x5 + x1*x6)*x11
(x2*x4 + x0*x6)*x8 + (x3*x5 + x1*x7)*x9 + (x2*x4 + x0*x6)*x10 + (x3*x5 + x1*x7)*x11
(x2*x5 + x1*x6)*x8 + (x1*x4 + x0*x5)*x9 + (x3*x4 + x0*x7)*x10 + (x3*x6 + x2*x7)*x11
(x3*x4 + x0*x7)*x8 + (x3*x6 + x2*x7)*x9 + (x2*x5 + x1*x6)*x10 + (x1*x4 + x0*x5)*x11
(x3*x5 + x1*x7)*x8 + (x2*x4 + x0*x6)*x9 + (x3*x5 + x1*x7)*x10 + (x2*x4 + x0*x6)*x11
(x3*x6 + x2*x7)*x8 + (x2*x5 + x1*x6)*x9 + (x1*x4 + x0*x5)*x10 + (x3*x4 + x0*x7)*x11 + 1

However, a bosphorus call on this system still produce a solution (which is not a solution of the problem however). After inspecting the output with option --anfwrite, it seems that some parsing is still going on and that a system is somehow produced, which is pretty odd.

Is it a feature, or should the parser raise an error because the system is not in ANF ?

msoos commented 3 years ago

Hi,

Thanks for the report! Parser should raise an error. It misparses the system. This is a bug, I'm flagging it as such. If you wanna have a go at it, the parsing function is here: https://github.com/meelgroup/bosphorus/blob/master/src/anf.cpp#L100 Otherwise, we'll try to fix :)

Thanks again,

Mate

msoos commented 3 years ago

Ah, I figured out what's going on. It ignores all brackets because people sometimes write x(1) and sometimes they write x1. I am now creating a test case to check for this!

msoos commented 3 years ago

Yay, fixed it! Also, thanked you in the commit :) Thanks again for reporting, and sorry for the delay. I also added a bunch of tests so we should be able to catch these next time without much further ado :)