Rust中push方法的困惑行为及递归调用实现疑问

问题背景 #

定义了如下Rust类型：

pub type Variable = char;

#[derive(Clone,Debug,PartialEq,Eq)]
pub enum Atom {
    Base(Variable),
    Not(Variable)
}

pub type Clause = Vec<Atom>;

pub type Formula = Vec<Clause>;

编写DPLL函数时遇到两个问题：

1. 初始版本中，formulaClone.push(...)的返回值类型是()，困惑于为什么push操作没有返回&mut Formula：

pub fn dpll(f:& mut Formula) -> bool {
    let mut formulaClone = f.clone();
    let v = 'a';
    let finalVect = formulaClone.push(vec![Atom::Base(v)]);
   
}

2. 想要实现递归逻辑：基于添加新Clause后的Formula递归调用dpll，但当前写法无法通过编译：

pub fn dpll(f:& mut Formula) -> bool {
    let mut formulaClone = f.clone();
    let v = 'a';
    let finalVect = formulaClone.push(vec![Atom::Base(v)]);
    let finalVect2 = formulaClone.push(vec![Atom::Not(v)]);
    return dpll(finalVect) || dpll(finalVect2);
}

问题解答 #

1. push返回()的原因 #

Rust中Vec::push的设计是原地修改向量，它接收&mut self作为参数，直接在原向量的内存空间追加元素，不需要返回新的引用或向量。返回单元类型()是因为调用者已经持有该向量的可变引用，操作完成后可直接使用原变量，这种设计避免了所有权和引用的冗余，符合Rust的内存安全原则。

2. 正确实现递归DPLL的方式 #

要实现递归分支，需为每个分支创建独立的公式副本，分别添加对应的子句后，传递可变引用给递归调用。注意不能在同一个副本上连续push两个子句，否则两个递归分支会共享同一个修改后的公式，不符合DPLL的分支逻辑。

修正后的代码框架如下：

pub fn dpll(f: &mut Formula) -> bool {
    // 补充DPLL递归终止条件：
    // 1. 公式为空，说明所有子句都被满足，返回true
    if f.is_empty() {
        return true;
    }
    // 2. 存在空子句，说明当前分支不可满足，返回false
    if f.iter().any(|clause| clause.is_empty()) {
        return false;
    }

    // 选择变量v（实际实现中需要从公式中提取，这里用'a'作为示例）
    let v = 'a';

    // 分支1：添加v的正文字句并递归
    let mut formula_with_base = f.clone();
    formula_with_base.push(vec![Atom::Base(v)]);
    if dpll(&mut formula_with_base) {
        return true;
    }

    // 分支2：添加v的负文字句并递归
    let mut formula_with_not = f.clone();
    formula_with_not.push(vec![Atom::Not(v)]);
    dpll(&mut formula_with_not)
}

说明：

• 每个递归分支使用独立的公式副本，避免分支间的状态干扰
• 递归调用时传递副本的可变引用&mut formula_with_base和&mut formula_with_not，符合函数参数要求
• 示例仅实现了最基础的分支逻辑，实际DPLL算法还需补充变量选择策略、单元传播、纯文字消除等核心步骤，才能正确工作

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