vsklad
commented
3 years ago Hi! Thank you very much for pointing this out. I have uploaded the fix. Essentially, assigning many constrains (as in 504out of 512 message bits) leads to many constants in the equation template for addition. This was not well optimised. It should work now. Meanwhile, please note that while CNF has been well tested with a number of types of constrains, ANF has been used much less historically. If you have means to solve ANF equation systems, I would suggest to solve a few to make sure the solutions make sense - as a way to test it.
Should you find any other issues please do let me know.
Hi, I am trying to generate hard instances in ANF format, but it does not work. I took one of the example command lines(see below) and specified ANF output, but it crashes. CNF works fine. Can this be fixed? Thanks
./cgen encode SHA1 -vM random except:8 -vH random -f ANF sha1_random.anf Encoding SHA-1 into ANF Assigned 504 bit(s) in "M" M = {{0xc90c4c, 0b11, , 0b1, 0x9}, 0x6e690698, {0x687, , 0b010, 0x9a8c}, 0x85e fafb7, 0x0e71e1d5, 0x02d9ff1c, 0x71e34faf, {0b00, , 0b0, 0x6140f3b}, 0xb63a2ce8 , 0xc75cbec6, 0xc3b8e820, {0x6, , 0b001, 0x90, , 0b100, 0xf77}, 0x22f762bf, {0 x9061, , 0b01, , 0x039}, 0xb970b31d, {0b100, , 0x238f739}} cgen: ./bal/anf/anf.cpp:200: bal::literalid_t bal::Anf::complete_equation(bal::l iteralid_t, bool): Assertion `(bool)((r) == bal::LITERALID_UNASSIGNED)' failed. Aborted (core dumped)