使用 Solver 验证属性答案

【问题标题】：Verifying properties using Solver使用 Solver 验证属性
【发布时间】：2015-06-01 10:40:11
【问题描述】：

我有一个如下形式的方程组：

x1 * x2 *.... * xn = a，其中 * 可以是 + 或 - 。

我正在建立一些其他相同形式的方程，我想验证如果他们对第一个系统感到满意。

我的问题是：有没有可以确定给定方程是否满足的求解器？

非常感谢，干杯

【问题讨论】：

【解决方案1】：

这是partition problem 的变体，带有偏差（您最终需要使一个子集比另一个子集大a，而不是它们相等）。可以通过在集合中添加a 来解决，现在解决“常规”分区问题。

这个问题是NP-Complete，但可以使用动态规划在伪多项式时间内解决：

D(x,i) = false   x<0
D(0,i) = true
D(x,0) = false   x != 0
D(x,i) = D(x,i-1) OR D(x-arr[i],i-1)

您正在寻找 sum (x1 + x2 + ... + xn + a) / 2 的子集

我们的想法是获得 2 套，一套带有a（让它成为A）和一套没有它（让它成为B）。

给A - 中的所有元素（a 除外）和B 中的所有元素一个+ 符号。
由于 sum(A) = sum(B)，你得到 p>

sum(B)-(sum(A)-a) = sum(B) - sum(A) + a = 0 + a = a

【讨论】：