我曾经回答了一个我认为很有趣的问题，链接是：可以使用SAT/SMT求解器找到所有解吗？但不幸的是，在我发表之前，该问题被作者删除了。如果对其他人有用的话，我会在这里重新发布问题及我的答案摘要。 假设我有一个SAT求解器，它可以对合取范式中的布尔公式进行求解，并返回满足公式的变量赋值或无解的信...

我想解析一个描述命题公式的String，然后使用SAT求解器找到该命题公式的所有模型。 现在我可以使用hatt包解析命题公式；请参见下面的testParse函数。 我也可以使用SBV库运行SAT求解器调用；请参见下面的testParse函数。 问题: 在运行时如何生成一个值为Predic...

一个好奇的问题。还记得那些在课堂小组作业时，教授会将人们分成固定数量(n)的小组吗？ 我的一些教授会从每个学生那里获取一个希望合作的n人名单和一个不想与之合作的n人名单，然后神奇地组成n人的小组，让学生与他们喜欢的人匹配，并避免与他们不喜欢的人一起工作。 对我来说，这个算法听起来很像一个背...

我知道布尔可满足性问题是NP完全的，但是对于布尔表达式的化简和简化，我的意思是将给定的符号形式的表达式转换为等效但简化的符号形式的表达式，是否也是NP完全的呢？我不确定是否有从可满足性到最小化的归约，但我感觉可能存在。是否有人可以确认一下呢？

SMT求解器可以用于约束求解。众所周知，CSP求解器也已经用于约束求解多年了。那么，SMT求解器相比CSP求解器有什么优势呢？