Confusing message during execution

[abakst]

Hi,

I noticed this output while running approxmc:

c WHAAAAT Detach issue. All below must be 1 to work ---
c -- can_detach: 1
c -- mfinder.no_irred_nonxor_contains_clash_vars(): 0
c -- !conf.gaussconf.autodisable: 1
c -- conf.xor_detach_reattach: 1

I'm not quite sure how to interpret this. I'm mostly concerned with distinguishing between two cases: does this indicate that a cryptominisat error that invalidates the approxmc results? Or is it just an unexpected case that does not affect the correctness results?

Potentially of interest: This particular CNF was generated by simplifying SMTLIB constraints with z3 (including applying some tactics that eliminate unconstrained variables). mis did not produce an MIS for the instance.

The following is printed when execution starts:

c -- header says num vars:         216610
c -- header says num clauses:     1729257
c -- clauses added: 1729257
c -- xor clauses added: 0
c -- vars added 254984

[kuldeepmeel]

The message indicates a performance related issue and does not indicate any issue with correctness.

If you are using Z3 to bit-blast, I would strongly suggest you to use projected counting formulation where the sampling set is the set of variables corresponding to original SMT variables and excludes all the additional variables.

[abakst]

Fantastic! Thanks! I'll look into projected counting.

[msoos]

Please reopen this, Kuldeep -- this needs fixing, it was not meant to show that warning. I'll dig into this later today :)

Thanks,

Mate

On Thu, Jul 16, 2020, 12:48 Kuldeep S. Meel notifications@github.com wrote:

Closed #13 https://github.com/meelgroup/approxmc/issues/13.

— 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/13#event-3552589606, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKF4OOPN7EU4BRZVZ6WYALR33LHFANCNFSM4O3PRD7A .

[msoos]

Hi!

Thanks for reporting. Can you please let me know what was the full command line you gave, and what was the initial few lines ouf output of approxmc, when it started up? Something like:

$ ./approxmc isolateRightmost.sk_7_481.cnf.gz.no_w.cnf.gz
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 -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 = Jul 16 2020 23:06:53
c ApproxMC compiled with gcc version 10.1.0
c CryptoMiniSat version 5.8.0
c CMS Copyright Mate Soos (soos.mate@gmail.com)
c CMS SHA revision 26109ef47541bbd97d7ab183ba8f7fcc6da8b4b4
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 =  -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 -DBOOST_TEST_DYN_LINK -DUSE_SQLITE3 -DUSE_ZLIB -DYALSAT_FPU -DUSE_M4RI -DUSE_MPI | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND = TRUE | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | ENABLE_TESTING = ON | M4RI_FOUND = TRUE | NOM4RI = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE = /usr/bin/python3 | PYTHON_LIBRARY = /usr/lib/libpython3.8.so | PYTHON_INCLUDE_DIRS = /usr/include/python3.8 | MY_TARGETS =  | LARGEMEM = OFF | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . | compilation date time = Jul 16 2020 23:06:29

Thanks again for reporting,

Mate

[abakst]

Here it is,

(I deleted an earlier version because I wasn't sure that if I had executed the correct build)

c ApproxMC SHA revision b1591a30ef87eddf8200def8b02f8bc989049e68
c ApproxMC version 4.0.1
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 -pedantic | COMPILE_DEFINES =  -DBOOST_TEST_DYN_LINK | STATICCOMPILE = OFF | Boost_FOUND = 1 | ZLIB_FOUND = TRUE | VALGRIND_FOUND =  | GMP_FOUND = TRUE | ENABLE_ASSERTIONS = ON | MY_TARGETS =  | compilation date time = Jul 15 2020 11:23:51
c ApproxMC compiled with gcc version 7.5.0
c CryptoMiniSat version 5.8.0
c CMS Copyright Mate Soos (soos.mate@gmail.com)
c CMS SHA revision 4b37dbd7740507685021393d05f3e4c8e3d98164
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/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 -mpopcnt -msse4.2 -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promotion -Wshadow -Wformat=2 -pedantic | COMPILE_DEFINES =  -DLARGE_OFFSETS -DEXTENDED_FEATURES -DUSE_GAUSS -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DYALSAT_FPU -DUSE_M4RI -DUSE_MPI | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = 1 | 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 = /home/abakst/pyenv/bin/python3 | PYTHON_LIBRARY = /usr/lib/x86_64-linux-gnu/libpython3.8.so | PYTHON_INCLUDE_DIRS = /usr/include/python3.8 | MY_TARGETS =  | LARGEMEM = ON | LIMITMEM = OFF | BREAKID_LIBRARIES =  | BREAKID-VER = . | BOSPHORUS_LIBRARIES =  | BOSPH-VER = . | compilation date time = Jul 16 2020 10:48:02

[abakst]

Sorry, missed the command line. It was just approxmc path/to/constraints.dimacs

[msoos]

Ah, good catch, thanks, fixed! :)