pysat
pysat copied to clipboard
Obtaining equisatisfiable CNF
Hello, this might be a documentation issue. I am a novice user (also not familiar with Python) and I was puzzled for a while trying to obtain an equisatisfiable CNF from e.g. f=Implies(Atom('x'),And('y','z'))
. After f.clausify()
, f.clauses
does not return what I expected. I did not find how to do it in the online documentation, so finally I decided to look at formula.py
and found that the __iter__
method of Formula
allows me to obtain the clauses I wanted as [c for c in f]
. It does not appear in the documentation yet it seems documented in the code, so I presume it's an issue with the setup of the documentation generator.