Skip to content

report the correct number of variables in unsat nnf#14

Merged
haz merged 1 commit intoQuMuLab:masterfrom
symphorien:unsat-nvars
Jul 4, 2021
Merged

report the correct number of variables in unsat nnf#14
haz merged 1 commit intoQuMuLab:masterfrom
symphorien:unsat-nvars

Conversation

@symphorien
Copy link

I should have seen it while reviewing #13

@haz
Copy link
Contributor

haz commented Jun 30, 2021

Hrmz...do satisfiable theories with un-smooth outputs include the correct variable count? Now I'm wondering if it only reports the number of variables that actually appear in the d-DNNF...

@symphorien
Copy link
Author

Yes:

$  cat foo.cnf
p cnf 10 1
1 0
$  ./dsharp -Fnnf nnf -Fgraph graph foo.cnf  
$  cat nnf 
nnf 1 1 10
L 1

@haz haz merged commit 7443df8 into QuMuLab:master Jul 4, 2021
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

Successfully merging this pull request may close these issues.

2 participants