Closed jmhorcas closed 2 years ago
I've refactored the AST functionality transformation to NNF (to_nnf()) and CNF (to_cnf()) and get_clauses() methods.
I relied on the algorithms from [Alexander Knüppel. The Role of Complex Constraints in Feature Modeling. Master's Thesis. 2016] and from [Büning, Hans Kleine, and Theodor Lettmann. Propositional logic: deduction and algorithms. Vol. 48. Cambridge University Press, 1999.]. So that, we are more confortable with this implementation than the previous one. All tests in benchmarking that previous implementation passed this also passes, as well as the tests from pysat plugin.
Fix the bug with distribute OR in converting AST to CNF.