How to solve a DNF-SAT problem with PySAT?

Question

is there any support for DNF formulas with PySAT? For example, can I call a SAT solver on a DNF formula using this module. In particular is there any way to turn a DNF into CNF using this python module?

I looked at the documentation but there seems to be no mention of DNF formulas at all.

Answer 1

Disjunctive Normal Form (DNF) corresponds to the rows of a truth-table where the output value is 1 or true. Therefore, DNF already lists all solutions for the expression to be solved. No SAT solving is required in this case.

SAT solvers come into play for Conjunctive Normal Form (CNF). They are also used, if the expression(s) relate to circuits of logical gates.