z3中有实值计算的问题

Question

我正在研究一个我想根据某些约束来学习真实参数的问题。以下是代码片段：

s = Solver()
def logistic_function(x, y):
   out = y[0]
   for i in range(len(x)):
      out = out + x[i] * y[i + 1]
   return out

self.W = RealVector('w', X.shape[1]+1)
self.F = RealVector('f', X.shape[0])

for h in hard_instances:
  if y[h] == 1:
      self.model.add(Learner.logistic_function(list(X.iloc[h]), self.W) >= 0)         
  else:
      self.model.add(Learner.logistic_function(list(X.iloc[h]), self.W) < 0)         
  self.model.add(Learner.logistic_function(list(X.iloc[h]), self.W) == self.F[h])

s.check()

其中{X，y}是一个数据集，而hard_instances是我正在使用的一组索引。从z3获得模型解决方案后，我通过提取W并将其与F [h]值。以下是两者的结果（hard_instances的大小为100）：

使用z3输出计算的置信度值：

[-27.378400928361582, -24.54479132404113, -24.307289651276747, -31.70713297755848, -30.762167609027458, -31.315939646075787, -33.00420507718851, -31.744112911331754, -26.23355531746848, -31.36228488104281, -30.427736819536484, -31.50527359981793, -42.88965873739677, -31.707129367228667, -31.56210015506779, -32.12409972766397, -31.70713297755848, -30.031558658483476, -18.358324137431104, -32.05022247782185, -41.531034659230095, -32.29000919967995, -31.75974435910986, -31.663303581555095, -31.492373296661544, -31.31746775645906, -31.707165983877054, -31.347401145915946, -9013.822052472326, -31.75724273178162, -38.284678733394, -290.3139883637738, -38.55432745005057, 186.6069890256151, -44.1131569461781, -3965.3468548458463, -30.19582424657528, -31.81069063619864, -30.619869067329255, -31.58128167212442, -31.822174319008383, -37.18356870531899, -33.442884835165096, -51.320302912234084, -267.50833857889654, -28.402318357266232, -31.62745176425138, 416.1353823972281, -40.42543492186646, -28.541400567435975, -94.80187721209138, -32.013861248574415, -29.42849153859601, -32.14935341971468, -31.20975052479889, 34.2925702396417, -52.91711293409269, -31.772331866138927, -28.05140296433753, -36.58557486365847, -31.83338866474074, -36.5299223283415, -31.327926505869392, -199.5517369747143, -32.08369384912356, -32.07316618164427, -98.62741827618949, -1003.470954079502, -31.240876251803435, 456.34073138747084, -64.27303567782826, -49.714357622299886, -31.905532688175438, 15.611397869700923, 518.5055614575923, -30.65519656405803, -72.45941570859743, -31.967928531880276, -30.55418177994407, -31.225101988980224, -395.9939788509901, -53.142500004465916, -29.61894900393206, -31.756397212326476, -32.51642103656665, -31.12483808710671, -30.768528286960102, -765.2299421009044, 240.09127856915606, 47.958346445463505, -30.42562757004379, -34.02946877293487, 245.48085838630791, -53.48190520867068, -11.398510468740053, -27.119576978335733, -1472.8001539856432, -7.909727924310422, -31.984175109074794, -1246.733548266756]

F变量的值：

['6.63397?', '48.31824?', '9.84546?', '-0.5', '0', '0', '-0.5', '-5.38594?', '-0.5', '0', '2.67479?', '-3.55787?', '-10.59216?', '-0.5', '-2.87871?', '-0.5', '-0.5', '-0.5', '21.51906?', '-0.84313?', '0', '-0.5', '-0.5', '-0.5', '-3.33203?', '0', '-0.5', '0', '-8980.16307?', '-0.5', '-7.06012?', '-248.88109?', '-6.90423?', '-0.5', '-12.90605?', '-3945.30152?', '-0.5', '0', '2.09643?', '0.57093?', '-0.5', '0', '-0.5', '-0.5', '-227.57308?', '0', '0', '490.58834?', '-0.5', '0', '-20.46458?', '-0.5', '-0.5', '-0.5', '0', '75.43883?', '-0.5', '-0.5', '3.39666?', '-0.5', '-0.5', '0', '0', '-91.32681?', '-1.13005?', '0', '-41.40830?', '-972.60267?', '0', '-0.5', '0', '0', '-0.5', '43.98384?', '570.67543?', '-0.5', '-41.06592?', '0', '8.24429?', '-3.43914?', '-377.45813?', '-21.85040?', '0', '-11.83317?', '-4.00421?', '-0.5', '0.53349?', '-691.19144?', '264.52677?', '68.84287?', '9.83243?', '3.52497?', '269.78794?', '-21.63869?', '40.52079?', '6.89110?', '-1451.54107?', '26.21240?', '0', '-1190.68525?']

似乎在z3内计算出的值（用F表示）与我根据从z3得到的解计算出的值之间存在巨大差异。这些值应该相同。

此外，hard_instances是来自完整数据集的随机样本。这种差异仅在某些样本中发生。对于许多样本，我计算出的值与我从z3获得的值相同。此外，如果我使用Integer求解器并学习整数参数而不是实数参数，则也没有差异。

Answer 1

您是说z3给您一个incorrect模型，还是您说它与使用其他方法计算出的值不匹配？从您的帖子中很难理解。

请注意，z3将为您提供a满足约束条件的解决方案。您确定它们是唯一的吗？如果可以对约束有多种解决方案，那么您可能会得到一个完全有效的模型，但不是您所期望的。例如，如果您对系统的约束不足，则会发生这种情况。

还要记住，您在z3之外的计算可能是使用浮点数完成的，并且可能会潜入计算误差。Z3的Reals是代数实数：即，对它们的算术是精确的。使用浮点，您可能会得到不同的结果。 （尽管除非问题中存在巨大的不稳定性，否则差异不应该那么大；尤其是对于较小的数字。）

如果您说的是z3的模型不是满足约束，那么那当然是应该报告的错误。如果您怀疑是这种情况，请发布MCVE：https://stackoverflow.com/help/minimal-reproducible-example共享代码不错，但是如果我们自己不能加载/运行它，那么它实际上并没有太大帮助。