Reconstruct Ganak Failed

[Annlean]

Hello! I reconstructed Ganak failed. During the reconstruction process, there is no error in the command before running "cp ganak ../bin/" according to the Readme. But running "cp ganak ../bin/" found the following problems: (1) running "cp ganak ../bin/" appeared "cp: cannot create regular file '../bin/': Not a directory"; (2 ) running"./run_ganak.sh " fails with "bash: syntax error near unexpected token `newline'". Please help to check whether the source code of the master is synchronized with the Readme that the reason I guessed the failed. Or is there a more detailed installation commands that I haven't noticed？

[msoos]

Hi,

Thank you for spotting the issues in the README! Sorry, they were outdated instructions. They are now fixed. Please follow how to compile under Linux and then you can run ./ganak myfile.cnf. Let me know how it goes,

Mate

[Annlean]

Hi Mate!

Thanks for your update！the Reconstruction is successed now.

But the result of myfile.cnf is not 128, it outputs:

Then, I tested another simple CNF: p cnf 3 4 1 -2 0 1 3 0 -1 2 3 0 2 -3 0 Ganak is an exact counter, so the exact solutions should be 4 while it outputs 2. I don't know what is wrong in this case. Hope you can explain it.

Anneke

[VincentDerk]

The exact model count of

p cnf 3 4
1 -2 0
1 3 0
-1 2 3 0
2 -3 0

is indeed 2 though, not 4: {1,2,3}, {1,2,-3}*. That is also the model count produced by both the D4 and dSharp model counters.

Assignment {1,-2} yields the remaining formula 3 ^ -3 (unsatisfiable). Assignment {-1} implies -2 and 3 (binary propagation on clause 1 and 2). This does not satisfy the last clause.

[msoos]

Hi,

When I run GANAK's master branch:

$ cat a.cnf 
p cnf 3 4
1 -2 0
1 3 0
-1 2 3 0
2 -3 0

$ ./ganak a.cnf
c Setting the timout to: 100000
c Outputting solution to console
c GANAK version 1.0.0
c ganak GIT revision: aa5c51671dda768c971ba41e8dbcc89ab48bfd21
c ganak build env: CMAKE_CXX_COMPILER = /usr/lib/ccache/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 = May 25 2023 16:18:04
c Setting the timout to: 100000
c Solving a.cnf
c variables (all/used/free):    3/3/0
c clauses (all/long/binary/unit): 4/1/3/0
c Sampling set is present, performing projected model counting 
c Sampling set size: 3
c Sampling set:  0 1 2
c 
c Preprocessing ..
c DONE
c variables (all/used/free):    1/0/1
c clauses (all/long/binary/unit): 1/0/1/0
c Maximum cache size:   6945 MB
c 
c 
c 
c variables (total / active / free)     1/0/1
c clauses (removed)                     4 (3)
c decisions                             0
c Max. decision level                   0
c conflicts                             0
c conflict clauses (all/bin/unit)       0/0/0
c 
c failed literals found by implicit BCP          0
c implicit BCP miss rate         0%
c bytes cache size      20234504
c bytes cache (overall)         20234504
c bytes cache components (overall)      96
c bytes cache (infra / comps) 20234408/96
c bytes pure comp data (curr)    4
c bytes pure comp data (overall) 4
c bytes cache with sysoverh (curr)    160
c bytes cache with sysoverh (overall) 160
c cache (lookup / stores / hits)                        0/1/0
c cache miss rate 0%
c avg. variable count (stores / hits)   0/0
c 
c 
s SATISFIABLE 
c # solutions 
s mc 2
c # END
c 
c time: 0.001221s

Are you sure you are getting 4? What version are you running with? Can you please try the following:

• delete all ganak related binaries, libraries, etc. from /usr/lib and /usr/local/lib, and include and bin.
• delete the build directory build
• re-build the binary given the instructions in the README (this has been recently updated :) )
• issue ldd ganak
• run ./ganak a.cnf
• run cat a.cnf

Please give the output for everything including cmake output, make output, ganak output, cat output, and also please include the output of git rev-parse HEAD.

Thanks,

Mate

[Annlean]

Hi,

The solutions of a.cnf is 2, you are right!

So how about the result of running myfile.cnf ? Are the reproduced Ganak results correct?

[msoos]

Hi,

You never attached myfile.cnf. Can you please attach it? Thanks,

mate

[Annlean]

$ cat myfile.cnf c ind 1 3 4 6 7 8 10 0 p cnf 500 1 3 4 0 It's in your README content.

[msoos]

Wow, that was a good catch! Sorry for that. I had to both fix the code and up date the README. It has now been fixed.

The CNF needs to look like:

p cnf 500 1
c ind 1 3 4 6 7 8 10 0
3 4 0

So the independent support needs to go after p cnf...

Also, the parsing was incorrect. This has now been fixed.

[Annlean]

thanks, Ganak is normal now.