varisat-formula：高效的布尔公式解析与SAT求解器插件库

简介

varisat-formula是一个专门用于解析和处理布尔公式的Rust库，作为varisat SAT求解器生态系统的重要组成部分。该库提供了高效的布尔公式表示和操作功能，支持CNF（合取范式）和其他形式的布尔表达式处理。

主要特性

• 高效的布尔公式内存表示
• 支持多种公式输入格式
• 与varisat求解器无缝集成
• 提供公式操作和转换功能
• 支持增量求解和公式修改

安装方法

在Cargo.toml中添加依赖：

[dependencies]
varisat-formula = "0.2"

基本使用方法

1. 创建布尔公式

use varisat_formula::{Lit, CnfFormula};

fn main() {
    let mut formula = CnfFormula::new();
    
    // 创建文字
    let x = Lit::from_dimacs(1);  // 正文字
    let not_x = Lit::from_dimacs(-1); // 负文字
    
    // 添加子句 (x ∨ ¬y ∨ z)
    formula.add_clause(&[x, Lit::from_dimacs(-2), Lit::from_dimacs(3)]);
}

2. 解析DIMACS格式

use varisat_formula::CnfFormula;

fn parse_dimacs() -> Result<CnfFormula, varisat_formula::ParseError> {
    let dimacs_input = "p cnf 3 2\n1 -2 0\n2 -3 0\n";
    CnfFormula::from_dimacs(dimacs_input)
}

3. 公式操作示例

use varisat_formula::{CnfFormula, Lit, ExtendFormula};

fn formula_operations() {
    let mut formula = CnfFormula::new();
    
    // 添加多个子句
    formula.add_clause(&[Lit::from_dimacs(1), Lit::from_dimacs(2)]);
    formula.add_clause(&[Lit::from_dimacs(-1), Lit::from_dimacs(3)]);
    
    // 获取公式信息
    println!("变量数量: {}", formula.var_count());
    println!("子句数量: {}", formula.len());
    
    // 迭代所有子句
    for clause in formula.iter() {
        println!("子句: {:?}", clause);
    }
}

4. 与varisat求解器集成

use varisat::{Solver, CnfFormula};
use varisat_formula::Lit;

fn solve_with_varisat() {
    let mut formula = CnfFormula::new();
    formula.add_clause(&[Lit::from_dimacs(1), Lit::from_dimacs(2)]);
    formula.add_clause(&[Lit::from_dimacs(-1), Lit::from_dimacs(2)]);
    formula.add_clause(&[Lit::from_dimacs(-2)]);
    
    let mut solver = Solver::new();
    solver.add_formula(&formula);
    
    match solver.solve() {
        Ok(result) => println!("可满足性: {}", result),
        Err(e) => println!("求解错误: {}", e),
    }
}

高级功能

公式转换

use varisat_formula::{CnfFormula, Lit, ExtendFormula};

fn tseitin_transformation() {
    let mut formula = CnfFormula::new();
    
    // 使用Tseitin变换添加等价关系
    // 实现 (a ∧ b) ≡ c
    let a = Lit::from_dimacs(1);
    let b = Lit::from_dimacs(2);
    let c = Lit::from_dimacs(3);
    
    // (¬a ∨ ¬b ∨ c) ∧ (a ∨ ¬c) ∧ (b ∨ ¬c)
    formula.add_clause(&[!a, !b, c]);
    formula.add_clause(&[a, !c]);
    formula.add_clause(&[b, !c]);
}

增量公式构建

use varisat_formula::{CnfFormula, Lit, ExtendFormula};

fn incremental_building() {
    let mut formula = CnfFormula::new();
    
    // 批量添加子句
    let clauses = vec![
        vec![Lit::from_dimacs(1), Lit::from_dimacs(2)],
        vec![Lit::from_dimacs(-1), Lit::from_dimacs(3)],
        vec![Lit::from_dimacs(-2), Lit::from_dimacs(-3)],
    ];
    
    for clause in clauses {
        formula.add_clause(&clause);
    }
}

性能提示

• 使用with_capacity预分配内存以提高性能
• 批量操作比单个操作更高效
• 复用公式对象避免不必要的内存分配

错误处理

库提供了详细的错误类型，包括解析错误和公式操作错误，建议在生产环境中适当处理这些错误。

这个库为Rust开发者提供了强大的布尔公式处理能力，特别适合需要集成SAT求解功能的应用程序。

完整示例demo

use varisat_formula::{CnfFormula, Lit, ExtendFormula};
use varisat::{Solver, CnfFormula as VarisatCnfFormula};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    // 示例1: 创建布尔公式
    println!("=== 创建布尔公式示例 ===");
    let mut formula = CnfFormula::new();
    
    // 创建文字
    let x = Lit::from_dimacs(1);        // 正文字 x
    let not_y = Lit::from_dimacs(-2);   // 负文字 ¬y
    let z = Lit::from_dimacs(3);        // 正文字 z
    
    // 添加子句 (x ∨ ¬y ∨ z)
    formula.add_clause(&[x, not_y, z]);
    println!("已添加子句: (x ∨ ¬y ∨ z)");

    // 示例2: 解析DIMACS格式
    println!("\n=== 解析DIMACS格式示例 ===");
    let dimacs_input = "p cnf 3 2\n1 -2 0\n2 -3 0\n";
    match CnfFormula::from_dimacs(dimacs_input) {
        Ok(parsed_formula) => {
            println!("成功解析DIMACS格式");
            println!("解析后的变量数量: {}", parsed_formula.var_count());
            println!("解析后的子句数量: {}", parsed_formula.len());
        }
        Err(e) => println!("解析错误: {}", e),
    }

    // 示例3: 公式操作
    println!("\n=== 公式操作示例 ===");
    let mut formula_ops = CnfFormula::new();
    
    // 添加多个子句
    formula_ops.add_clause(&[Lit::from_dimacs(1), Lit::from_dimacs(2)]);
    formula_ops.add_clause(&[Lit::from_dimacs(-1), Lit::from_dimacs(3)]);
    
    // 获取公式信息
    println!("变量数量: {}", formula_ops.var_count());
    println!("子句数量: {}", formula_ops.len());
    
    // 迭代所有子句
    for (i, clause) in formula_ops.iter().enumerate() {
        println!("子句 {}: {:?}", i + 1, clause);
    }

    // 示例4: 与varisat求解器集成
    println!("\n=== 与varisat求解器集成示例 ===");
    let mut solver_formula = CnfFormula::new();
    solver_formula.add_clause(&[Lit::from_dimacs(1), Lit::from_dimacs(2)]);
    solver_formula.add_clause(&[Lit::from_dimacs(-1), Lit::from_dimacs(2)]);
    solver_formula.add_clause(&[Lit::from_dimacs(-2)]);
    
    let mut solver = Solver::new();
    solver.add_formula(&solver_formula);
    
    match solver.solve() {
        Ok(result) => println!("可满足性: {}", result),
        Err(e) => println!("求解错误: {}", e),
    }

    // 示例5: Tseitin变换
    println!("\n=== Tseitin变换示例 ===");
    let mut tseitin_formula = CnfFormula::new();
    
    // 实现 (a ∧ b) ≡ c
    let a = Lit::from_dimacs(1);
    let b = Lit::from_dimacs(2);
    let c = Lit::from_dimacs(3);
    
    // (¬a ∨ ¬b ∨ c) ∧ (a ∨ ¬c) ∧ (b ∨ ¬c)
    tseitin_formula.add_clause(&[!a, !b, c]);
    tseitin_formula.add_clause(&[a, !c]);
    tseitin_formula.add_clause(&[b, !c]);
    
    println!("Tseitin变换完成，添加了3个子句");

    // 示例6: 增量公式构建
    println!("\n=== 增量公式构建示例 ===");
    let mut incremental_formula = CnfFormula::new();
    
    // 批量添加子句
    let clauses = vec![
        vec![Lit::from_dimacs(1), Lit::from_dimacs(2)],
        vec![Lit::from_dimacs(-1), Lit::from_dimacs(3)],
        vec![Lit::from_dimacs(-2), Lit::from_dimacs(-3)],
    ];
    
    for clause in clauses {
        incremental_formula.add_clause(&clause);
    }
    
    println!("增量构建完成，总子句数: {}", incremental_formula.len());

    Ok(())
}

这个完整示例演示了varisat-formula库的主要功能，包括布尔公式的创建、DIMACS格式解析、公式操作、与SAT求解器的集成、Tseitin变换以及增量公式构建。每个功能模块都有清晰的注释说明，方便理解和使用。