xhajnal commented 5 years ago

Some of the results shows all unsat even when the param exists:

alpha, n_samples, max_depth, min_rect_size , population, algorithm, v_p, v_q 0.95, 100, 12, 1e-05, 5, 1, 0.45223461506339047, 0.5057623641293089

xhajnal commented 5 years ago

[x] factorisation
```
from z3 import *
```

p = Real('p') q = Real('q') s = Solver() s.add( p >= 0, q >= 0, p<=1, q<=1)

s.add( -(p - 1)**5 > (-1)*p**5+5*p**4-10*p**3+10*p**2-5*p+1 )

s.add( 5p(p - 1)**4*(q - 1)**4 > (5*q**4p5-20q*3p5-20q4p**4+30q2p5+80q3p4+30q4p3-20qp5-120q2p4-120q3p3-20q4p**2+5p5+80qp4+180q*2p3+80q3p**2+5q4p-20p4-120qp3-120q2*p**2-20q3p+30p3+80qp2+30q2p-20p2-20qp+5*p))

s.add( -10p(p - 1)**3(q - 1)3(2pq - p - 2q) > ((-20)q**4p5+70q*3p5+80q4p**4-90q2p5-270q3p4-120q4p3+50qp5+330q2p4+390q3p3+80q4p**2-10p5-170qp4-450q*2p3-250q3p**2-20q4p+30p4+210qp3+270q2*p**2+60q3p-30p3-110qp2-60q2p+10p2+20qp) )

s.add( 10p(p - 1)**2(q - 1)2(3p2q**2 - 3p2q + p2 - 6pq2 + 3pq + 3q2) > (30q4*p**5-90q3p5-120q4p4+100q2p**5+330q3p4+180q4p3-50qp5-320q2p4-450q3p**3-120q4p2+10p5+130qp4+370q2p3+270q3p2+30q4p-20p4-110qp3-180q2p2-60*q3p+10p3+30qp**2+30q2p))

s.add( -5p(p - 1)(q - 1)(2pq - p - 2q)(2p2q**2 - 2p2q + p2 - 4pq2 + 2pq + 2q2) > ((-20)q*4p5+50q3p**5+80q4p4-50q2p5-170q3p**4-120q4p3+25qp5+130q2p**4+210q3p3+80q4p2-5p5-45qp4-110q2*p**3-110q3p2-20*q4p+5p4+20qp**3+30q2p**2+20q3p))

s.add( p(5p4*q*4 - 10p4*q3 + 10*p*4q2 - 5*p4*q + p*4 - 20p3*q4 + 30*p*3q3 - 20*p3*q*2 + 5p3q + 30p2*q*4 - 30p2*q3 + 10*p*2q2 - 20pq4 + 10pq3 + 5*q4) > (5*q*4p5-10*q3*p*5-20q4*p4+10*q*2p5+30*q3*p*4+30q4*p3-5qp5-20*q2*p*4-30q3*p3-20*q*4p2+p5+5qp4+10*q2*p*3+10q3*p*2+5q*4p)) print(s.check())

each unsat

more refine

from z3 import *

p = Real('p') q = Real('q') s = Solver() s.add( p >= 0, q >= 0, p<=1, q<=1)

s.add( Or([-(p - 1)5 > (-1)*p*5+5p4-10*p3+10*p*2-5p+1, -(p - 1)5 < (-1)*p5+5*p*4-10p3+10*p*2-5p+1,

   5*p*(p - 1)**4*(q - 1)**4 > (5*q**4*p**5-20*q**3*p**5-20*q**4*p**4+30*q**2*p**5+80*q**3*p**4+30*q**4*p**3-20*q*p**5-120*q**2*p**4-120*q**3*p**3-20*q**4*p**2+5*p**5+80*q*p**4+180*q**2*p**3+80*q**3*p**2+5*q**4*p-20*p**4-120*q*p**3-120*q**2*p**2-20*q**3*p+30*p**3+80*q*p**2+30*q**2*p-20*p**2-20*q*p+5*p),
   5*p*(p - 1)**4*(q - 1)**4 < (5*q**4*p**5-20*q**3*p**5-20*q**4*p**4+30*q**2*p**5+80*q**3*p**4+30*q**4*p**3-20*q*p**5-120*q**2*p**4-120*q**3*p**3-20*q**4*p**2+5*p**5+80*q*p**4+180*q**2*p**3+80*q**3*p**2+5*q**4*p-20*p**4-120*q*p**3-120*q**2*p**2-20*q**3*p+30*p**3+80*q*p**2+30*q**2*p-20*p**2-20*q*p+5*p),

   -10*p*(p - 1)**3*(q - 1)**3*(2*p*q - p - 2*q) > ((-20)*q**4*p**5+70*q**3*p**5+80*q**4*p**4-90*q**2*p**5-270*q**3*p**4-120*q**4*p**3+50*q*p**5+330*q**2*p**4+390*q**3*p**3+80*q**4*p**2-10*p**5-170*q*p**4-450*q**2*p**3-250*q**3*p**2-20*q**4*p+30*p**4+210*q*p**3+270*q**2*p**2+60*q**3*p-30*p**3-110*q*p**2-60*q**2*p+10*p**2+20*q*p),
   -10*p*(p - 1)**3*(q - 1)**3*(2*p*q - p - 2*q) < ((-20)*q**4*p**5+70*q**3*p**5+80*q**4*p**4-90*q**2*p**5-270*q**3*p**4-120*q**4*p**3+50*q*p**5+330*q**2*p**4+390*q**3*p**3+80*q**4*p**2-10*p**5-170*q*p**4-450*q**2*p**3-250*q**3*p**2-20*q**4*p+30*p**4+210*q*p**3+270*q**2*p**2+60*q**3*p-30*p**3-110*q*p**2-60*q**2*p+10*p**2+20*q*p),

   10*p*(p - 1)**2*(q - 1)**2*(3*p**2*q**2 - 3*p**2*q + p**2 - 6*p*q**2 + 3*p*q + 3*q**2) >  (30*q**4*p**5-90*q**3*p**5-120*q**4*p**4+100*q**2*p**5+330*q**3*p**4+180*q**4*p**3-50*q*p**5-320*q**2*p**4-450*q**3*p**3-120*q**4*p**2+10*p**5+130*q*p**4+370*q**2*p**3+270*q**3*p**2+30*q**4*p-20*p**4-110*q*p**3-180*q**2*p**2-60*q**3*p+10*p**3+30*q*p**2+30*q**2*p),
   10*p*(p - 1)**2*(q - 1)**2*(3*p**2*q**2 - 3*p**2*q + p**2 - 6*p*q**2 + 3*p*q + 3*q**2) <  (30*q**4*p**5-90*q**3*p**5-120*q**4*p**4+100*q**2*p**5+330*q**3*p**4+180*q**4*p**3-50*q*p**5-320*q**2*p**4-450*q**3*p**3-120*q**4*p**2+10*p**5+130*q*p**4+370*q**2*p**3+270*q**3*p**2+30*q**4*p-20*p**4-110*q*p**3-180*q**2*p**2-60*q**3*p+10*p**3+30*q*p**2+30*q**2*p), 

   -5*p*(p - 1)*(q - 1)*(2*p*q - p - 2*q)*(2*p**2*q**2 - 2*p**2*q + p**2 - 4*p*q**2 + 2*p*q + 2*q**2) > ((-20)*q**4*p**5+50*q**3*p**5+80*q**4*p**4-50*q**2*p**5-170*q**3*p**4-120*q**4*p**3+25*q*p**5+130*q**2*p**4+210*q**3*p**3+80*q**4*p**2-5*p**5-45*q*p**4-110*q**2*p**3-110*q**3*p**2-20*q**4*p+5*p**4+20*q*p**3+30*q**2*p**2+20*q**3*p),
   -5*p*(p - 1)*(q - 1)*(2*p*q - p - 2*q)*(2*p**2*q**2 - 2*p**2*q + p**2 - 4*p*q**2 + 2*p*q + 2*q**2) < ((-20)*q**4*p**5+50*q**3*p**5+80*q**4*p**4-50*q**2*p**5-170*q**3*p**4-120*q**4*p**3+25*q*p**5+130*q**2*p**4+210*q**3*p**3+80*q**4*p**2-5*p**5-45*q*p**4-110*q**2*p**3-110*q**3*p**2-20*q**4*p+5*p**4+20*q*p**3+30*q**2*p**2+20*q**3*p),

   p*(5*p**4*q**4 - 10*p**4*q**3 + 10*p**4*q**2 - 5*p**4*q + p**4 - 20*p**3*q**4 + 30*p**3*q**3 - 20*p**3*q**2 + 5*p**3*q + 30*p**2*q**4 - 30*p**2*q**3 + 10*p**2*q**2 - 20*p*q**4 + 10*p*q**3 + 5*q**4) > (5*q**4*p**5-10*q**3*p**5-20*q**4*p**4+10*q**2*p**5+30*q**3*p**4+30*q**4*p**3-5*q*p**5-20*q**2*p**4-30*q**3*p**3-20*q**4*p**2+p**5+5*q*p**4+10*q**2*p**3+10*q**3*p**2+5*q**4*p),
   p*(5*p**4*q**4 - 10*p**4*q**3 + 10*p**4*q**2 - 5*p**4*q + p**4 - 20*p**3*q**4 + 30*p**3*q**3 - 20*p**3*q**2 + 5*p**3*q + 30*p**2*q**4 - 30*p**2*q**3 + 10*p**2*q**2 - 20*p*q**4 + 10*p*q**3 + 5*q**4) < (5*q**4*p**5-10*q**3*p**5-20*q**4*p**4+10*q**2*p**5+30*q**3*p**4+30*q**4*p**3-5*q*p**5-20*q**2*p**4-30*q**3*p**3-20*q**4*p**2+p**5+5*q*p**4+10*q**2*p**3+10*q**3*p**2+5*q**4*p),

   p*(5*p**4*q**4 - 10*p**4*q**3 + 10*p**4*q**2 - 5*p**4*q + p**4 - 20*p**3*q**4 + 30*p**3*q**3 - 20*p**3*q**2 + 5*p**3*q + 30*p**2*q**4 - 30*p**2*q**3 + 10*p**2*q**2 - 20*p*q**4 + 10*p*q**3 + 5*q**4) > (5*q**4*p**5-10*q**3*p**5-20*q**4*p**4+10*q**2*p**5+30*q**3*p**4+30*q**4*p**3-5*q*p**5-20*q**2*p**4-30*q**3*p**3-20*q**4*p**2+p**5+5*q*p**4+10*q**2*p**3+10*q**3*p**2+5*q**4*p),
   p*(5*p**4*q**4 - 10*p**4*q**3 + 10*p**4*q**2 - 5*p**4*q + p**4 - 20*p**3*q**4 + 30*p**3*q**3 - 20*p**3*q**2 + 5*p**3*q + 30*p**2*q**4 - 30*p**2*q**3 + 10*p**2*q**2 - 20*p*q**4 + 10*p*q**3 + 5*q**4) > (5*q**4*p**5-10*q**3*p**5-20*q**4*p**4+10*q**2*p**5+30*q**3*p**4+30*q**4*p**3-5*q*p**5-20*q**2*p**4-30*q**3*p**3-20*q**4*p**2+p**5+5*q*p**4+10*q**2*p**3+10*q**3*p**2+5*q**4*p)])
  )

print(s.check())



\>> unsat

xhajnal commented 5 years ago

[ ] SMT solver

from z3 import *

p = Real('p')
q = Real('q')
s = Solver()
s.add( p >= 0, q >= 0, p<=1, q<=1)
s.add( -(p - 1)**5 > 0 )
s.add( -(p - 1)**5 < 0.05243949578356076 )
s.add( 5*p*(p - 1)**4*(q - 1)**4 > 0)
s.add( 5*p*(p - 1)**4*(q - 1)**4 > 0.05243949578356076)
s.add( -10*p*(p - 1)**3*(q - 1)**3*(2*p*q - p - 2*q) > 0.02890940565345658)
s.add( -10*p*(p - 1)**3*(q - 1)**3*(2*p*q - p - 2*q) < 0.15109059434654343)
s.add( 10*p*(p - 1)**2*(q - 1)**2*(3*p**2*q**2 - 3*p**2*q + p**2 - 6*p*q**2 + 3*p*q + 3*q**2) > 0.09137732417251183)
s.add( 10*p*(p - 1)**2*(q - 1)**2*(3*p**2*q**2 - 3*p**2*q + p**2 - 6*p*q**2 + 3*p*q + 3*q**2) < 0.2486226758274882)
s.add( -5*p*(p - 1)*(q - 1)*(2*p*q - p - 2*q)*(2*p**2*q**2 - 2*p**2*q + p**2 - 4*p*q**2 + 2*p*q + 2*q**2) > 0.4170802307169153)
s.add( -5*p*(p - 1)*(q - 1)*(2*p*q - p - 2*q)*(2*p**2*q**2 - 2*p**2*q + p**2 - 4*p*q**2 + 2*p*q + 2*q**2) < 0.6229197692830847)
s.add( p*(5*p**4*q**4 - 10*p**4*q**3 + 10*p**4*q**2 - 5*p**4*q + p**4 - 20*p**3*q**4 + 30*p**3*q**3 - 20*p**3*q**2 + 5*p**3*q + 30*p**2*q**4 - 30*p**2*q**3 + 10*p**2*q**2 - 20*p*q**4 + 10*p*q**3 + 5*q**4) > 0.0997006426365767)
s.add( p*(5*p**4*q**4 - 10*p**4*q**3 + 10*p**4*q**2 - 5*p**4*q + p**4 - 20*p**3*q**4 + 30*p**3*q**3 - 20*p**3*q**2 + 5*p**3*q + 30*p**2*q**4 - 30*p**2*q**3 + 10*p**2*q**2 - 20*p*q**4 + 10*p*q**3 + 5*q**4) < 0.2602993573634233)
print(s.check())

>> unsat

xhajnal commented 5 years ago

[x] putting p,q values in the intervals

p = 0.45223461506339047
q = 0.5057623641293089

from sympy import Interval

#D3[("synchronous_parallel_",5,100,0.45223461506339047,0.5057623641293089)] = [0.02, 0.02, 0.09, 0.17, 0.52, 0.18]

#print(eval('-(p - 1)**5'))
#print(eval('5*p*(p - 1)**4*(q - 1)**4'))
#print(eval('-10*p*(p - 1)**3*(q - 1)**3*(2*p*q - p - 2*q)'))
#print(eval('10*p*(p - 1)**2*(q - 1)**2*(3*p**2*q**2 - 3*p**2*q + p**2 - 6*p*q**2 + 3*p*q + 3*q**2)'))
#print(eval('-5*p*(p - 1)*(q - 1)*(2*p*q - p - 2*q)*(2*p**2*q**2 - 2*p**2*q + p**2 - 4*p*q**2 + 2*p*q + 2*q**2)'))
#print(eval('p*(5*p**4*q**4 - 10*p**4*q**3 + 10*p**4*q**2 - 5*p**4*q + p**4 - 20*p**3*q**4 + 30*p**3*q**3 - 20*p**3*q**2 + 5*p**3*q + 30*p**2*q**4 - 30*p**2*q**3 + 10*p**2*q**2 - 20*p*q**4 + 10*p*q**3 + 5*q**4)'))

# f[5] in [p,q]= [0.04931430553373004, 0.012146618656640419, 0.09030005441060454, 0.26868678263438983, 0.37490621227921134, 0.20464602648542365]

#create_intervals(0.95, 100,D3[("synchronous_parallel_",5,100,0.45223461506339047,0.5057623641293089)])
# [(-0.012439495783560756, 0.05243949578356076),
# (-0.012439495783560756, 0.05243949578356076),
# (0.02890940565345658, 0.15109059434654343),
# (0.09137732417251183, 0.2486226758274882),
# (0.4170802307169153, 0.6229197692830847),
# (0.0997006426365767, 0.2602993573634233)]

print(eval('-(p - 1)**5') in Interval(-0.012439495783560756, 0.05243949578356076))
print(eval('5*p*(p - 1)**4*(q - 1)**4') in Interval(-0.012439495783560756, 0.05243949578356076))
print(eval('-10*p*(p - 1)**3*(q - 1)**3*(2*p*q - p - 2*q)') in Interval(0.02890940565345658, 0.15109059434654343))
print(eval('10*p*(p - 1)**2*(q - 1)**2*(3*p**2*q**2 - 3*p**2*q + p**2 - 6*p*q**2 + 3*p*q + 3*q**2)') in Interval(0.09137732417251183, 0.2486226758274882))
print(eval('-5*p*(p - 1)*(q - 1)*(2*p*q - p - 2*q)*(2*p**2*q**2 - 2*p**2*q + p**2 - 4*p*q**2 + 2*p*q + 2*q**2)') in Interval(0.4170802307169153, 0.6229197692830847))
print(eval('p*(5*p**4*q**4 - 10*p**4*q**3 + 10*p**4*q**2 - 5*p**4*q + p**4 - 20*p**3*q**4 + 30*p**3*q**3 - 20*p**3*q**2 + 5*p**3*q + 30*p**2*q**4 - 30*p**2*q**3 + 10*p**2*q**2 - 20*p*q**4 + 10*p*q**3 + 5*q**4)') in Interval(0.0997006426365767, 0.2602993573634233))

>> True True True False False True

xhajnal commented 5 years ago

In this case the 0.95 confidence interval is not enough to fit the interval

xhajnal / DiPS

Weird All unsat results #16

s.add( -(p - 1)**5 > (-1)*p**5+5*p**4-10*p**3+10*p**2-5*p+1 )

s.add( 5p(p - 1)**4*(q - 1)**4 > (5*q**4p5-20q*3p5-20q4p**4+30q2p5+80q3p4+30q4p3-20qp5-120q2p4-120q3p3-20q4p**2+5p5+80qp4+180q*2p3+80q3p**2+5q4p-20p4-120qp3-120q2*p**2-20q3p+30p3+80qp2+30q2p-20p2-20qp+5*p))

s.add( -10p(p - 1)**3(q - 1)3(2pq - p - 2q) > ((-20)q**4p5+70q*3p5+80q4p**4-90q2p5-270q3p4-120q4p3+50qp5+330q2p4+390q3p3+80q4p**2-10p5-170qp4-450q*2p3-250q3p**2-20q4p+30p4+210qp3+270q2*p**2+60q3p-30p3-110qp2-60q2p+10p2+20qp) )

s.add( 10p(p - 1)**2(q - 1)2(3p2q**2 - 3p2q + p2 - 6pq2 + 3pq + 3q2) > (30q4*p**5-90q3p5-120q4p4+100q2p**5+330q3p4+180q4p3-50qp5-320q2p4-450q3p**3-120q4p2+10p5+130qp4+370q2p3+270q3p2+30q4p-20p4-110qp3-180q2p2-60*q3p+10p3+30qp**2+30q2p))

s.add( -5p(p - 1)(q - 1)(2pq - p - 2q)(2p2q**2 - 2p2q + p2 - 4pq2 + 2pq + 2q2) > ((-20)q*4p5+50q3p**5+80q4p4-50q2p5-170q3p**4-120q4p3+25qp5+130q2p**4+210q3p3+80q4p2-5p5-45qp4-110q2*p**3-110q3p2-20*q4p+5p4+20qp**3+30q2p**2+20q3p))

xhajnal / DiPS

Weird All unsat results #16

s.add( -(p - 1)5 > (-1)*p*5+5p4-10*p*3+10p*2-5p+1 )

s.add( 5p(p - 1)4*(q - 1)*4 > (5q4*p5-20*q*3p5-20*q4*p*4+30q2*p5+80*q*3p4+30*q4*p3-20qp5-120*q2*p4-120*q*3p3-20*q4*p*2+5p5+80qp4+180*q*2p3+80*q3*p*2+5q4p-20p4-120qp3-120*q2*p*2-20q3p+30p3+80qp2+30*q2p-20p2-20qp+5*p))

s.add( -10p(p - 1)3*(q - 1)*3(2pq - p - 2q) > ((-20)q4*p5+70*q*3p5+80*q4*p*4-90q2*p5-270*q*3p4-120*q4*p3+50qp5+330*q2*p4+390*q*3p3+80*q4*p*2-10p5-170qp4-450*q*2p3-250*q3*p*2-20q4p+30p4+210qp3+270*q2*p*2+60q3p-30p3-110qp2-60*q2p+10p2+20qp) )

s.add( 10p(p - 1)2*(q - 1)2(3p2*q2 - 3*p2*q + p2 - 6pq2 + 3pq + 3*q2) > (30*q4*p*5-90q3*p5-120*q*4p4+100*q2*p*5+330q3*p4+180*q*4p3-50qp5-320*q*2p4-450*q3*p*3-120q4*p2+10*p5+130qp4+370*q2*p3+270*q*3p2+30*q4p-20p4-110qp3-180*q*2p2-60*q3p+10p3+30qp*2+30q*2p))

s.add( -5p(p - 1)(q - 1)(2pq - p - 2q)(2*p2*q*2 - 2p2*q + p2 - 4pq2 + 2pq + 2*q2) > ((-20)*q*4p5+50*q3*p*5+80q4*p4-50*q*2p5-170*q3*p*4-120q4*p3+25qp5+130*q2*p*4+210q3*p3+80*q*4p2-5*p5-45qp4-110*q2*p*3-110q3*p2-20*q4p+5p4+20qp*3+30q2*p*2+20q*3p))

s.add( -(p - 1)**5 > (-1)*p**5+5*p**4-10*p**3+10*p**2-5*p+1 )

s.add( 5p(p - 1)**4*(q - 1)**4 > (5*q**4p5-20q*3p5-20q4p**4+30q2p5+80q3p4+30q4p3-20qp5-120q2p4-120q3p3-20q4p**2+5p5+80qp4+180q*2p3+80q3p**2+5q4p-20p4-120qp3-120q2*p**2-20q3p+30p3+80qp2+30q2p-20p2-20qp+5*p))

s.add( -10p(p - 1)**3(q - 1)3(2pq - p - 2q) > ((-20)q**4p5+70q*3p5+80q4p**4-90q2p5-270q3p4-120q4p3+50qp5+330q2p4+390q3p3+80q4p**2-10p5-170qp4-450q*2p3-250q3p**2-20q4p+30p4+210qp3+270q2*p**2+60q3p-30p3-110qp2-60q2p+10p2+20qp) )

s.add( 10p(p - 1)**2(q - 1)2(3p2q**2 - 3p2q + p2 - 6pq2 + 3pq + 3q2) > (30q4*p**5-90q3p5-120q4p4+100q2p**5+330q3p4+180q4p3-50qp5-320q2p4-450q3p**3-120q4p2+10p5+130qp4+370q2p3+270q3p2+30q4p-20p4-110qp3-180q2p2-60*q3p+10p3+30qp**2+30q2p))

s.add( -5p(p - 1)(q - 1)(2pq - p - 2q)(2p2q**2 - 2p2q + p2 - 4pq2 + 2pq + 2q2) > ((-20)q*4p5+50q3p**5+80q4p4-50q2p5-170q3p**4-120q4p3+25qp5+130q2p**4+210q3p3+80q4p2-5p5-45qp4-110q2*p**3-110q3p2-20*q4p+5p4+20qp**3+30q2p**2+20q3p))