search

meelgroup / weighted-to-unweighted

Weighted to unweighted formula converter
https://www.msoos.org/2019/12/weighted-to-unweighted-counting-and-sampling/
3 stars 0 forks source link

Model count after conversion does not gives the correct weighted count #2

Closed AlexandreDubray closed 5 months ago

AlexandreDubray commented 5 months ago

Hey! I'm looking at using this script for some benchmarks. Unfortunately, it seems that for some Bayesian networks, the conversion does not give me the correct results. For instance, this is an instance with a probability of 0.0438. GPMC returns the correct result on the WMC instance.

After converting using the script, with the default parameters, the new formula should be divided by 2**1953. GPMC gives, after normalization, a model count of ~21, and Ganak even has a segmentation fault. I guess something might go wrong during the conversion (the fact that Ganak segfault is very strange). Also, increasing the precision does not change the result.

EDIT: All solvers are run with default parameters (gpmc -mode=0 unweighted.cnf and ganak unweighted.cnf)

msoos commented 5 months ago

Hi,

Nice, thank you for the issue! I think the problem was related to instance parsing and to our tool skipping counting when the weight is set to 1. I have fixed this in the following ways.

Firstly, I transformed your instance to the new CNF input format as per: https://mccompetition.org/assets/files/2021/competition2021.pdf You can find this transformed file here: insurance_1.cnf.gz

Then, I have updated the code to match this format and fixed the bug that got triggered on your instance related to weights of 1.0. This now gives:

 ./weighted_to_unweighted.py insurance_1.cnf out
Header says vars: 501  maximum var used: 501
Orig vars: 501     Added vars: 1938
The resulting count you have to divide by: 2**1953
Time to transform: 0.014 s

And the new GANAK will print:

$ ../ganak/build/ganak out 
c o Arjun T: 0.97
c o irred cls (all/long/bin/unit): 1796/976
c o Max cache size (80% free mem-200MB): 37475 MB
c o ind size: 2305 nvars: 2316
c o opt ind size: 2316 ind size: 2305 nvars: 2316
s SATISFIABLE
c o Total time [Arjun+GANAK]: 23.46
c s type pmc
c s log10-estimate 586.560130
c s exact arb int 36318652154033136406183369603628212531228308898650813351844021697530212924377476311941613001752737088313678320015694450218082797481562533467074300478641413406658053954636269536265436269209580164080014411422053318947589202076719921823266551566858983986343179097924862006377745571528506159647946544090780667736145964137328387573310912960663746598622201491541102341954756499925486096329594645020963904638153634087822349917849280919623062966140759446533874524332754805559603558524295967403092811050966065849560649791310397472429613973334703548539034128069149591694075788547513839618929721344

Which translates to:

python
Python 3.11.8 (main, Feb 12 2024, 14:50:05) [GCC 13.2.1 20230801] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import decimal
>>> decimal.Decimal(36318652154033136406183369603628212531228308898650813351844021697530212924377476311941613001752737088313678320015694450218082797481562533467074300478641413406658053954636269536265436269209580164080014411422053318947589202076719921823266551566858983986343179097924862006377745571528506159647946544090780667736145964137328387573310912960663746598622201491541102341954756499925486096329594645020963904638153634087822349917849280919623062966140759446533874524332754805559603558524295967403092811050966065849560649791310397472429613973334703548539034128069149591694075788547513839618929721344)/(decimal.Decimal(2)**decimal.Decimal(1953))

Decimal('0.04451928605034364278244160201')

Note that using the new weighted format has the advantage that sharpsat-td also works on it:

./sharpSAT -WE -decot 25 -decow 100 -tmpdir . -cs 3500 --prec 20 insurance_1.cnf
c o Solved. 25.098
s SATISFIABLE
c s type wmc
c s log10-estimate -1.359
c s exact arb float 0.044

In case you are interested in the new GANAK, please do let me know, I'd be happy to give it to you. It's a lot faster than old GANAK.

I am now closing this issue, as the underlying issue as been fixed. In case you have any further questions, or if you have any bug you find, please do let us know. We'd be happy to help/collaborate on cool projects. Also! PLEASE don't forget to send your instances to the model counting competition! They need new instances every year, and you can send your to them until the 30th of March, so only 4-5 days left!

Please consider sending your instances. It would really help the community: https://mccompetition.org/2024/mc_description

Thanks again for all,

Mate