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

Question

布尔可满足性问题是用于检查布尔表达式可满足性的概括。现在布尔表达式由多项式的非负性算法生成。例如，多项式可以是并且具有某个区间，例如变量的数量在哪里。我目前使用特殊算法（例如分支定界算法）检查多项式的特征，例如非负性，在这种算法中，我将大问题转化为较小的问题，但缺少一些 SAT 求解器（例如MiniSat ）承诺的学习功能。所以

1. 一些 SAT 求解器旨在检查多项式的属性，例如多线性函数或一般多元函数？

2. 将多元函数和非负性算法转换为布尔表达式的任何简单方法？

Answer 1

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

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

更合适的范例是约束规划，尽管支持连续域的求解器很少见。

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