问题标签 [picosat]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
python - Picosat SAT求解器：设置传播限制——但是什么值？
从 API：
我查看了文档，但找不到任何详细信息。我应该选择什么值？有比随机测试更好的猜测吗？后者可能需要几天时间，因为我的执行时间一次运行长达 24 小时。
我实际上使用“pycosat”为picosat 的python 绑定。
PS：有人可以添加“picosat”标签吗？
haskell - Haskell：绑定到快速简单的 SAT 求解器
今天我也想研究一下在 haskell 中解决 SAT 的选项。首先，我想为 picosat 求解器编写自己的界面。
然后我发现那里有SBV 库。它是 Z3、Yices、CVC4 和 Boolector 的接口。
此外，我在 github 上进行了谷歌搜索，结果发现甚至有可用的Picosat 绑定。
考虑到快速/高性能的限制，是否有任何其他与 SAT 求解器相关的 Haskell 绑定值得关注。Carification：适用于高性能 SAT 解决（例如，运行数天的问题，以及需要尽快完成的问题，因为我检查了 2^20 或更多 SAT 问题）。例如，我在 hackage 中特别缺少的是与 Plingeling 等快速并行 SAT 求解器的绑定。（另外，我偶然发现了 github 上当前更新的 picosat 绑定，我很可能会错过其他选项）
SBV 库的默认选项是 Z3 SMT 求解器。我的有根据的猜测是否正确，即 picosat 比 Z3 更快地解决普通 SAT 问题？