大规模DNF转无指数膨胀CNF及PySAT MaxSAT求解方案咨询

问题本质简化 #

你当前的问题本质是最大独立集求解：将每个整数编码的变量视作图的节点，双向互斥关系视作节点间的无向边，你需要选出最多的节点，使得任意两个节点之间没有边（即无互斥关系）。该场景完全不需要对原始DNF做复杂转换，可以直接建模为CNF格式的MaxSAT问题，无任何子句膨胀问题。

核心CNF建模逻辑 #

完全避开DNF转CNF的冗余步骤，直接按如下规则构造表达式：

• 硬约束（必须全部满足）：对每一对互斥变量u和v，添加CNF子句 ¬u ∨ ¬v，表示两个变量不能同时为真。
• 软约束（尽可能多满足）：对每个变量x，添加权重为1的单位软子句 x，表示我们优先让变量取值为真，最大化满足的软子句数量等价于最大化兼容变量的数量。

如果你确实需要对原始DNF表达式做Tseitin转换（比如有其他业务逻辑绑定了该DNF结构），可按如下步骤实现，子句数量仅为线性规模：

• 为DNF的每个析取项C_i（即(i & -2 & -3...)）引入一个新的辅助变量t_i
• 对每个t_i添加等价约束：t_i ↔ C_i，拆分为CNF子句为：
  • 对C_i里的每个文字l（包括i和所有互斥变量的取反），添加子句 ¬t_i ∨ l
  • 添加子句 t_i ∨ ¬i ∨ 2 ∨ 3 ∨ ...（即C_i所有文字取反后析取）
• 总硬约束为所有辅助变量的析取：t_1 ∨ t_2 ∨ ... ∨ t_n
• 软约束设置为每个t_i权重为1，最大化满足的t_i数量即可

PySAT实现参考 #

我们基于更高效的最大独立集建模给出实现，可直接支持10万级变量规模：

from pysat.solvers import RC2
from pysat.formula import WCNF

def solve_max_compatible(mutex_pairs: list[tuple[int, int]], var_count: int) -> list[int]:
    # 初始化加权CNF对象
    wcnf = WCNF()
    
    # 添加硬约束：互斥变量不能同时为真
    for u, v in mutex_pairs:
        wcnf.append([-u, -v])
    
    # 添加软约束：每个变量尽可能为真，权重统一为1
    for var in range(1, var_count + 1):
        wcnf.append([var], weight=1)
    
    # 调用RC2 MaxSAT求解器
    with RC2(wcnf) as solver:
        solver.compute()
        # 过滤出取值为真的变量即为兼容集合
        model = solver.get_model()
        return [lit for lit in model if lit > 0]

# 测试用例：2个变量互斥，预期返回[1]或[2]
if __name__ == "__main__":
    mutex_pairs = [(1, 2)]
    var_count = 2
    res = solve_max_compatible(mutex_pairs, var_count)
    print(f"最大兼容变量集合：{res}")

规模适配说明 #

10万级变量场景下，只要互斥对的数量不超过千万级，RC2求解器都可以正常处理。如果互斥关系存在分组（比如多个变量在同一个互斥组里，组内所有变量两两互斥），还可以用基数约束AtMost(group, 1)进一步压缩子句数量，PySAT的CardEnc类可以直接生成该约束的CNF编码。

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