Issue with compiling dimacs file into sdd and vtree

[LedaguenelArthur]

Hi,

I have encountered some issue when trying to compile a test.txt file in dimacs format into a constraint.vtree and a constraint.sdd files using the following command line :

pysdd -c test.txt -W constraint.vtree -R constraint.sdd

I do not get any error but only the following prompt :

reading cnf...
Read CNF: vars=1860 clauses=5455
creating initial vtree balanced 
creating manager...
compiling...

and then nothing else... no trace of the constraint.vtree and constraint.sdd files.

I don't think it is an installation error since I can make this command work fine on an other file dimacs.txt encoding hot one encoding for 3 variables. In this case I get :

reading cnf...
Read CNF: vars=3 clauses=23    
creating initial vtree balanced
creating manager...
compiling...

compilation time         : 0.000 sec
 sdd size                : 6
 sdd node count          : 3
 sdd model count         : 3    0.000 sec
saving compiled sdd ...done
saving vtree ...done
done

Could it be that the number of variables in test.txt is too high to be processed ? Is there any thing else about the test.txt file that could explain this bug ?

Here are both input files : dimacs.txt test.txt

Best regards, Arthur

[art-ai]

I tried compiling the CNF myself using a min-fill vtree, and also by turning off dynamic minimization, and it compiled quickly. It might be that the (dynamic) CNF compiler is slow on this particular CNF.

The vtree is attached below. I used minic2d to get the vtree using min-fill. minic2d can also save the SDD to file. You can also get minic2d here.

[ test.vtree.txt ](url)

[LedaguenelArthur]

Hi @art-ai,

Thanks a lot for the quick answer and the compiled vtree ! I was wondering if it was possible to turn off dynamic minimization in PySDD wrapper directly or if I had to use minic2d for this ?

Best regards, Arthur

[VincentDerk]

Hi @art-ai,

Thanks a lot for the quick answer and the compiled vtree ! I was wondering if it was possible to turn off dynamic minimization in PySDD wrapper directly or if I had to use minic2d for this ?

Best regards, Arthur

This solved issue might help with that: https://github.com/wannesm/PySDD/issues/23#issuecomment-722512504