如何识别两个CNF公式的公共子句数量？偏好Z3等SMT求解器方案

核心需求拆解 #

你需要的是超越语法匹配、基于语义等价的CNF公共子句计数，即判断两个子句是否在所有变量赋值下真值完全一致，而非仅仅字符串或符号序列相同。比如(x1∨¬x2)和(¬x2∨x1)虽然语法顺序不同，但语义等价，应被算作公共子句。

基于Z3 SMT求解器的实现方案 #

实现思路 #

1. 将两个CNF公式拆解为独立子句的集合C1和C2
2. 对每个子句c1 ∈ C1，遍历C2中的子句c2，通过Z3验证c1 ↔ c2是否为永真式（即逻辑等价）
3. 统计满足等价条件的子句对，注意去重（避免同一等价类被重复计数）

代码示例（Python + Z3） #

from z3 import *

def parse_clause(clause_str):
    # 解析子句字符串为Z3表达式，可根据实际输入格式调整
    clause_str = clause_str.strip('()')
    literals = clause_str.split('∨')
    exprs = []
    for lit in literals:
        lit = lit.strip()
        if lit.startswith('¬'):
            var = lit[1:]
            exprs.append(Not(Bool(var)))
        else:
            exprs.append(Bool(lit))
    return Or(*exprs)

def are_clauses_equivalent(c1, c2):
    # 验证c1和c2是否语义等价：c1 ↔ c2 是永真式
    s = Solver()
    s.add(Not(Equiv(c1, c2)))
    return s.check() == unsat

def count_common_semantic_clauses(cnf1_clauses, cnf2_clauses):
    z3_c1 = [parse_clause(c) for c in cnf1_clauses]
    z3_c2 = [parse_clause(c) for c in cnf2_clauses]
    
    # 标记已匹配的子句，避免重复计数
    matched_in_c2 = [False] * len(z3_c2)
    count = 0
    
    for c1 in z3_c1:
        for idx, c2 in enumerate(z3_c2):
            if not matched_in_c2[idx] and are_clauses_equivalent(c1, c2):
                count += 1
                matched_in_c2[idx] = True
                break  # 每个c1仅匹配一个c2，需多匹配可移除该行
    
    return count

# 示例测试
cnf1 = ["(x1∨¬x2)", "(¬x1∨x3)", "(x2∨¬x3)"]
cnf2 = ["(x1∨¬x2)", "(x2∨¬x3)", "(x1∨x3)"]
print("公共语义等价子句数量：", count_common_semantic_clauses(cnf1, cnf2))  # 输出2

关键说明 #

• parse_clause函数需根据实际的CNF输入格式调整（比如处理不同否定符号、变量命名规则）
• 若允许同一子句在两个公式中多次出现并重复计数，可移除matched_in_c2的标记逻辑
• 语义等价检查的核心是验证Equiv(c1,c2)的否定不可满足，即不存在赋值让两者真值不同

原问题优化表述建议 #

为避免歧义，建议将问题明确为以下两种之一：

1. 语义等价公共子句计数：统计两个CNF公式中相互语义等价的子句对数量（或不同等价类的数量），需说明是否允许重复计数（如同一子句在公式中多次出现的情况）
2. 语法匹配公共子句计数：仅统计字符串/符号序列完全一致的子句数量，需说明是否忽略子句内文字的顺序（如(x1∨x2)和(x2∨x1)是否算作相同子句）

补充：CNF公式的子句顺序不影响逻辑含义，统计时无需考虑子句在公式中的位置。

内容的提问来源于stack exchange，提问作者andre_c