search

meelgroup / unigen

UniGen approximately uniform sampler
Other
25 stars 4 forks source link

Unigen crashes on a benchmark. #13

Closed yashpote closed 1 year ago

yashpote commented 1 year ago

I ran the following command: ./unigen --seed 1023 -v 0 bug.txt

It gives me the output:

  c [unig] Original sampling vars: 31 0 1 2 3 4 5 6 33 32 20 21 22 23 24 25 26 27 28 29 30
  c [unig] Orig sampling vars size: 21
  c WARNING: Turning off gates, because the sampling size is small, so we can just do it
  c [arjun] final indep set: 34 32 30 28 26 24 23 22 21 7 33 31 29 27 25 5 4 9 0
  c [arjun] final set size:       18 percent of original:  85.71 %
  ERROR: variable 3 is set as sampling but is unset!
  NOTE: var 3 has removed value: not removed and is set to l_Undef
   unigen: /unigen/cms_git/cryptominisat/src/solver.cpp:1437: void
 CMSat::Solver::extend_solution(bool):  Assertion model[var] != l_Undef' failed.
   Aborted (core dumped)`

However, I did not get the error for a different seed: ./unigen --seed 1024 -v 0 bug.txt

I have attached the buggy cnf. bug.txt

I suspect that the bug is in the maintenance of the sampling vars, as this line of the output seems to say that '0' is a sampling var. c [unig] Original sampling vars: 31 0 1 2 3 4 5 6 33 32 20 21 22 23 24 25 26 27 28 29 30

msoos commented 1 year ago

Hi,

Thanks for the bugreport! Unfortunately, I cannot reproduce this bug. I have added some minor changes, to make sure we catch something like this, but I can't seem to reproduce it. Can you please give me the full output of your 

./unigen --version

please? Also, unfortunately the above will not give the Arjun version (which I have now fixed). In general, I think you need to update CryptoMiniSat, Arjun, ApproxMC, and UniGen, i.e. ALL of them, in that order, and then the bug will be gone. Can you please check if the bug goes away if you do that?

Thanks,

Mate

msoos commented 1 year ago

For me, the --version output is:

 ~/de/sat_solvers/unigen/build  master *3 ?10  ./unigen --version                                               ✔ 
c UniGen SHA revision 6dd16d14db4b8c2062dad483ab60a23117c32f13
c UniGen version 2.5.2
c UniGen compilation env CMAKE_CXX_COMPILER = /usr/lib/ccache/bin/c++ | CMAKE_CXX_FLAGS =  -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 -g -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DBOOST_TEST_DYN_LINK | STATICCOMPILE = OFF | Boost_FOUND = TRUE | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | GMP_FOUND = TRUE | ENABLE_ASSERTIONS = ON | MY_TARGETS =  | compilation date time = Mar  3 2023 19:10:30
c UniGen compiled with gcc version 12.2.1 20230201
c ApproxMC SHA revision f04ef377b41afa517eedeaa2abff40c940d4cab8
c ApproxMC version 4.1.9
c ApproxMC compilation env CMAKE_CXX_COMPILER = /usr/lib/ccache/bin/c++ | CMAKE_CXX_FLAGS =  -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 -g -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DBOOST_TEST_DYN_LINK | STATICCOMPILE = OFF | Boost_FOUND = TRUE | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | GMP_FOUND = TRUE | ENABLE_ASSERTIONS = ON | MY_TARGETS =  | compilation date time = Mar  3 2023 19:10:11
c ApproxMC compiled with gcc version 12.2.1 20230201
c CryptoMiniSat version 5.11.7
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision bd2b169e6e5bb05c8370901b8247c756b01c75f7
c CMS is MIT licensed
c Using VMTF code by Armin Biere from CaDiCaL
c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14
c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96,
c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'
c       by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos
c Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]'
c       by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015
c CMS compilation env CMAKE_CXX_COMPILER = /usr/lib/ccache/bin/c++ | CMAKE_CXX_FLAGS =  -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 -g -Wno-class-memaccess -mpopcnt -msse4.2 -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DUSE_TBUDDY -DRDB0_ONLY_FEATURES -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DYALSAT_FPU | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING = ON | M4RI_FOUND =  | NOM4RI = ON | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . | compilation date time = Mar  3 2023 19:10:25
c CMS compiled with gcc version 12.2.1 20230201
c Arjun Version: ef581b7e6e84e2c7b628a3fb24ee9c3854e467de
c CryptoMiniSat version 5.11.7
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision bd2b169e6e5bb05c8370901b8247c756b01c75f7
c CMS is MIT licensed
c Using VMTF code by Armin Biere from CaDiCaL
c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14
c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96,
c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'
c       by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos
c Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]'
c       by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015
c CMS compilation env CMAKE_CXX_COMPILER = /usr/lib/ccache/bin/c++ | CMAKE_CXX_FLAGS =  -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 -g -Wno-class-memaccess -mpopcnt -msse4.2 -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DUSE_TBUDDY -DRDB0_ONLY_FEATURES -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DYALSAT_FPU | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING = ON | M4RI_FOUND =  | NOM4RI = ON | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . | compilation date time = Mar  3 2023 19:10:25
c CMS compiled with gcc version 12.2.1 20230201

By the way, next time you need to paste such text in, you can use the triple-backtick at the beginning of the text, and then the triple-backtick at the end of your text. I fixed your bugreport to use this. It looks better and is a lot less work in general. Please check how I fixed it and next time you can use the triple-backtick so it's easier for both you and me. Thanks!

Mate

yashpote commented 1 year ago

I am still getting the same bug after updating.

This is output of --version for me:

c UniGen SHA revision 6dd16d14db4b8c2062dad483ab60a23117c32f13
c UniGen version 2.5.2
c UniGen compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -fvisibility=hidden -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -g -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DBOOST_TEST_DYN_LINK | STATICCOMPILE = OFF | Boost_FOUND = TRUE | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | GMP_FOUND = TRUE | ENABLE_ASSERTIONS = ON | MY_TARGETS =  | compilation date time = Mar  4 2023 19:43:56
c UniGen compiled with gcc version 11.3.0
c ApproxMC SHA revision e93d483d98fdd4e796959213439c5da3d5bb53db
c ApproxMC version 4.1.9
c ApproxMC compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -fvisibility=hidden -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -g -fvisibility=hidden -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DBOOST_TEST_DYN_LINK | STATICCOMPILE = OFF | Boost_FOUND = TRUE | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | GMP_FOUND = TRUE | ENABLE_ASSERTIONS = ON | MY_TARGETS =  | compilation date time = Mar  4 2023 19:43:28
c ApproxMC compiled with gcc version 11.3.0
c CryptoMiniSat version 5.11.7
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision be44a04788205e26c784de40c9f6b4bd3d2583f5
c CMS is MIT licensed
c Using VMTF code by Armin Biere from CaDiCaL
c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14
c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96,
c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'
c       by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos
c Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]'
c       by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015
c CMS compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -fvisibility=hidden -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 -g -Wno-class-memaccess -mpopcnt -msse4.2 -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DRDB0_ONLY_FEATURES -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DYALSAT_FPU | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING = OFF | M4RI_FOUND =  | NOM4RI = ON | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . | compilation date time = Mar  4 2023 19:41:26
c CMS compiled with gcc version 11.3.0
c Arjun Version: ee38c30704c97dba170785dffdefaa0109c8d414
c CryptoMiniSat version 5.11.7
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision be44a04788205e26c784de40c9f6b4bd3d2583f5
c CMS is MIT licensed
c Using VMTF code by Armin Biere from CaDiCaL
c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14
c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96,
c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'
c       by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos
c Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]'
c       by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015
c CMS compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -fvisibility=hidden -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 -g -Wno-class-memaccess -mpopcnt -msse4.2 -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES =  -DRDB0_ONLY_FEATURES -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DYALSAT_FPU | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING = OFF | M4RI_FOUND =  | NOM4RI = ON | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . | compilation date time = Mar  4 2023 19:41:26
c CMS compiled with gcc version 11.3.0

I updated CryptoMiniSat, Arjun, ApproxMC, and UniGen in that order. The SHA revision values for CMS, Arjun, ApproxMC, and Unigen are of the latest commits as of now.

msoos commented 1 year ago

Ah, I see, I can now reproduce it. Sorry, let me look at this.

msoos commented 1 year ago

I have managed to find the issue. Can you please test and if it's good, close this issue? Thanks! You will need to update CMS, Arjun, ApproxMC, and UniGen. Sorry, it wasn't my idea to cut it into so many projects :S

Let me know if this fixed it,

Mate

yashpote commented 1 year ago

Works perfectly! Thank you.