pysathq / pysat

A toolkit for SAT-based prototyping in Python
https://pysathq.github.io/
MIT License
386 stars 69 forks source link

Obtaining equisatisfiable CNF #175

Open nano-o opened 2 months ago

nano-o commented 2 months ago

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.

alexeyignatiev commented 2 months ago

Thanks for reporting, @nano-o!