BCSAT

描述

BCSAT 是一种布尔电路的语言。它支持标准的命题门（与、或、非）、n-元门和一系列专用门：if-then-else、偶数/奇数和阈值门。

计划中的功能

以下功能已被考虑但尚未实现。如果需要，我将实现它们，或者如果我在自己的项目中需要它们。

• 更多简化

  • 将蕴涵链简化为合取和一个单一的蕴涵或一个单一的析取。

    a=> (b=> (c=>d)) === (a&b&c) =>d=== ~a| ~b| ~c|d

• 等效/等价变异：由于基准测试数量较少，SAT 求解器受到批评，过度拟合 SAT-race 的启发式方法。这可以通过人工增加基准测试集来对抗。将基准测试随机化以击败这些求解器所做的预处理可能有助于解决这个问题。这可能会是一个不同的 crate。

• 简化到 cnf：已存在一个工具，除了可能需要集成外，没有必要重写。

许可证

双许可以与 Rust 项目兼容。

根据您的选择，许可协议为 Apache 许可证第 2.0 版 https://apache.ac.cn/licenses/LICENSE2.0 或 MIT 许可证 http://opensource.org/licenses/MIT。本项目不得根据这些条款之外的方式进行复制、修改或分发。