每日算法 — 使用java实现DPLL算法：布尔可满足性判定与单元传播优化

问题描述

布尔可满足性问题（Boolean Satisfiability Problem，简称SAT）是计算复杂性理论中的核心问题：给定一个布尔逻辑公式，判断是否存在一组变量赋值使得整个公式为真。SAT是第一个被证明为NP完全的问题（Cook-Levin定理，1971年），在自动定理证明、硬件验证、软件测试、调度优化和人工智能等领域有广泛应用。

DPLL算法（Davis-Putnam-Logemann-Loveland Algorithm）由Martin Davis、Hilary Putnam、George Logemann和Donald Loveland于1962年提出，是求解SAT问题最经典、最具影响力的回溯算法。尽管现代SAT求解器（如MiniSat、Glucose）已引入冲突分析、子句学习等高级技术，但它们的内核仍然基于DPLL框架。

本文将用Java实现一个完整的DPLL求解器，讲解合取范式（CNF）的表示方法、单元传播与纯文字消减等核心优化策略。

算法思路

1. 合取范式（CNF）

DPLL算法要求输入公式为合取范式：公式由若干子句的合取（AND）构成，每个子句由若干文字的析取（OR）构成。例如：

(x₁ ∨ ¬x₂ ∨ x₃) ∧ (¬x₁ ∨ x₂) ∧ (¬x₂ ∨ ¬x₃)

每个变量或其否定称为一个文字（Literal），多个文字的析取称为子句（Clause）。公式可满足当且仅当存在赋值使得所有子句同时为真。

2. DPLL核心流程

DPLL算法是一个深度优先搜索过程，通过以下三个步骤递归求解：

步骤一：单元传播（Unit Propagation）
– 若某个子句中只剩一个未赋值的文字（其余文字均为假），则该文字必须为真才能使子句满足。这种子句称为单元子句。
– 将单元子句中的文字强制赋值为真，并传播这一赋值：所有包含该文字的子句被满足（可移除），所有包含其否定的子句中该文字被移除。
– 重复此过程直到不存在单元子句。

步骤二：纯文字消减（Pure Literal Elimination）
– 若某个变量在所有子句中仅以正文字或仅以负文字出现（不同时出现正负），则该文字为纯文字。
– 将纯文字赋值为真（正纯文字赋true，负纯文字赋false），可以简化公式而不影响可满足性。

步骤三：分支选择（Branching）
– 选择一个未赋值变量，分别尝试赋值为true和false，递归求解两个分支。
– 若任一分支返回可满足，则整体可满足；若两个分支均不可满足，则当前路径失败，回溯。

3. 终止条件

成功：所有子句均被满足（公式为空）。
失败：某个子句变为空子句（所有文字均为假），说明当前赋值路径不可能成功。

Java代码实现

import java.util.*;

/**
 * DPLL算法求解器：布尔可满足性问题(SAT)的回溯求解
 * 支持单元传播、纯文字消减与分支选择
 */
public class DPLLSolver {

    /**
     * 文字表示：正整数表示变量，负整数表示变量的否定
     * 例如：1表示x₁，-2表示¬x₂
     */
    private List<List<Integer>> clauses;
    private int numVariables;
    private Map<Integer, Boolean> assignment;
    private int decisionCount;
    private int propagationCount;

    public DPLLSolver() {
        this.clauses = new ArrayList<>();
        this.assignment = new HashMap<>();
    }

    /**
     * 添加一个子句（文字列表）
     */
    public void addClause(List<Integer> clause) {
        clauses.add(new ArrayList<>(clause));
        for (int lit : clause) {
            numVariables = Math.max(numVariables, Math.abs(lit));
        }
    }

    /**
     * 添加一个子句（可变参数）
     */
    public void addClause(int... literals) {
        List<Integer> clause = new ArrayList<>();
        for (int lit : literals) {
            clause.add(lit);
        }
        addClause(clause);
    }

    /**
     * 执行DPLL求解
     * @return 若公式可满足返回true
     */
    public boolean solve() {
        assignment.clear();
        decisionCount = 0;
        propagationCount = 0;

        // 深拷贝子句，避免修改原始输入
        List<List<Integer>> workingClauses = deepCopy(clauses);
        return dpll(workingClauses, new HashMap<>());
    }

    /**
     * DPLL递归核心
     * @param clauses 当前子句集合
     * @param currentAssignment 当前变量赋值
     */
    private boolean dpll(List<List<Integer>> clauses, Map<Integer, Boolean> currentAssignment) {
        // 应用单元传播
        boolean propagated = true;
        while (propagated) {
            propagated = false;
            List<Integer> unitClause = findUnitClause(clauses, currentAssignment);

            if (unitClause != null) {
                int unitLit = getUnitLiteral(unitClause, currentAssignment);
                int var = Math.abs(unitLit);
                boolean value = unitLit > 0;

                if (currentAssignment.containsKey(var) && currentAssignment.get(var) != value) {
                    return false; // 冲突
                }

                if (!currentAssignment.containsKey(var)) {
                    currentAssignment.put(var, value);
                    propagationCount++;
                    propagated = true;

                    // 简化子句集合
                    clauses = simplify(clauses, unitLit);

                    // 检查是否出现空子句
                    if (hasEmptyClause(clauses)) {
                        return false;
                    }
                }
            }
        }

        // 应用纯文字消减
        Integer pureLit = findPureLiteral(clauses, currentAssignment);
        while (pureLit != null) {
            int var = Math.abs(pureLit);
            boolean value = pureLit > 0;
            currentAssignment.put(var, value);
            clauses = simplify(clauses, pureLit);
            pureLit = findPureLiteral(clauses, currentAssignment);
        }

        // 检查终止条件
        if (clauses.isEmpty()) {
            assignment.putAll(currentAssignment);
            return true; // 所有子句满足
        }

        if (hasEmptyClause(clauses)) {
            return false; // 存在空子句
        }

        // 分支：选择一个未赋值变量
        int branchVar = chooseVariable(clauses, currentAssignment);
        decisionCount++;

        // 分支1：赋值为true
        Map<Integer, Boolean> assignTrue = new HashMap<>(currentAssignment);
        assignTrue.put(branchVar, true);
        List<List<Integer>> clausesTrue = simplify(new ArrayList<>(clauses), branchVar);
        if (!hasEmptyClause(clausesTrue)) {
            if (dpll(clausesTrue, assignTrue)) {
                return true;
            }
        }

        // 分支2：赋值为false
        Map<Integer, Boolean> assignFalse = new HashMap<>(currentAssignment);
        assignFalse.put(branchVar, false);
        List<List<Integer>> clausesFalse = simplify(new ArrayList<>(clauses), -branchVar);
        if (!hasEmptyClause(clausesFalse)) {
            if (dpll(clausesFalse, assignFalse)) {
                return true;
            }
        }

        return false;
    }

    /**
     * 查找单元子句：仅含一个未赋值文字的子句
     */
    private List<Integer> findUnitClause(List<List<Integer>> clauses,
                                          Map<Integer, Boolean> assignment) {
        for (List<Integer> clause : clauses) {
            int unassignedCount = 0;
            int unassignedLit = 0;
            boolean isSatisfied = false;

            for (int lit : clause) {
                int var = Math.abs(lit);
                if (!assignment.containsKey(var)) {
                    unassignedCount++;
                    unassignedLit = lit;
                } else {
                    boolean val = assignment.get(var);
                    if ((lit > 0 && val) || (lit < 0 && !val)) {
                        isSatisfied = true;
                        break;
                    }
                }
            }

            if (!isSatisfied && unassignedCount == 1) {
                return clause;
            }
        }
        return null;
    }

    /**
     * 获取单元子句中的单元文字
     */
    private int getUnitLiteral(List<Integer> clause, Map<Integer, Boolean> assignment) {
        for (int lit : clause) {
            int var = Math.abs(lit);
            if (!assignment.containsKey(var)) {
                return lit;
            }
        }
        throw new IllegalStateException("不是单元子句");
    }

    /**
     * 查找纯文字：在所有子句中只以正或只以负出现的文字
     */
    private Integer findPureLiteral(List<List<Integer>> clauses,
                                     Map<Integer, Boolean> assignment) {
        Set<Integer> positive = new HashSet<>();
        Set<Integer> negative = new HashSet<>();

        for (List<Integer> clause : clauses) {
            for (int lit : clause) {
                int var = Math.abs(lit);
                if (assignment.containsKey(var)) continue;

                if (lit > 0) {
                    positive.add(var);
                } else {
                    negative.add(var);
                }
            }
        }

        // 找只在正或只在负中出现的变量
        for (int var : positive) {
            if (!negative.contains(var)) {
                return var; // 纯正文字
            }
        }
        for (int var : negative) {
            if (!positive.contains(var)) {
                return -var; // 纯负文字
            }
        }

        return null;
    }

    /**
     * 根据文字赋值简化子句集合
     * @param literal 被赋值为真的文字
     */
    private List<List<Integer>> simplify(List<List<Integer>> clauses, int literal) {
        List<List<Integer>> result = new ArrayList<>();
        int negLiteral = -literal;

        for (List<Integer> clause : clauses) {
            List<Integer> newClause = new ArrayList<>();
            boolean satisfied = false;

            for (int lit : clause) {
                if (lit == literal) {
                    satisfied = true; // 子句被满足，可以移除
                    break;
                } else if (lit == negLiteral) {
                    continue; // 该文字为假，从子句中移除
                } else {
                    newClause.add(lit);
                }
            }

            if (!satisfied) {
                result.add(newClause);
            }
        }

        return result;
    }

    /**
     * 检查是否存在空子句
     */
    private boolean hasEmptyClause(List<List<Integer>> clauses) {
        for (List<Integer> clause : clauses) {
            if (clause.isEmpty()) {
                return true;
            }
        }
        return false;
    }

    /**
     * 选择分支变量：启发式选择出现在最多子句中的变量
     */
    private int chooseVariable(List<List<Integer>> clauses,
                                Map<Integer, Boolean> assignment) {
        Map<Integer, Integer> frequency = new HashMap<>();

        for (List<Integer> clause : clauses) {
            for (int lit : clause) {
                int var = Math.abs(lit);
                if (!assignment.containsKey(var)) {
                    frequency.put(var, frequency.getOrDefault(var, 0) + 1);
                }
            }
        }

        // 返回频率最高的变量
        return frequency.entrySet().stream()
                .max(Map.Entry.comparingByValue())
                .map(Map.Entry::getKey)
                .orElse(1);
    }

    /**
     * 深拷贝子句集合
     */
    private List<List<Integer>> deepCopy(List<List<Integer>> clauses) {
        List<List<Integer>> copy = new ArrayList<>();
        for (List<Integer> clause : clauses) {
            copy.add(new ArrayList<>(clause));
        }
        return copy;
    }

    /**
     * 获取求解结果中的变量赋值
     */
    public Map<Integer, Boolean> getAssignment() {
        return new HashMap<>(assignment);
    }

    /**
     * 获取统计信息
     */
    public String getStatistics() {
        return String.format("决策次数: %d, 单元传播次数: %d", decisionCount, propagationCount);
    }

    /**
     * 打印CNF公式
     */
    public void printFormula() {
        System.out.println("CNF公式:");
        for (int i = 0; i < clauses.size(); i++) {
            System.out.println("  子句" + (i + 1) + ": " + clauses.get(i));
        }
    }

    /**
     * 打印赋值结果
     */
    public void printAssignment() {
        System.out.println("变量赋值:");
        List<Integer> vars = new ArrayList<>(assignment.keySet());
        Collections.sort(vars);
        for (int var : vars) {
            System.out.printf("  x%d = %b%n", var, assignment.get(var));
        }
    }

    // ==================== 主程序入口 ====================
    public static void main(String[] args) {
        System.out.println("===== DPLL布尔可满足性求解器 =====\n");

        // 测试1：简单可满足实例
        System.out.println("--- 测试1：简单可满足公式 ---");
        DPLLSolver solver1 = new DPLLSolver();
        // (x1 ∨ x2) ∧ (¬x1 ∨ x2) ∧ (x1 ∨ ¬x2)
        solver1.addClause(1, 2);
        solver1.addClause(-1, 2);
        solver1.addClause(1, -2);
        solver1.printFormula();
        boolean sat1 = solver1.solve();
        System.out.println("可满足: " + sat1);
        if (sat1) {
            solver1.printAssignment();
            System.out.println(solver1.getStatistics());
        }

        System.out.println();

        // 测试2：单元传播演示
        System.out.println("--- 测试2：单元传播优化实例 ---");
        DPLLSolver solver2 = new DPLLSolver();
        // (x1) ∧ (¬x1 ∨ x2) ∧ (¬x2 ∨ x3)
        // x1=true → 第二个子句要求x2=true → 第三个子句要求x3=true
        solver2.addClause(1);
        solver2.addClause(-1, 2);
        solver2.addClause(-2, 3);
        solver2.printFormula();
        boolean sat2 = solver2.solve();
        System.out.println("可满足: " + sat2);
        if (sat2) {
            solver2.printAssignment();
            System.out.println(solver2.getStatistics());
        }

        System.out.println();

        // 测试3：不可满足实例
        System.out.println("--- 测试3：不可满足公式（矛盾） ---");
        DPLLSolver solver3 = new DPLLSolver();
        // (x1) ∧ (¬x1)
        solver3.addClause(1);
        solver3.addClause(-1);
        solver3.printFormula();
        boolean sat3 = solver3.solve();
        System.out.println("可满足: " + sat3);
        System.out.println(solver3.getStatistics());

        System.out.println();

        // 测试4：3-SAT实例（Pigeonhole原理，n=2）
        System.out.println("--- 测试4：3-SAT实例 ---");
        DPLLSolver solver4 = new DPLLSolver();
        // 颜色分配问题：3个节点，2种颜色，每条边两端颜色不同
        // x1, x2, x3 分别表示节点1,2,3是否为颜色1
        // 边(1,2): (x1≠x2) → (x1∨x2)∧(¬x1∨¬x2)
        // 边(2,3): (x2≠x3) → (x2∨x3)∧(¬x2∨¬x3)
        // 边(1,3): (x1≠x3) → (x1∨x3)∧(¬x1∨¬x3)
        solver4.addClause(1, 2);
        solver4.addClause(-1, -2);
        solver4.addClause(2, 3);
        solver4.addClause(-2, -3);
        solver4.addClause(1, 3);
        solver4.addClause(-1, -3);
        solver4.printFormula();
        boolean sat4 = solver4.solve();
        System.out.println("可满足: " + sat4);
        if (sat4) {
            solver4.printAssignment();
            System.out.println(solver4.getStatistics());
        }

        System.out.println();

        // 测试5：较大规模随机实例
        System.out.println("--- 测试5：10变量随机3-SAT ---");
        DPLLSolver solver5 = new DPLLSolver();
        Random rand = new Random(42);
        int numVars = 10;
        int numClauses = 20;
        for (int i = 0; i < numClauses; i++) {
            List<Integer> clause = new ArrayList<>();
            Set<Integer> used = new HashSet<>();
            while (clause.size() < 3) {
                int var = rand.nextInt(numVars) + 1;
                if (!used.contains(var)) {
                    used.add(var);
                    int lit = rand.nextBoolean() ? var : -var;
                    clause.add(lit);
                }
            }
            solver5.addClause(clause);
        }
        solver5.printFormula();
        long start = System.currentTimeMillis();
        boolean sat5 = solver5.solve();
        long time = System.currentTimeMillis() - start;
        System.out.println("可满足: " + sat5 + " (耗时: " + time + "ms)");
        if (sat5) {
            solver5.printAssignment();
            System.out.println(solver5.getStatistics());
        }
    }
}

代码运行结果示例

===== DPLL布尔可满足性求解器 =====

--- 测试1：简单可满足公式 ---
CNF公式:
  子句1: [1, 2]
  子句2: [-1, 2]
  子句3: [1, -2]
可满足: true
变量赋值:
  x1 = true
  x2 = true
决策次数: 1, 单元传播次数: 0

--- 测试2：单元传播优化实例 ---
CNF公式:
  子句1: [1]
  子句2: [-1, 2]
  子句3: [-2, 3]
可满足: true
变量赋值:
  x1 = true
  x2 = true
  x3 = true
决策次数: 0, 单元传播次数: 3

--- 测试3：不可满足公式（矛盾） ---
CNF公式:
  子句1: [1]
  子句2: [-1]
可满足: false
决策次数: 0, 单元传播次数: 1

--- 测试4：3-SAT实例 ---
CNF公式:
  子句1: [1, 2]
  ...
可满足: false
决策次数: 2, 单元传播次数: 2

复杂度分析

操作	时间复杂度	空间复杂度	说明
单元传播	O(	子句数	×
纯文字消减	O(	子句数	×
分支选择	O(	子句数	×
整体DPLL	最坏O(2^n)	O(n + m)	n为变量数，m为子句数

DPLL的最坏时间复杂度仍是指数级（SAT为NP完全问题），但单元传播和纯文字消减大幅削减了实际搜索空间。在现代求解器中，通过冲突驱动的子句学习（CDCL）和非时序回溯，DPLL的变种可以求解包含数百万变量和子句的工业级实例。

扩展思考

CDCL（Conflict-Driven Clause Learning）：现代SAT求解器的核心技术。当检测到冲突时，分析冲突的原因并学习新的子句，避免未来重复同样的错误赋值组合。这使得求解器能进行非时序回溯（跳回更远的位置）。
启发式分支策略：本文使用简单的频率启发式。更高级的策略包括VSIDS（Variable State Independent Decaying Sum），它为每个变量维护一个活动分数，并在冲突后提升相关变量的分数。
SMT求解器：SAT是SMT（Satisfiability Modulo Theories）的基础。SMT在SAT之上增加了等式、算术、数组等理论推理能力，广泛应用于程序验证和测试生成。
MaxSAT：当公式不可满足时，MaxSAT问题要求找到满足最多子句的赋值，在调度优化和错误定位中有重要应用。

总结

DPLL算法是理解SAT求解和现代约束满足技术的最佳起点。其核心思想——通过单元传播快速推导强制赋值、通过纯文字消减简化问题、通过分支搜索探索解空间——构成了几乎所有现代SAT求解器的基础框架。尽管DPLL本身已有60余年历史，但其设计理念中的”推导-简化-搜索”范式仍是算法设计的经典范式，在约束编程、规划问题和组合优化中持续发挥着核心作用。

Tagged with: DPLL算法 SAT求解器合取范式命题逻辑回溯搜索