CODEWITHSUNDEEP
z3smt
Kshitij Goyal
Kshitij Goyal

Reputation: 61

Issues with real value calculation in z3

I am working on a problem where I want to learn real parameters based on certain constraints. Following is a snippet of the code:

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()

Where {X,y} is a dataset and hard_instances is a set of indexes that I am working with. After I get a model solution from the z3, I manually calculate the Learner.logistic_function(list(X.iloc[h]), self.W) value for each of the indices in the hard_instance by extracting the W and compare it with the F[h] values. Following are the results for both (with the size of hard_instances being 100):

Confidence value calculated using z3 output:

[-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]

Values of the F variable:

['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?']

There seems to be a huge difference in the values calculated within z3 (represented by F) and values I calculate based on the solution that I get from z3. These values should be same.

Also, hard_instances are random samples from the full dataset. This kind of discrepancy happens only with some samples. For a lot of the samples, the value I calculate and the value I get from z3 are same. Also, there is no discrepancy if I use the Integer solver and learn integer parameters instead of real ones.

Upvotes: 0

Views: 148

Answers (1)

alias
alias

Reputation: 30525

Are you saying z3 is giving you an incorrect model, or are you saying it doesn't match what you calculated using other means? It's hard to understand from your post.

Note that z3 will give you a solution that satisfies the constraints. Are you sure they are unique? If there can be multiple solutions to the constraints, you might be getting a totally valid model but not what you expected. This can happen if you under-constrain the system, for instance.

Also keep in mind that your calculations outside of z3 are probably done using floating-point numbers, and there might be computational errors creeping in. Z3's Reals are algebraic-reals: i.e., arithmetic on them are precise. With floating point, you might be getting results that differ. (Though unless there's huge instabilities in the problem, the differences shouldn't be that large; especially for small numbers.)

If you're saying z3's model does not satisfy the constraints, then that would be a bug that should be reported, of course. If you suspect that is the case, then please post an MCVE: https://stackoverflow.com/help/minimal-reproducible-example Sharing code is nice, but if we can't load/run it ourselves, it doesn't really help all that much.

Upvotes: 1

Related Questions