Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Wrong model counts with DSharp-PCompile #3

Open
allrtaken opened this issue Mar 23, 2020 · 0 comments
Open

Wrong model counts with DSharp-PCompile #3

allrtaken opened this issue Mar 23, 2020 · 0 comments

Comments

@allrtaken
Copy link

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant