讽刺

讽刺是一个教育用（即，不是功能齐全）的 SAT 求解器，它可能在未来发展成为其他东西（也可能不会）。

我主要为了通过编写一个 SAT 求解器来学习 SAT 求解器的内部结构而编写讽刺。然而，我也努力将 SAT 求解器的不同概念在不同的模块中分离出来，因此它可能对发现现有 SAT 求解器代码难以阅读或正在学习如何组织 Rust 代码的人来说有帮助。

如何使用

讽刺接受有限的 DIMAC CNF 文件格式。

satire [dpll|cdcl] check testcases/satch_cnfs/add4.cnf

要运行整个测试套件，请使用 cargo test。

# Run all tests (note: it doesn't pass all tests in time)
cargo test --release

# Run all tests only with cdcl solver (note: it doesn't pass all tests in time)
cargo test --release -- cdcl

已知限制

• DPLL 求解器使用递归，这无必要地造成了函数调用开销。
• CDCL 求解器使用 O(1) 数据结构进行文字标记，但由于常数开销，它通常比线性搜索慢。
• 用于 VSIDS 计分方案的二叉堆相当低效。可以通过自定义二叉堆实现来修复。
• 没有子句最小化。
• 没有重启。

参考文献

• SATCH
• MiniSat
• splr