检查2-CNF布尔函数可以满足的,用解析方法吗?

Question

输入是2-CNF中的布尔公式，以符号字符串的形式给出。

示例:p/ (p ->Q)/ (p ->~r)/ (~r/~s)/ (s/~q)

我正在使用分辨率方法来解决这个2cnf问题，但我被困在如何比较python中两个子句的字面量，因为我们需要检查变量及其在另一个子句

中的否定

Answer 1

这是你的作业，所以没有人会帮你做。如果你在某一点上卡住了，我们可以帮助你，但我们不会做你应该做的工作。

也就是说，我可以给你一些关于如何组织代码的提示:

• 首先，在各个子句
中拆分输入字符串
• 那么你可能想要转换析取的含义(你知道规则，不是吗)
• 在这一点上有相当多的已知算法，我不知道你的老师希望你做什么。假设我们采用最简单的解决方案:为变量生成所有可能的真值赋值，并检查每个子句的结果真值。请注意，您正在使用连接词，因此只要一个子句为假，整个CNF就为假

编辑

很抱歉误解了你的问题。simpy有一个具有许多功能的logic模块，包括分辨率功能。但是如果你需要将自己限制在标准库中，那么你将不得不使用字符串。

我假设每个子句是:a)单个文字;B)有两个字面意思的暗示;C)两个或多个字面值的分离，并且每个变量恰好是1个字符。如果我们想要管理更复杂的情况，我们需要定义一个简单的标记器。

这是第一个函数的可能代码:

def is_sat(cnf):
str_clauses = cnf.translate(str.maketrans("", "", "() ")).split("/\")
vars = {x for x in cnf if x in "abcdefghijklmnopqrstuvwxyz"}
clauses = []
for str_clause in str_clauses:
if "->" in str_clause: ## <lit1 -> lit2>
a,b = str_clause.split("->")
clauses.append(set((negate(a), b)))
elif "/" in str_clause: ## <lit1 / ... / litn>
clauses.append(set(str_clause.split("/")))
else: ##<lit1>
clauses.append(set([str_clause]))
for var in vars:
##remove tautologies
tautology = set((var, negate(var)))
for i,clause in enumerate(clauses[:]):
if tautology == clause:
del clauses[i]
elif tautology < clause:
clause -= tautology
if not clauses:
return True
##resolutions
asserting = [i for i,c in enumerate(clauses) if var in c]
negating = [i for i,c in enumerate(clauses) if negate(var) in c]
while asserting and negating:
if asserting[-1] > negating[-1]:
x, y = asserting[-1], negating[-1]
del asserting[-1]
del negating[-1]
else:
y, x = asserting[-1], negating[-1]
del negating[-1]
del asserting[-1]
resolved = (clauses[x] | clauses[y]) - tautology
if not resolved:
return False
print(f'resolution: {clauses[x]}, {clauses[y]} => {resolved}')
del clauses[x]
del clauses[y]
clauses.append(resolved)
else:
return True
def negate(s):
if s[0] == '~':
return s[1:]
else:
return '~' + s