布尔公式的创建、操作和求解的库

这是一个预览版本！API可能还会发生重大变化！程序尚未完全测试，请勿在生产环境中使用！

简介

这是为Rust编写的LogicNG。LogicNG的原始版本是一个用于创建、操作和求解布尔和伪布尔公式的Java库。

其主要重点是布尔公式的内存高效数据结构和操作、求解它们的高效算法。该库设计和最值得注意的是，它被用于工业系统，这些系统每天需要操作和解决数百万个公式。LogicNG的Java版本在德国汽车行业中被广泛使用，以验证和优化其产品文档，支持车辆配置过程，并计算排放和消耗的WLTP值。

实现的算法

LogicNG的Rust版本目前提供以下关键功能

• 布尔公式、基数约束和伪布尔公式的支持
• 线程安全的公式工厂（与Java版本不同）
• 从字符串或文件解析布尔公式
• 公式的转换，如
  • 使用各种可配置算法的正常形式NNF、DNF或CNF
  • 公式的匿名化
  • 通过子集或骨架简化公式
• 使用大多数不同算法将基数约束和伪布尔公式编码为纯布尔公式
• 使用集成SAT求解器求解公式，包括
  • 求解器上的快速骨架计算
  • 增量/减量求解器接口
  • 证明生成
  • 使用增量基数约束进行优化
• 使用MaxSAT求解器优化公式（集成 Open-WBO），通过功能 open_wbo 激活
• 使用BDD或DNNF进行知识编译

哲学

图书馆最重要的哲学是避免不必要的对象创建。因此，公式只能通过公式工厂生成。公式工厂确保公式在内存中只创建一次。如果用户创建了相同公式的另一个实例，工厂将返回已存在的实例。这导致内存占用小且算法执行速度快。公式可以缓存在其上执行的算法的结果，并且由于每个公式在内存中只保留一次，因此可以保证相同的公式上的相同算法也只执行一次。

白皮书

如果您想了解LogicNG的概述以及它在产品配置领域的许多应用，您可以阅读我们的白皮书。

第一步

以下代码以编程方式创建了布尔公式 A and not (B or not C)。

use logicng::formulas::FormulaFactory;

let f = FormulaFactory::new();
let a = f.variable("A");
let b = f.variable("B");
let not_c = f.literal("C", false);
let formula = f.and(&[a, f.not(f.or(&[b, not_c]))]);

或者您可以直接从字符串解析公式

use logicng::formulas::FormulaFactory;

let f = FormulaFactory::new();
let formula = f.parse("A & ~(B | ~C)").expect("Parsing failed");

甚至更短

use logicng::formulas::{FormulaFactory, ToFormula};

let f = FormulaFactory::new();
let formula = "A & ~(B | ~C)".to_formula(&f);

一旦创建公式，例如，您可以将其转换为NNF或CNF，或者使用MiniSat的实例求解它

use logicng::formulas::{FormulaFactory, ToFormula};
use logicng::solver::minisat::MiniSat;

let f = FormulaFactory::new();
let formula = "A & ~(B | ~C)".to_formula(&f);

let nnf = f.nnf_of(formula);
let cnf = f.cnf_of(formula);
let mut miniSat = MiniSat::new();
let result = miniSat.sat();

功能

资金

LogicNG用于Rust开发由SofDCar项目资助