In Sat, there is a cnf function which I wrote myself. It's the naive algorithm. Which may be ok. It's certainly easier to debug. But it may be worth, if performance becomes an issue, replacing with Tseitin.
There may be some obstacles to that. And the formulas are typically not very big, so it is not guaranteed to be a good idea.
In
Sat, there is acnffunction which I wrote myself. It's the naive algorithm. Which may be ok. It's certainly easier to debug. But it may be worth, if performance becomes an issue, replacing with Tseitin.There may be some obstacles to that. And the formulas are typically not very big, so it is not guaranteed to be a good idea.