0

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

示例：p /\ (p -> q) /\ (p -> ~r) /\ (~r / ~s) /\ (s / ~q)

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

4

1 回答 1

0

这是你的作业，所以没有人会为你做。如果您被困在某个特定点，我们可以提供帮助，但我们不会做您应该做的工作。

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

  • 首先，在 variuos 子句中拆分输入字符串
  • 然后你可能想要转换析取的含义（你知道规则，不是吗）
  • 目前已知的算法已经不少了，不知道老师希望你做什么。假设我们采用最简单的解决方案：为变量生成所有可能的真值赋值，并检查每个子句的结果真值。请注意，您正在使用连词，因此只要一个子句为假，整个 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
于 2021-10-04T14:54:17.177 回答