CNF简化 [英] CNF simplification

问题描述

给定一组子句，我想首先检查它们是否可以满足要求.如果是的话，我想简化它们并创建一个CNF，例如(a OR b)^(NOt b)应该简化为:a ^(NOt b).我只使用命题公式.我尝试使用Java SAT4j库来执行此操作.它可以告诉我这组子句是否令人满意，但是似乎没有任何方法可以返回简化的CNF.如何有效简化CNF?有任何Java或Python实现吗?

Given a set of clauses, I want to first check whether they are satisfiable. If they are, I want to simplify them and create a CNF, eg., (a OR b) ^ (NOT b) should simplify to: a ^ (NOT b). I'm only working with propositional formulas. I've tried to use Java SAT4j library for doing this. It can show me whether the set of clauses are satisfiable, but doesn't seem to have any method for returning me a simplified CNF. What can I do for simplifying CNF efficiently? Are there any Java or Python implementations for this?

推荐答案

您可以使用 Riss3g

You could use the Riss3g Coprocessor of Norbert Manthey to simplify your CNF.

SAT求解器 minisat 2 允许

The SAT solver minisat 2 allows to store the preprocessed CNF in a file.

Lingeling ，来自奥地利的SAT求解器可以选择"-s"来简化条款.

Lingeling, a SAT solver from Austria has an option "-s" to simplify CNF clauses.

要将布尔表达式转换为简化的CNF，可以使用 bc2cnf .

To convert a Boolean expression into a simplified CNF, you could use bc2cnf.

这篇关于CNF简化的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！