meelgroup/bosphorus

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

ErwinHaasnoot opened this issue · 3 comments

ErwinHaasnoot commented

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 commented

FYI: I am running Bosphorus from the docker container built on the latest commit that you so kindly made after my previous bug report: dd9654a

msoos commented

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 commented