pysat icon indicating copy to clipboard operation
pysat copied to clipboard

Obtaining equisatisfiable CNF

Open nano-o opened this issue 7 months ago • 1 comments

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.

nano-o avatar Jul 11 '24 05:07 nano-o