what(): Variable index out of bounds. - with 510 variables and clauses

[ErwinHaasnoot]

Hi!

Thanks again for making this tool avaiable. I've been having a lot of fun playing around with it. It works great normally, but I've hit a (hopefully interesting) snag.

You mention in the README.md that:

Known issues

    PolyBoRi cannot handle ring of sizes over approx 1 million (1048574). Do not run bosphorus on instances with over a million variables.

I seem to have found an instance where I get a PBoriError at 510 variables, with as many clauses. I have been able to successfully run bosphorus on ANF's with many more variables, so this seems like an issue worth reporting. The full output I'm getting is as follows:

c Bosphorus SHA revision dbf61ae96a7a18bdf7547835ddf955d34ec8f211
c Executed with command line: /usr/local/bin/bosphorus --anfread /dat/polybori_error.txt
c Compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES =  | STATICCOMPILE = ON | ONLY_SIMPLE =  | Boost_FOUND = 1 | STATS =  | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING =  | M4RI_FOUND = TRUE | SLOW_DEBUG =  | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM =  | LIMITMEM =  | compilation date time = Apr 25 2020 12:34:11
c --- Configuration --
c maxTime = 1.00e+20
c XL simp (deg = 1; s = 30.00+4.00): 1
c EL simp (s = 30.00): 1
c SAT simp (10000:100000): 1
 using 1 threads
c Cut num: 5
c Brickenstein cutoff: 10
c --------------------
terminate called after throwing an instance of 'polybori::PBoRiError'
  what():  Variable index out of bounds.

Please find the .anf in the attachment (renamed to .txt, because github does not allow uploads otherwise) polybori_error.txt

For context, this is an ANF of the first 32-bit Mersenne Twister state transform on the seed bits (x(0)..x(31), with a myriad of help-variables sprinkled in. I'm not 100% sure yet whether it is an actual representation of the mersenne twister, but in any case it should be a valid ANF

I hope you will be able to look at this! If you need any further information, please do let me know.

Best,

Erwin

[ErwinHaasnoot]

FYI: I am running Bosphorus from the docker container built on the latest commit that you so kindly made after my previous bug report: https://github.com/meelgroup/bosphorus/commit/dd9654af6e380a77e9ff8dfe4ec72b6da90edb40

[msoos]

Ah, you have a bug in your ANF. I will think about how to warn about this. Your line is:

x(372) x(27) + x(373) x(23) + x(374) x(20) + x(28) x(30) + x(15) + x(375) x(28) + x(20) + x(21) + x(23) + x(24) + x(25) + x(28) + x(29) + x(31) + x(376) x(19) + x(377) x(374) + x(378) x(379) + x(375) x(30) + x(380) x(22) + x(376) x(381) + x(379) x(14) + x(382) x(22) + x(377) x(20) + x(372) x(383) + x(384) x(385) + x(382) x(380) + x(386) x(23) + x(373) x(386) + x(378) x(14) + x(24) x(384) + x(27) x(383) + x(381) x(19) + x(24) x(385)x(34) + x(3) + x(1)

Spot the error :D The issue is x(24) * x(385)x(34), you are missing a * between the two x-s. I'll try to catch this kind of thing next time :)

Mate

[ErwinHaasnoot]

Oh! I'm sorry, I should've caught that. I was thrown off by the error. It successfully worked when I limited the output. Programming is tricky sometimes.

On Sun, May 3, 2020, 4:30 PM Mate Soos notifications@github.com wrote:

Closed #17 https://github.com/meelgroup/bosphorus/issues/17.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/meelgroup/bosphorus/issues/17#event-3297475928, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKTFVKYCAKIVT5SYMJJJ53RPV5YFANCNFSM4MX4IXHA .