Feature: Tseytin transformation for converting arbitrary propositional formulas to CNF

[AzeezDa]

Dear Maintainers of rustsat,

Thank you for the useful and incredible library!

I noticed that the library does not provide a way to negate Cnfs. (Or I may have missed it.)
One simple way to achieve this is using the Tseytin transformation on the negated CNF.

Would it be possible to add such a feature to rustsat?

Best regards

[chrjabs]

Hi. This question goes beyond just negating CNFs. Support for converting any arbitrary propositional formula to CNF via the Tseitin transformation (similar to what PySAT supports since a while) would be a really cool feature, but not one that's very high priority on my todo list.

If anyone wants to work on this, I'd gladly give feedback and help getting this implemented. I think roughly the following would be needed.

• A new type (maybe PropFormula or so) representing an arbitrary propositional formula
• A bunch of operator implementations for Lit Var Clause Cnf PropFormula etc for conveniently building propositional formulas
• A Tseitin encoder that recursively converts any PropFormula to CNF

If anyone is interested in working on this, let me know and we can discuss this more.