#constraints #cardinality #sat #api-bindings #pb

sys pblib-rs

Rust 对 pblib 的安全绑定

1 个不稳定版本

0.1.0 2023年12月4日

#1715 in 编码

LGPL-3.0-or-later

5.5MB
8K SLoC

C++ 7.5K SLoC // 0.1% comments Rust 488 SLoC Shell 19 SLoC

pblib-rs

Rust 对 pblib 的安全绑定。

pblib 的源代码来自 Radomír Černoch 在 Github 上维护的分支 [链接]。该包目前提供了对初始库函数的部分绑定。如果需要有关编码的更多信息,请参阅原始文档(可以从分支的 README 页面检索)。

API 的入口点是 PB2CNF 结构。如果您想使用 pblib-rs,请首先查看其文档。

TL;DR

基数约束

use pblib_rs::PB2CNF;

// we encode x1 + x2 + x3 >= 2
let literals = vec![1, 2, 3];
let pb2cnf = PB2CNF::new();
// the threshold is 2 and the first variable not in use is 4
let encoding = pb2cnf.encode_at_least_k(literals, 2, 4);
println!("the encoding uses {} variables", encoding.next_free_var_id() - 4);
println!("the encoding uses {} clauses", encoding.clauses().len());
encoding.clauses().iter().enumerate().for_each(|(i,c)| println!("clause {i} is {:?}", c));

伪布尔约束

use pblib_rs::PB2CNF;

// we encode 8*x1 + 4*x2 + 2*x3 + 1*x4 >= 6
let weights = vec![8, 4, 2, 1];
let literals = vec![1, 2, 3, 4];
let pb2cnf = PB2CNF::new();
// the threshold is 6 and the first variable not in use is 5
let encoding = pb2cnf.encode_geq(weights.clone(), literals, 6, 5);
println!("the encoding uses {} variables", encoding.next_free_var_id() - 4);
println!("the encoding uses {} clauses", encoding.clauses().len());
encoding.clauses().iter().enumerate().for_each(|(i,c)| println!("clause {i} is {:?}", c));

许可证

pblib-rs 在 CRIL(阿图瓦大学 & CNRS)开发。它根据 GNU Lesser GPLv3 许可证的条款提供。

依赖项