search

meelgroup / ganak

The first scalable probabilistic exact counter
MIT License
25 stars 6 forks source link

WMC ganak fails on the given examples #22

Closed AlexandreDubray closed 7 months ago

AlexandreDubray commented 1 year ago

Hello,

After compiling (edit: on linux) ganak on the wmc branch, for weighted model counting, it fails on the file benchmarks/toy.cnf with the following error message

c Outputting solution to console
c GANAK version 1.0.0
c ganak GIT revision: 66d056ed46bede6a9440b0d75887d2717640c147
c ganak build env: CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -mtune=native -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 -ggdb3 | COMPILE_DEFINES =  | STATICCOMPILE = OFF | ONLY_SIMPLE =  | Boost_FOUND =  | ZLIB_FOUND =  | ENABLE_TESTING =  | ENABLE_ASSERTIONS = ON | MY_TARGETS =  | compilation date time = Oct 18 2022 16:17:37
The sum of positive and negative literal is not equal to 1 for variable 4 pos weight 0.5 neg weight 0.5

Which is strange given that 0.5+0.5 = 1

msoos commented 1 year ago

Actually, the WMC branch has a bug, I think. Sorry, it's really not stable. Can you please attach here the example CNF that triggers this bug? However, it's really not stable. I'm sorry, I wish it was, but it isn't. Also, I may not have the time to work on it right now :(

AlexandreDubray commented 1 year ago

The file gnerating the bug is the file benchmarks/toy.cnf on the repo

msoos commented 7 months ago

Hi,

Thanks for this, but currently, WMC is not supported. I cannot fix this now because we'll have a new version of GANAK that has weights, but it's a very different code, with thousands of lines of change. Sorry.