msoos
commented
3 years ago Nice catch and a great report! Thanks :) I'll look at this in the evening and fix it ASAP! Also, I'll likely need to write a fuzzer so we can find these issues :) Thanks again, I'll fix by tonight most likely!
Mate
On Tue, Mar 30, 2021, 04:01 T. Miller @.***> wrote:
E.g., from your co-authored paper "Principled Network Reliability Approximation: A Counting-Based Approach" I encoded Fig 1. like so:
c ind 1 2 3 4 5 0 p cnf 11 14 2 -3 -9 0 -7 4 -1 0 4 -3 -10 0 2 -6 -1 0 3 -4 -10 0 -3 -1 0 -8 1 -5 0 1 -6 -2 0 -8 5 -1 0 1 -4 -7 0 -5 4 -11 0 3 -2 -9 0 1 3 0 -11 -4 5 0
Running ApproxMC4 dumps core on a failed assertion:
c ApproxMC SHA revision df6d9fc8d112d758301d7527817e2eb1029fa5eb c ApproxMC version 4.0.1 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 -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 = | STATICCOMPILE = ON | Boost_FOUND = TRUE | ZLIB_FOUND = TRUE | VALGRIND_FOUND = | GMP_FOUND = TRUE | ENABLE_ASSERTIONS = ON | MY_TARGETS = | compilation date time = Oct 2 2020 22:34:49 c ApproxMC compiled with gcc version 10.2.0 c CryptoMiniSat version 5.8.0 c CMS Copyright Mate Soos @.***) c CMS SHA revision 6477e8bc43b0fda7038965bb148b64b8637c804b c CMS is GPL licensed due to M4RI being linked. Build without M4RI to get MIT version 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 = -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 = -DEXTENDED_FEATURES -DUSE_GAUSS -DUSE_ZLIB -DYALSAT_FPU -DUSE_M4RI | STATICCOMPILE = ON | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND = FALSE | ZLIB_FOUND = TRUE | VALGRIND_FOUND = | ENABLE_TESTING = OFF | M4RI_FOUND = TRUE | NOM4RI = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE = /usr/bin/python2.7 | PYTHON_LIBRARY = PYTHON_LIBRARY-NOTFOUND | PYTHON_INCLUDE_DIRS = | MY_TARGETS = | LARGEMEM = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES = | BREAKID-VER = . | BOSPHORUS_LIBRARIES = | BOSPH-VER = . | compilation date time = Oct 2 2020 22:34:07 c CMS compiled with gcc version 10.2.0 c executed with command line: /home/cerebus2/projects/pynet-a/scratch/approxmc-linux-x64 formula.cnf c -- header says num vars: 11 c -- header says num clauses: 14 c -- clauses added: 14 c -- xor clauses added: 0 c -- vars added 11 c [appmc] Sampling set size: 5 c [appmc] Sampling set: 1, 2, 3, 4, 5, c [sparse] Using match: 0 sampling set size: 5 prev end inclusive is: -1 this end inclusive is: 50 next end inclusive is: 100 sampl size: 5 c [appmc] threshold set to 72 sparse: 0 c [appmc] Starting up, initial measurement c [appmc] Starting at hash count: 1 c [appmc] [ 0.00 ] round: 0 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 0 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c [appmc] simplifying c [appmc] [ 0.00 ] round: 1 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 1 hashes: 0 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0 c [appmc] simplifying c [appmc] [ 0.00 ] round: 2 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 2 hashes: 0 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0 c [appmc] simplifying c [appmc] [ 0.00 ] round: 3 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 3 hashes: 0 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0 c [appmc] simplifying c [appmc] [ 0.00 ] round: 4 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 4 hashes: 0 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0 c [appmc] simplifying c [appmc] [ 0.00 ] round: 5 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 5 hashes: 0 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0 c [appmc] simplifying c [appmc] [ 0.00 ] round: 6 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 6 hashes: 0 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0 c [appmc] simplifying c [appmc] [ 0.00 ] round: 7 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 7 hashes: 0 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0 c [appmc] simplifying c [appmc] [ 0.00 ] round: 8 hashes: 1 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 1 c WHAAAAT Detach issue. All below must be 1 to work --- c -- can_detach: 0 c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0 c -- !conf.gaussconf.autodisable: 1 c -- conf.xor_detach_reattach: 1 c [appmc] [ 0.00 ] round: 8 hashes: 0 c [appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0 approxmc-linux-x64: /home/soos/development/sat_solvers/approxmc/src/counter.cpp:447: ApproxMC::SolCount Counter::count(): Assertion `numHashList.size() > 0 && "UNSAT should not be possible"' failed. aborted (core dumped)
I'm not sure if this affect results on larger graphs. I've run counts on more substantial CNFs and get results, but nothing I've been able to verify by other methods.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/meelgroup/approxmc/issues/21, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKF4OOSIJOURLE2KTGAEV3TGEWGHANCNFSM42BA4EIQ .
E.g., from your co-authored paper "Principled Network Reliability Approximation: A Counting-Based Approach" I encoded Fig 1. like so:
Running ApproxMC4 dumps core on a failed assertion:
I'm not sure if this affect results on larger graphs. I've run counts on more substantial CNFs and get results, but nothing I've been able to verify by other methods.