#sat-solver #sat #solver #backtracking #combinatorial #search

已删除 backtrack-rs

带示例的回溯求解器

0.1.0 2021年2月27日

#11#backtracking

MIT/Apache

22KB
304

backtrack-rs 🦀

Documentation crates.io CI License

backtrack-rs 允许您简洁地定义和解决回溯问题。

问题通过其 范围 和对可能解决方案的 检查 来定义。The Scope 确定可能解决方案的长度和允许的值。The CheckCheckInc trait 确定某个值组合是否令人满意。

用法

如果完整解决方案也应该满足,则部分解决方案(即比范围更短的解决方案)必须满足。 Solvers 在搜索 候选解决方案 的过程中借用问题。

检查

我们使用有限数字集定义倒计时问题,并迭代解决。

use backtrack_rs::problem::{Check, Scope};
use backtrack_rs::solvers::IterSolveNaive;
// helper trait to filter solutions of interest
use backtrack_rs::solve::IterSolveExt;

/// Obtain permutations of some 3 descending numbers
struct CountDown {}

impl Scope for CountDown {
    fn size(&self) -> usize { 3 }
    fn domain(&self) -> Vec<usize> { (0..=3).collect() }
}

impl Check for CountDown{
    fn extends_sat(&self, solution: &[usize], x_l: usize) -> bool {
        solution.last().map_or(true, |last| *last > x_l)
    }
}

let solver = IterSolveNaive::new(&CountDown{});
let mut sats = solver.sat_iter();

assert_eq!(sats.next(), Some(vec![2, 1, 0]));
assert_eq!(sats.next(), Some(vec![3, 1, 0]));
assert_eq!(sats.next(), Some(vec![3, 2, 0]));
assert_eq!(sats.next(), Some(vec![3, 2, 1]));
assert_eq!(sats.next(), None);

增量检查

如果您的检查可以用简化解决方案表示,请实现 CheckInc

可以通过“计算”每步的最后项目来表示与上述相同的结果。如果任何给定 sat 检查需要对多个先前值执行实际工作,则此方法更有意义。

use backtrack_rs::problem::{CheckInc, Scope};
// ...
impl CheckInc for CountDown{
    type Accumulator = usize;

    fn fold_acc(&self, accu: Option<Self::Accumulator>, x: &usize) -> Self::Accumulator {
        // only last value is of interest for checking
        *x
    }

    fn accu_sat(&self, accu: Option<&Self::Accumulator>, x: &usize, index: usize) -> bool {
       accu.map_or(true, |last| last > x)
    }
}
// since `CheckInc` impls `Check`, the same solver as in example above can be used
// todo: specialize solver to actually realize performance advantage
// ...

示例

请查看 examples 文件夹中的示例问题。

# 4-queens solution
cargo run --example n_queens 4 | grep Sat
## n_queens.rs: NQueens { n: 4 }
## Sat([1, 3, 0, 2])
## Sat([2, 0, 3, 1])
# sequence of numbers which sum up to a minimum value but not more
cargo run --example total_sum | grep Sat

基准测试

backtrack-rs 使用 criterion 进行基准测试。

cargo benches

待办事项

  • CheckInc 求解器
  • 通用 domain
  • 并行化搜索

无运行时依赖项