Satoxid，一个SAT可满足性问题编码库

Satoxid是一个专注于易用性和可调试性的库，用于帮助编码SAT问题。

功能

• 预定义的常见约束
• 变量是用户定义类型的值，而不是整数
• 模块化，您可以实现自己的约束和后端

示例

use satoxid::{CadicalEncoder, constraints::ExactlyK};

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
enum Var {
    A, B, C
}

use Var::*;

fn main() {
    let mut encoder = CadicalEncoder::new();

    let constraint = ExactlyK {
        k: 1,
        lits: [A, B, C].iter().copied()
    };

    encoder.add_constraint(constraint);

    if let Some(model) = encoder.solve() {

        let true_vars = model.vars()
                             .filter(|v| v.is_pos())
                             .count();

        assert_eq!(true_vars, 1);
    }
}

更多复杂示例请参见这个 Rummysolver。

lib.rs:

Satoxid，一个SAT可满足性问题编码库

Satoxid是一个专注于易用性和可调试性的库，用于帮助编码SAT问题。

示例

use satoxid::{CadicalEncoder, constraints::ExactlyK};

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
enum Var {
    A, B, C
}

use Var::*;

fn main() {
    let mut encoder = CadicalEncoder::new();

    let constraint = ExactlyK {
        k: 1,
        lits: [A, B, C].iter().copied()
    };

    encoder.add_constraint(constraint);

    if let Some(model) = encoder.solve() {

        let true_lits = model.vars()
                             .filter(|v| v.is_pos())
                             .count();

        assert_eq!(true_lits, 1);
    }
}

概念

变量

SAT求解器通常使用有符号整数来表示文字。根据符号，文字是正的或负的，绝对值定义了SAT变量。

虽然这是一个SAT求解器的简单API，但用户编码此类问题可能不方便。因此，当使用Satoxid时，我们不直接使用整数，而是定义自己的变量类型，其中该类型的每个值都是一个SAT变量。

例如，假设我们想要编码著名的数独游戏（请参见示例以获得完整实现）。我们有一个9x9网格，其中每个方格都有一个x-y坐标和一个值。我们可以将其表示如下：

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
struct Tile {
    x: u32,
    y: u32,
    value: u32,
}

Tile的值表示在位置( x, y)的方格具有value中的数字。

要使类型可用于作为SAT变量，它需要实现SatVar，这只需要 traits Debug、Copy、Eq和Hash。

现在我们可以使用Tile在约束中使用，但本身它只表示一个正文字。如果我们想要使用负文字，我们需要将其包装在Lit中，它是一个枚举，清楚地定义了正或负文字。

最后还有一种第三种类型 VarType，它可以作为字面量使用。当使用像 add_constraint_implies_repr 这样的函数时，Satoxid 会生成新的变量，这些变量与用户定义的 SAT 变量（如 Tile）没有关系。 VarType 允许用户使用这样的 未命名 变量。

Satoxid 内部使用 VarMap 类型将用户定义的 SAT 变量转换为求解器使用的整数 SAT 变量。

一种常见的模式是使用一个枚举，列出问题中所有可能的变量类型。然后，这个枚举被用作主要变量类型。

约束条件

Satoxid 在 constraints 模块中提供了一套预定义的约束条件。约束条件是一种可以转换为有限数量的 SAT 子句的类型。这通过 Constraint 特性来表示。

例如，如果我们想要约束我们的 Tile 类型，使得每个坐标只能有一个值，我们会使用 ExactlyK 约束条件。

use satoxid::constraints::ExactlyK;
#

let constraint = ExactlyK {
    k: 1,
    lits: (1..=9).map(|value| Tile { x, y, value })
};
encoder.add_constraint(constraint);

对于大多数简单问题，提供的约束条件应该足够，但如果有必要，用户可以创建自己的约束条件，通过实现此特性。

有时，需要以非平凡的方式组合多个不同的约束条件。（例如，我们希望至少满足四个不同的约束条件。）为此，ConstraintRepr 特性允许将约束条件编码到一个新的变量中，然后可以在其他约束条件中使用该变量。

编码器和求解器

Encoder 是用户交互的主要类型。它接收要编码的约束条件，并处理将所有 SAT 变量映射到相应的整数 SAT 变量。此外，它还有一个 debug 标志，该标志启用/禁用后端（在某个地方打印编码的约束条件）的调试功能。

约束条件生成的子句被提供给实现 Backend 的类型。这样的后端可能是一个能够解决编码问题的求解器，或者可能只是将子句打印到某个地方以供外部使用，如 DimacsWriter。

如果后端能够解决它，它将实现 Solver 特性，并允许用户在编码器上调用 solve。默认情况下，Satoxid 提供了 CaDiCaL SAT 求解器作为后端，该后端可以使用 CadicalEncoder 类型定义。可以使用 cadical 功能禁用此依赖项。