Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Unigen crashes on a benchmark. #13

Closed
yashpote opened this issue Mar 3, 2023 · 6 comments
Closed

Unigen crashes on a benchmark. #13

yashpote opened this issue Mar 3, 2023 · 6 comments

Comments

@yashpote
Copy link

yashpote commented Mar 3, 2023 •
edited by msoos
Loading

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

@yashpote yashpote changed the title Unigen crashes for a particular seed. Unigen crashes on a benchmark. Mar 3, 2023
@msoos
Copy link
Collaborator

msoos commented Mar 3, 2023

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
Copy link
Collaborator

msoos commented Mar 3, 2023

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
Copy link
Author

yashpote commented Mar 4, 2023 •
edited
Loading

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
Copy link
Collaborator

msoos commented Mar 4, 2023

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

@msoos
Copy link
Collaborator

msoos commented Mar 4, 2023

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
Copy link
Author

yashpote commented Mar 4, 2023

Works perfectly! Thank you.

@yashpote yashpote closed this as completed Mar 4, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@msoos @yashpote