Rust中的SAT求解器

此crate包含布尔可满足性问题（SAT）的各种可满足性求解器的实现。

可用求解器列表

• crate::solvers::syntactic - 基于用户提供的解释的纯语法求解器

此crate还包含一些用于处理命题变量和公式的有用结构体，例如

• crate::notation::Formula - 用于处理命题公式的结构体
• crate::notation::Clause - 用于处理命题子句的结构体
• crate::notation::Literal - 用于处理命题文字（原子）的结构体

用法

可以将crate用作库或二进制文件。要将其用作二进制文件，请运行以下命令

cargo run <CNF_FILE> <SOLVER>

或者

sat-rs <CNF_FILE> <SOLVER>