-
Notifications
You must be signed in to change notification settings - Fork 0
Description
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