From 4a532ca05a8d22c9e51f7bef93ce0bdc3c48a7e1 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Thu, 8 Dec 2022 21:48:36 -0500 Subject: [PATCH 1/2] Fix for the tautology bug in nnf. --- bauhaus/utils.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bauhaus/utils.py b/bauhaus/utils.py index 8b9ca7a..cac9f8c 100644 --- a/bauhaus/utils.py +++ b/bauhaus/utils.py @@ -173,7 +173,7 @@ def _nnfify(lit): if not T.satisfiable(): return 0 - return dsharp.compile(T.to_CNF(), smooth=True).model_count() + return dsharp.compile(T.to_CNF(simplify_tautologies=False), smooth=True).model_count() def likelihood(base_formula, lit): return count_solutions(base_formula, [lit]) / count_solutions(base_formula) From 7dd551e83a967fb31cdb4e72eaba0759f72e4612 Mon Sep 17 00:00:00 2001 From: Christian Muise Date: Tue, 13 Dec 2022 00:02:45 -0500 Subject: [PATCH 2/2] Fixing syntax. --- bauhaus/utils.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bauhaus/utils.py b/bauhaus/utils.py index cac9f8c..8d984cc 100644 --- a/bauhaus/utils.py +++ b/bauhaus/utils.py @@ -173,7 +173,7 @@ def _nnfify(lit): if not T.satisfiable(): return 0 - return dsharp.compile(T.to_CNF(simplify_tautologies=False), smooth=True).model_count() + return dsharp.compile(T.to_CNF(simplify=False), smooth=True).model_count() def likelihood(base_formula, lit): return count_solutions(base_formula, [lit]) / count_solutions(base_formula)