如何将布尔表达式转换为cnf文件?
作者:互联网
我需要使用sat解算器来检查布尔表达式的可满足性.
我有像这样的复杂布尔表达式
是否有任何自动cnf文件转换器,以便我可以直接给坐在求解器?
我读了cnf格式文件..但是如何在.cnf文件中表达这个表达式?当paranthesis里面有一个连词以及如何表达时,我会感到困惑 – >和< - > ?请帮我
解决方法:
有几种解决方案.
Limboole是一个开源工具,我认为它包含一个单独的’CNF’转换器的命题逻辑.
更一般地说,您还可以使用支持命题逻辑的工具;一些例子包括Z3,CVC3和Yices.
标签:java,boolean-expression,sat-solvers,conjunctive-normal-form 来源: https://codeday.me/bug/20190610/1212497.html