MAXSAT求解后如何还原CNF转换前的原始变量值？

核心原理 #

limboole在将表达式转换为CNF时，会自动生成以c 开头的注释行，用来记录原始变量名与CNF内部变量编号的对应关系——这就是完成映射的核心依据。

具体步骤 #

• 提取映射关系：从limboole输出的CNF文件中，筛选所有c 开头的行，格式为c <CNF变量编号> <原始变量名>。

  示例注释行：
  c 2 v0
  c 8 v1
  c 5 v2
  把这些对应关系整理成字典，比如orig_to_cnf = {"v0": 2, "v1": 8, "v2": 5, ...}。

• 解析SAT求解结果：sat4j输出的最优解以v 开头，后续的数字遵循规则：

  • 正数：对应CNF编号的变量赋值为True（比如5表示CNF编号5的变量为真）
  • 负数：对应CNF编号的变量赋值为False（比如-2表示CNF编号2的变量为假）
    把这些值整理成cnf_to_val字典，键为CNF编号，值为布尔值。

• 映射回原始变量：遍历所有原始变量（比如v0、v1、v2...），通过orig_to_cnf找到对应的CNF编号，再从cnf_to_val中取出该编号的赋值结果，即可得到原始变量的最终取值。

自动化处理脚本（Python） #

当变量数量较多时，手动处理效率极低，可通过以下脚本快速完成映射：

# 1. 构建原始变量到CNF编号的映射字典
orig_to_cnf = {}
cnf_file_path = "your_cnf_output.cnf"
with open(cnf_file_path, "r", encoding="utf-8") as f:
    for line in f:
        line = line.strip()
        if line.startswith("c "):
            parts = line.split()
            cnf_id = int(parts[1])
            orig_var = parts[2]
            orig_to_cnf[orig_var] = cnf_id

# 2. 解析sat4j的解文件，记录CNF变量的赋值
cnf_to_val = {}
solution_file_path = "sat4j_solution.txt"
with open(solution_file_path, "r", encoding="utf-8") as f:
    for line in f:
        line = line.strip()
        if line.startswith("v "):
            for num_str in line.split()[1:]:
                num = int(num_str)
                cnf_id = abs(num)
                cnf_to_val[cnf_id] = num > 0

# 3. 输出所有原始变量的赋值结果
print("原始变量赋值结果：")
for var_name in sorted(orig_to_cnf.keys()):
    cnf_id = orig_to_cnf[var_name]
    val = cnf_to_val[cnf_id]
    print(f"{var_name}: {'True' if val else 'False'}")

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