Assertion Failure in findWatchedOfBin (src/watchalogs.h:160)

[HariNarayana123]

I encountered an assertion failure in findWatchedOfBin while solving a CNF problem with 476,982 variables and 2,971,156 clauses (p cnf 476982 2971156). I was running CryptoMiniSat using 4 threads, and after approximately 24 hours, the solver terminated due to the failure of this assertion.

cryptominisat-5.11.21/src/watchalgos.h:160: CMSat::Watched& CMSat::findWatchedOfBin(CMSat::watch_array&, CMSat::Lit, CMSat::Lit, bool, int32_t): Assertion 'false' failed.

This issue seems similar to [(https://github.com//issues/759)].

version of cryptominisat

c CryptoMiniSat version 5.11.23
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision 7b2b6fac74be4c337c6582e6c53fe16e91646098
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 CMS is MIT licensed
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 =  -DLARGE_OFFSETS -DRDB0_ONLY_FEATURES -DYALSAT_FPU | STATICCOMPILE = OFF | ONLY_SIMPLE =  | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = FALSE | VALGRIND_FOUND =  | ENABLE_TESTING = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM = ON | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . |
c CMS compiled with gcc version 11.4.0
c CryptoMiniSat version 5.11.23
c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
c CMS SHA revision 7b2b6fac74be4c337c6582e6c53fe16e91646098
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 CMS is MIT licensed
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 =  -DLARGE_OFFSETS -DRDB0_ONLY_FEATURES -DYALSAT_FPU | STATICCOMPILE = OFF | ONLY_SIMPLE =  | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND = FALSE | VALGRIND_FOUND =  | ENABLE_TESTING = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE =  | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  | MY_TARGETS =  | LARGEMEM = ON | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . |
c CMS compiled with gcc version 11.4.0

how can i resolve this error?

[msoos]

Hi,

Thank you for the bug report. Can you please try using one of the binaries at the bottom of this GitHub Action under "Artifacts":

https://github.com/msoos/cryptominisat/actions/runs/13882992042

Alternatively, you can also switch to the synthesis branch and use cryptominisat via nix, typing nix shell -- it will then build cryptominisat5 and you can use it by simply typing cryptominisat5. If you use nix this should be easier. Otherwise, the static binaries as per above link should work flawlessly and waaay easier than to install nix, etc. Can you please try the static binaries?

Thanks,

Mate

[msoos]

I am closing as there have been no feedback for 3 months.