Obtaining a conjunctive normal form of a PySMT formula

[Sanjai Narain]

Hello, I would appreciate any pointers for doing so. Formulas are constructed with Boolean combinations of Python calls (that return formulas) but how do we get the final formula into a CNF form? 

Doing write_smtlib(formula, 'file.smt') creates just a single assert statement in the file. 

Thanks. -- Sanjai 

[Marco Gario]

Hi Sanjai,

To use an SMT solver, you do not need the CNF. The SMT-LIB format is more permissive than the DIMACS format (used by SAT solvers).

If you want to use a SAT solver, you can use pysmt.rewritings.CNFizer . Note that this will give you an equisatisfiable formula in CNF, using the definitional encoding (aka Tseitin). However, if you wrote the formula in a form that is already CNF (or almost CNF), the rewriting will not realize it, and you might end up with something different from what you expect.

Finally, if you already wrote the formula in CNF, you should try the pysmt.shortcuts.to_smtlib function and set the parameter daggify=False. The usual translation that we do in smtlib (i.e., the one used by write_smtlib) writes the formula in a compact way, by creating aliases for sub-parts of the formulas that appear in many places. You can think of this as the difference between writing the formula as a tree or a DAG. This can lead to exponentially smaller formulae, and unless you have a good reason to want the CNF (education, debugging, etc.), I would suggest you use this format.

Note that the fact of having a single assert has nothing to do with the formula being in CNF, and pySMT will not create a file with multiple asserts. If this is what you need, you should look directly into the smtlib functionalities in pysmt.smtlib.script to see how to create an SMT-LIB script.

Let me know if you need additional clarifications.

Marco

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+unsubscribe@googlegroups.com.
To post to this group, send email to py...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/52266e81-1363-43ba-8c14-cbe67e215132%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Marco Gario]

Can you provide more information on what are you trying to accomplish?

Of the solutions I mentioned before, does anyone satisfy your needs? If not, why? 

Conjunctive partitionin takes a big conjunction, flattens it and returns each conjunct. It does not perform cnf conversion.

Marco 

On Tue, Mar 20, 2018, 10:36 Sanjai Narain <sanjai...@gmail.com> wrote:

Hi Marco: Thanks for your post. It is very helpful for understanding the internals of pysmt. Will try out the suggestions. 

Also discovered conjunctive_partition(formula) that seems to find the top-level conjunction. I would think that using it recursively would give a CNF? 

-- Sanjai

On Saturday, March 17, 2018 at 9:28:36 PM UTC-4, Marco Gario wrote:

Hi Sanjai,

To use an SMT solver, you do not need the CNF. The SMT-LIB format is more permissive than the DIMACS format (used by SAT solvers).

If you want to use a SAT solver, you can use pysmt.rewritings.CNFizer . Note that this will give you an equisatisfiable formula in CNF, using the definitional encoding (aka Tseitin). However, if you wrote the formula in a form that is already CNF (or almost CNF), the rewriting will not realize it, and you might end up with something different from what you expect.

Finally, if you already wrote the formula in CNF, you should try the pysmt.shortcuts.to_smtlib function and set the parameter daggify=False. The usual translation that we do in smtlib (i.e., the one used by write_smtlib) writes the formula in a compact way, by creating aliases for sub-parts of the formulas that appear in many places. You can think of this as the difference between writing the formula as a tree or a DAG. This can lead to exponentially smaller formulae, and unless you have a good reason to want the CNF (education, debugging, etc.), I would suggest you use this format.

Note that the fact of having a single assert has nothing to do with the formula being in CNF, and pySMT will not create a file with multiple asserts. If this is what you need, you should look directly into the smtlib functionalities in pysmt.smtlib.script to see how to create an SMT-LIB script.

Let me know if you need additional clarifications.

Marco

On Sat, Mar 17, 2018 at 6:35 PM, Sanjai Narain <sanjai...@gmail.com> wrote:

Hello, I would appreciate any pointers for doing so. Formulas are constructed with Boolean combinations of Python calls (that return formulas) but how do we get the final formula into a CNF form? 

Doing write_smtlib(formula, 'file.smt') creates just a single assert statement in the file. 

Thanks. -- Sanjai 

--
You received this message because you are subscribed to the Google Groups "pySMT" group.

To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+un...@googlegroups.com.

To post to this group, send email to py...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/52266e81-1363-43ba-8c14-cbe67e215132%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "pySMT" group.

To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+un...@googlegroups.com.

To post to this group, send email to py...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/f8a60ade-2833-449f-8855-42f15c8ac24c%40googlegroups.com.