Runtime:0.621364
('The time taken by D4/Dsharp_PCompile is ', 0.6676230430603027)
('The time taken to parse the nnf text:', 0.04232501983642578)
('The time taken for Model Counting:', 0.16436100006103516)
('Model Count limited to var in dDNNF:', mpfr('1.4659544630212627e-70'))
('The time taken by sampling:', 0.02062702178955078)
('Samples saved to', 'samples.txt')
Hi,
I have attached a file which has a sampling set, for which dsharp-pcompile returns the wrong model count (invoked through WAPS). WAPS output:
WAPS output:
Seperating weights from Input cnf Extracting the Sampling Set cachesize Max: 2048000 kbytes
Vars:1893
Clauses:4776
bin Cls:3184
BEGIN preprocessing found UCCL14
END preprocessing
Vars remaining:1136
Clauses remaining:2846
bin Cls remaining:2064
Uncompressed Edges: 58514 Compressed Edges: 57947
Variables: 1893
Clauses: 4833
Clauses removed: 1987
added Clauses: 205
of all assignments: 7.0759e+569 = 2^(1893)
Pr[satisfaction]: 1.45611e-560
of solutions: 1.03033e+10
SAT (full): 10303307776
Num. conflicts: 20 Num. implications: 285505 Num. decisions: 2447 max decision level: 16 avg decision level: 11.0316 avg conflict level: 0.896714 avg solution level: 11.0404 CCLLen 1stUIP - max: 19 avg: 0.596244 CCLLen lastUIP - max: 32 avg: 8.62911
FormulaCache stats: memUse: 807628 cached: 1940 used Buckets: 1937 cache retrievals: 629 cache tries: 1940
Time: 0.621364s
Runtime:0.621364 ('The time taken by D4/Dsharp_PCompile is ', 0.6676230430603027) ('The time taken to parse the nnf text:', 0.04232501983642578) ('The time taken for Model Counting:', 0.16436100006103516) ('Model Count limited to var in dDNNF:', mpfr('1.4659544630212627e-70')) ('The time taken by sampling:', 0.02062702178955078) ('Samples saved to', 'samples.txt')
The correct model count is 8690991616 eijks349.aig_4.txt