algorithm - SAT 求解器确定多元函数的特征？

Question

Boolean Satisfiabiity problem是检查 bool 表达式的可满足性的概括。现在 bool 表达式是由多项式的非负性算法生成的。例如，多项式可以是 和 有一些间隔，例如 其中 是变量的数量。我目前使用特殊算法(例如分支定界算法)检查多项式的特征(例如非负性)，在这种算法中，我将大问题变成较小的问题，但缺少某些 SAT 求解器 promise 的学习特征，例如 MiniSat .所以

1. Some SAT solvers designed to check properties of polynomials such as multilinear functions or general multivariate functions?

2. Any easy way to convert a multivariate function and the non-negativity algorithm into a boolean expression?

Answer 1

粗略搜索后，似乎没有任何专门用于此目的的 SAT 求解器或算法来执行您提到的转换。因此，您的两个问题的答案似乎都是“否”。

为此使用 SAT 求解器也存在一些概念性问题。看起来你的变量域是连续的，这意味着它不能直接转换为 SAT。您需要离散化您的域。第二个问题是您需要检查不等式，您可以在 SAT 中对其进行编码，但您冒着问题规模呈指数增长的风险。

更合适的范例是 constraint programming ，尽管支持连续域的求解器很少见。

总而言之，在我看来，您当前的分支定界方法可能是最合适的方法。我不相信子句学习等技术对您的特定应用程序有用，因为您正在处理真实的时间间隔。从句学习本质上做的是识别隐藏的问题结构，可以用来解决问题。它可能有助于对您的问题进行 SAT 编码，但所有要发现的结构都是将原始问题编码为 SAT 时丢失的内容。