基于Python启发式的MiniSAT C++ pickBranchLit函数改造问询

API 探路者

2026-5-15

如何让MiniSAT的C++ pickBranchLit调用Python启发式逻辑？

问题背景

我正在优化MiniSAT的分支选择逻辑，用Python实现了自定义启发式，但需要让C代码中的pickBranchLit()函数调用Python的输出；同时Python要能获取C中变量的当前状态，来测试启发式的性能。这是我第一次做C++/Python交互，对自己的初步设计存疑，想请教：

我的设计是否合理？
如何修改C++的pickBranchLit代码以响应Python的输出？

原C++的pickBranchLit()代码：

Lit Solver::pickBranchLit() {
 Var next = var_Undef;
 // Random decision:
 if (drand(random_seed) < random_var_freq && !order_heap.empty()){
 next = order_heap[irand(random_seed,order_heap.size())];
 if (value(next) == l_Undef && decision[next]) rnd_decisions++;
 }
 // Activity based decision:
 while (next == var_Undef || value(next) != l_Undef || !decision[next])
 if (order_heap.empty()){
 next = var_Undef;
 break;
 }else next = order_heap.removeMin();
 // Choose polarity based on different polarity modes (global or per-variable):
 if (next == var_Undef) return lit_Undef;
 else if (user_pol[next] != l_Undef) return mkLit(next, user_pol[next] == l_True);
 else if (rnd_pol) return mkLit(next, drand(random_seed) < 0.5);
 else return mkLit(next, polarity[next]);
}

我的初步设计思路：

C++函数修改：

Lit Solver::pickBranchLit() {
 // 等待Python返回待赋值的(variable, value)
 // 更新order_heap
 // 返回mkLit(variable, value)
}

Python函数逻辑：

CNF = get_cnf(filename)
c_solver.solve(filename) # 加载CNF到C++中
while True:
 # Python函数决定待赋值的变量和值
 variable, value = python_decide_variable(CNF)
 # 调用C++的pickBranchLit
 result, new_variables, values = python_sat_solver.assign_value(variable, value)
 if result == "SATISFIABLE":
 break

回答

首先得说，你的初步设计方向是对的，但交互主动权搞反了——MiniSAT的solve()是一个完整的求解流程，会自动循环调用pickBranchLit()来选择分支、处理冲突、回溯，而你的设计是让Python主动发起赋值请求，这会打乱Solver内部的状态管理（比如order_heap的维护、冲突子句的处理等），很容易出bug。下面是调整后的合理方案：

1. 选择合适的C++/Python交互工具

推荐用pybind11（现代、简洁，对C新手友好），它能快速把C类和函数绑定成Python可调用的模块，避免直接写繁琐的Python C API。

2. 给Solver类添加Python接口，让Python能获取状态

首先在Solver.h里添加成员函数，暴露变量状态给Python：

// 获取所有未赋值且可决策的变量
std::vector<Var> getUnassignedVars() const;
// 获取变量的activity值（原启发式的核心依据）
double getVarActivity(Var v) const;
// 获取变量当前的赋值状态（l_Undef/l_True/l_False）
lbool getVarValue(Var v) const;

然后在Solver.cc里实现这些函数，比如：

std::vector<Var> Solver::getUnassignedVars() const {
    std::vector<Var> res;
    for (Var v = 0; v < nVars(); v++) {
        if (value(v) == l_Undef && decision[v]) {
            res.push_back(v);
        }
    }
    return res;
}

double Solver::getVarActivity(Var v) const {
    return activity[v];
}

lbool Solver::getVarValue(Var v) const {
    return value(v);
}

3. 修改`pickBranchLit()`，让它回调Python启发式

在Solver.h里添加一个成员变量，用来保存Python的回调函数（用pybind11的类型），再加一个setter：

#include <pybind11/pybind11.h>
namespace py = pybind11;

class Solver {
    // ... 原有成员 ...
    py::function py_branch_heuristic;
public:
    // ... 原有函数 ...
    void setBranchHeuristic(py::func f) { py_branch_heuristic = f; }
};

然后修改pickBranchLit()，优先调用Python启发式，不合法时fallback到原逻辑：

Lit Solver::pickBranchLit() {
    // 如果设置了Python启发式，优先调用
    if (py_branch_heuristic) {
        try {
            // 调用Python函数，返回(Var, polarity)
            py::tuple result = py_branch_heuristic();
            Var next = py::cast<Var>(result[0]);
            bool polarity = py::cast<bool>(result[1]);
            
            // 验证变量合法性：未赋值、可决策
            if (next != var_Undef && next < nVars() && value(next) == l_Undef && decision[next]) {
                return mkLit(next, polarity);
            }
        } catch (const py::error_already_set& e) {
            // 捕获Python异常，避免Solver崩溃
            std::cerr << "Python heuristic error: " << e.what() << std::endl;
        }
    }

    // 原有的随机+activity分支逻辑，作为fallback
    Var next = var_Undef;
    // Random decision:
    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
        next = order_heap[irand(random_seed,order_heap.size())];
        if (value(next) == l_Undef && decision[next]) rnd_decisions++;
    }
    // Activity based decision:
    while (next == var_Undef || value(next) != l_Undef || !decision[next])
        if (order_heap.empty()){
            next = var_Undef;
            break;
        }else next = order_heap.removeMin();
    // Choose polarity based on different polarity modes (global or per-variable):
    if (next == var_Undef) return lit_Undef;
    else if (user_pol[next] != l_Undef) return mkLit(next, user_pol[next] == l_True);
    else if (rnd_pol) return mkLit(next, drand(random_seed) < 0.5);
    else return mkLit(next, polarity[next]);
}

4. 用pybind11写绑定代码，暴露Solver给Python

创建一个minisat_bindings.cpp文件：

#include <pybind11/pybind11.h>
#include "Solver.h"

namespace py = pybind11;

PYBIND11_MODULE(minisat_py, m) {
    m.doc() = "MiniSAT Python bindings with custom branch heuristic support";

    // 绑定Solver类
    py::class_<Solver>(m, "Solver")
        .def(py::init<>())
        .def("add_clause", &Solver::addClause, "Add a clause to the solver")
        .def("solve", &Solver::solve, "Run the SAT solver")
        .def("set_branch_heuristic", &Solver::setBranchHeuristic, "Set custom Python branch heuristic")
        .def("get_unassigned_vars", &Solver::getUnassignedVars, "Get list of unassigned decision variables")
        .def("get_var_activity", &Solver::getVarActivity, "Get activity value of a variable")
        .def("get_var_value", &Solver::getVarValue, "Get current value of a variable")
        .def("n_vars", &Solver::nVars, "Get number of variables");

    // 绑定枚举类型
    py::enum_<lbool>(m, "lbool")
        .value("l_Undef", l_Undef)
        .value("l_True", l_True)
        .value("l_False", l_False)
        .export_values();

    // 绑定Var类型（MiniSAT的Var是unsigned int）
    py::class_<Var>(m, "Var")
        .def(py::init<unsigned int>())
        .def_readonly("var_Undef", var_Undef);
}

然后用setup.py编译这个模块（需要安装pybind11）：

from setuptools import setup, Extension
import pybind11

ext_modules = [
    Extension(
        "minisat_py",
        ["minisat_bindings.cpp", "core/Solver.cc"], # 加上MiniSAT的源文件
        include_dirs=[pybind11.get_include(), "."],
        language="c++",
        extra_compile_args=["-O3"],
    ),
]

setup(
    name="minisat_py",
    ext_modules=ext_modules,
)

5. Python端的使用代码

现在Python可以正常调用Solver，并且传入自定义启发式：

import minisat_py

def custom_branch_heuristic(solver):
    # 获取当前未赋值变量
    unassigned = solver.get_unassigned_vars()
    if not unassigned:
        return (minisat_py.Var(minisat_py.var_Undef), False)
    
    # 示例：选择activity最高的变量，极性取True
    var_activity = {v: solver.get_var_activity(v) for v in unassigned}
    best_var = max(var_activity, key=var_activity.get)
    return (best_var, True)

def load_cnf(solver, filename):
    # 实现从CNF文件读取子句，调用solver.add_clause添加
    # 示例逻辑（简化版）：
    with open(filename, "r") as f:
        for line in f:
            line = line.strip()
            if not line or line.startswith("c") or line.startswith("p"):
                continue
            literals = list(map(int, line.split()))[:-1] # 忽略末尾的0
            solver.add_clause([minisat_py.mkLit(abs(lit)-1, lit < 0) for lit in literals])

def main():
    solver = minisat_py.Solver()
    load_cnf(solver, "test.cnf")
    
    # 设置自定义启发式（用lambda把solver传给回调函数）
    solver.set_branch_heuristic(lambda: custom_branch_heuristic(solver))
    
    # 启动求解
    is_sat = solver.solve()
    if is_sat:
        print("SATISFIABLE")
        # 获取赋值结果
        for v in range(solver.n_vars()):
            val = solver.get_var_value(v)
            print(f"Var {v}: {val}")
    else:
        print("UNSATISFIABLE")

if __name__ == "__main__":
    main()

关键调整点说明

交互模式修正：让C++在需要分支时主动回调Python，而不是Python主动推赋值，这样完全贴合MiniSAT的原有求解流程，不会破坏内部状态。
保留fallback逻辑：如果Python启发式返回非法结果或抛出异常，Solver会自动用原有的分支逻辑，保证求解的稳定性。
状态暴露：给Python提供获取Solver内部状态的接口，让你的启发式能基于当前变量的真实状态做决策，而不是只靠初始CNF。

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