每日算法 — 使用java实现剧本杀：逻辑约束传播与贝叶斯概率推理

引言

剧本杀是一种依赖逻辑推理和信息交换的社交游戏，玩家需要通过线索分析、证言比对和逻辑推演找出真相。本文将剧本杀推理过程抽象为约束满足问题（CSP），用Java实现辅助推理系统，核心算法包括命题逻辑约束传播、贝叶斯概率推理更新，以及基于DPLL的回溯求解框架。

核心算法原理

1. 命题逻辑建模

将剧本杀中的每个事实建模为布尔变量：
– ( A_i )：嫌疑人 ( i ) 是凶手
– ( W_j )：线索 ( j ) 为真
– ( T_k )：时间线 ( k ) 成立

约束表示为子句集合，如 “只有一人是凶手”：
[ (A_1 \lor A_2 \lor \dots \lor A_n) \land \bigwedge_{i \neq j} (\neg A_i \lor \neg A_j) ]

2. 约束传播：单元传播

若子句中只有一个未赋值文字，则该文字必须为真。反复应用此规则可缩小搜索空间。

3. 贝叶斯概率推理

给定新证据 ( E )，更新各嫌疑人的后验概率：

[ P(A_i | E) = \frac{P(E | A_i) \cdot P(A_i)}{P(E)} ]

4. DPLL回溯求解

结合单元传播、纯文字消去和回溯搜索，判定约束系统的可满足性。

Java完整实现

import java.util.*;

/**
 * 剧本杀逻辑推理引擎
 * 核心算法：命题逻辑约束传播 + 贝叶斯概率更新 + DPLL回溯求解
 */
public class MurderMysterySolver {

    // 命题变量：嫌疑人是否为凶手
    private final int suspectCount;
    // 约束子句列表，每个子句是文字列表（正数表示正文字，负数表示负文字）
    private final List<List<Integer>> clauses;
    // 当前赋值：null=未赋值, true/false
    private Boolean[] assignment;
    // 先验概率
    private final double[] priorProb;
    // 后验概率
    private double[] posteriorProb;

    public MurderMysterySolver(int suspectCount) {
        this.suspectCount = suspectCount;
        this.clauses = new ArrayList<>();
        this.priorProb = new double[suspectCount];
        this.posteriorProb = new double[suspectCount];

        // 初始均匀先验
        for (int i = 0; i < suspectCount; i++) {
            priorProb[i] = 1.0 / suspectCount;
            posteriorProb[i] = priorProb[i];
        }

        // 添加"只有一人是凶手"约束
        // 至少一人：(A1 || A2 || ... || An)
        List<Integer> atLeastOne = new ArrayList<>();
        for (int i = 1; i <= suspectCount; i++) atLeastOne.add(i);
        clauses.add(atLeastOne);

        // 至多一人：对所有 i≠j，(!Ai || !Aj)
        for (int i = 1; i <= suspectCount; i++) {
            for (int j = i + 1; j <= suspectCount; j++) {
                List<Integer> atMostOne = new ArrayList<>();
                atMostOne.add(-i);
                atMostOne.add(-j);
                clauses.add(atMostOne);
            }
        }
    }

    /**
     * 添加新线索约束
     * @param clause 子句，如 [1, -2] 表示 "嫌疑人1是凶手 或 嫌疑人2不是凶手"
     */
    public void addClue(List<Integer> clause) {
        clauses.add(new ArrayList<>(clause));
    }

    /**
     * 单元传播：反复寻找单位子句并赋值
     * @param assign 当前赋值数组
     * @param clauses 子句集合
     * @return 若出现空子句则返回false（矛盾），否则返回true
     */
    private boolean unitPropagate(Boolean[] assign, List<List<Integer>> clauses) {
        boolean changed = true;
        while (changed) {
            changed = false;
            for (List<Integer> clause : clauses) {
                int unassignedCount = 0;
                int lastUnassigned = 0;
                boolean satisfied = false;

                for (int lit : clause) {
                    int var = Math.abs(lit);
                    if (assign[var - 1] == null) {
                        unassignedCount++;
                        lastUnassigned = lit;
                    } else {
                        boolean value = assign[var - 1];
                        if ((lit > 0 && value) || (lit < 0 && !value)) {
                            satisfied = true;
                            break;
                        }
                    }
                }

                if (satisfied) continue;
                if (unassignedCount == 0) return false; // 空子句，矛盾
                if (unassignedCount == 1) {
                    // 单元子句，强制赋值
                    int var = Math.abs(lastUnassigned);
                    assign[var - 1] = lastUnassigned > 0;
                    changed = true;
                }
            }
        }
        return true;
    }

    /**
     * DPLL回溯求解
     * @param assign 当前赋值
     * @param clauses 剩余子句
     * @return 是否存在满足赋值
     */
    private boolean dpll(Boolean[] assign, List<List<Integer>> clauses) {
        Boolean[] newAssign = assign.clone();
        if (!unitPropagate(newAssign, clauses)) return false;

        // 检查是否所有子句满足
        boolean allSatisfied = true;
        for (List<Integer> clause : clauses) {
            boolean sat = false;
            for (int lit : clause) {
                int var = Math.abs(lit);
                if (newAssign[var - 1] != null) {
                    if ((lit > 0 && newAssign[var - 1]) || (lit < 0 && !newAssign[var - 1])) {
                        sat = true;
                        break;
                    }
                } else {
                    allSatisfied = false;
                }
            }
            if (!sat && allSatisfied) return false;
        }
        if (allSatisfied) {
            this.assignment = newAssign;
            return true;
        }

        // 选择第一个未赋值变量
        int branchVar = -1;
        for (int i = 0; i < suspectCount; i++) {
            if (newAssign[i] == null) { branchVar = i; break; }
        }
        if (branchVar == -1) return true;

        // 分支：先尝试true
        newAssign[branchVar] = true;
        if (dpll(newAssign, clauses)) return true;

        // 回溯，尝试false
        newAssign[branchVar] = false;
        return dpll(newAssign, clauses);
    }

    /**
     * 求解当前约束系统
     */
    public boolean solve() {
        Boolean[] initAssign = new Boolean[suspectCount];
        return dpll(initAssign, clauses);
    }

    /**
     * 贝叶斯概率更新
     * @param evidence 证据：evidence[i] = 0/1/null 表示第i个线索为假/真/未知
     * @param likelihoods 似然矩阵：likelihoods[i][j] = P(证据j | 嫌疑人i是凶手)
     */
    public void updateProbabilities(int[] evidence, double[][] likelihoods) {
        int clueCount = evidence.length;
        double[] numerator = new double[suspectCount];
        double denominator = 0;

        for (int i = 0; i < suspectCount; i++) {
            double likelihoodProduct = 1.0;
            for (int j = 0; j < clueCount; j++) {
                if (evidence[j] == 1) {
                    likelihoodProduct *= likelihoods[i][j];
                } else if (evidence[j] == 0) {
                    likelihoodProduct *= (1 - likelihoods[i][j]);
                }
            }
            numerator[i] = likelihoodProduct * priorProb[i];
            denominator += numerator[i];
        }

        for (int i = 0; i < suspectCount; i++) {
            posteriorProb[i] = denominator > 0 ? numerator[i] / denominator : priorProb[i];
        }
    }

    /**
     * 获取当前最可能的凶手
     */
    public int getMostLikelySuspect() {
        int best = 0;
        for (int i = 1; i < suspectCount; i++) {
            if (posteriorProb[i] > posteriorProb[best]) best = i;
        }
        return best;
    }

    /**
     * 打印推理结果
     */
    public void printInference() {
        System.out.println("=== 剧本杀逻辑推理引擎 ===\n");
        System.out.println("约束子句:");
        for (List<Integer> clause : clauses) {
            System.out.println("  " + clause);
        }

        System.out.println("\nDPLL求解结果:");
        if (solve()) {
            System.out.println("  约束系统可满足");
            for (int i = 0; i < suspectCount; i++) {
                System.out.printf("  嫌疑人 %d: %s%n", i + 1, assignment[i] != null ? assignment[i] : "未知");
            }
        } else {
            System.out.println("  约束系统矛盾（存在虚假线索）");
        }

        System.out.println("\n贝叶斯概率推理:");
        for (int i = 0; i < suspectCount; i++) {
            System.out.printf("  嫌疑人 %d 概率: %.4f%n", i + 1, posteriorProb[i]);
        }
        System.out.printf("\n最可能凶手: 嫌疑人 %d (概率 %.4f)%n",
            getMostLikelySuspect() + 1, posteriorProb[getMostLikelySuspect()]);
    }

    public static void main(String[] args) {
        // 5人剧本杀
        MurderMysterySolver solver = new MurderMysterySolver(5);

        // 添加线索约束
        // 线索1：如果嫌疑人1不是凶手，则嫌疑人3有不在场证明
        solver.addClue(Arrays.asList(1, -3));

        // 线索2：嫌疑人2和嫌疑人4至少一人有动机
        solver.addClue(Arrays.asList(2, 4));

        // 线索3：如果嫌疑人5是凶手，则指纹证据为真（由其他约束处理）
        solver.addClue(Arrays.asList(-5, 5)); // 恒真，占位

        // 证据：3条线索 [真, 假, 真]
        int[] evidence = {1, 0, 1};

        // 似然矩阵：likelihoods[i][j] = P(证据j | 嫌疑人i是凶手)
        double[][] likelihoods = {
            {0.9, 0.2, 0.7},  // 嫌疑人1
            {0.3, 0.8, 0.4},  // 嫌疑人2
            {0.2, 0.9, 0.3},  // 嫌疑人3
            {0.6, 0.5, 0.8},  // 嫌疑人4
            {0.4, 0.3, 0.9}   // 嫌疑人5
        };

        solver.updateProbabilities(evidence, likelihoods);
        solver.printInference();
    }
}

复杂度分析

总结

本文构建了剧本杀辅助推理引擎，核心创新包括：
1. 命题逻辑建模：将游戏事实转化为布尔约束系统
2. DPLL高效求解：单元传播大幅剪枝，快速判定线索一致性
3. 贝叶斯概率更新：综合多条证据量化各嫌疑人嫌疑度
4. 约束传播：自动推导隐藏信息，辅助玩家逻辑推演

该系统可扩展应用于侦探小说推理、法律证据分析等更广泛的逻辑推理场景。