Finding real solutions to problem is slower than expected

Question

Sorry this is a basic question, I'm new to z3.

I wrote a program to find a real solution to a certain equation. Since it should be generated for every equation, I can't simplify the equation to much beforehand. But the program is really slow. It is a long equation, but I only have 4 unknown variables, so I wouldn't expect it to take this long (Similar equations (but shorter) had a much shorter runtime and where done in milliseconds). Did I somehow create a loop or is this equation really to complicated.

(declare-const l1 Real)

(declare-const l0 Real)

(declare-const sqrt0 Real)

(assert 
  (>= sqrt0 0)
)

(assert 
  (= 
    (^ sqrt0 2)
   
    (+ 
      (^ l0 2)
     
      (^ l1 2)
    )
  )
)

(declare-const sqrt1 Real)

(assert 
  (>= sqrt1 0)
)

(assert 
  (= 
    (^ sqrt1 2)
   
    (- 
      (^ sqrt0 2)
     1)
  )
)

(assert 
    (= 
      (+ 
        (^ 
          (- 0.625000 l0)
         2)
       
        (^ 
          (- 0.414578 l1)
         2)
      )
     
      (^ 
        (+ 
          (/ 1 
            (- 
              (* -2 sqrt0)
             
              (* 2 sqrt1)
            )
          )
         
          (+ 
            (* 0.5 sqrt0)
           
            (* 0.5 sqrt1)
          )
        )
       2)
    )
)
(assert 
    (= 
      (+ 
        (^ 
          (- 0.500000 l0)
         2)
       
        (^ 
          (- 0.000000 l1)
         2)
      )
     
      (^ 
        (+ 
          (/ 1 
            (- 
              (* -2 sqrt0)
             
              (* 2 sqrt1)
            )
          )
         
          (+ 
            (* 0.5 sqrt0)
           
            (* 0.5 sqrt1)
          )
        )
       2)
    )
  )
)

(check-sat)

I tried using the FloatingPoint type with the built in fp.sqrt function, but it didn't make program any faster (Maybe I'm wrong but I also couldn't find a built square function for FLoatingPoint, so I used fp.mul). I hoped using the fp.sqrt function would help alot, as after is should only have two unknown constants.

Thanks in advance and sorry if this is a stupid question.

Answer 1

It's anybody's guess when a solver takes too long to answer: It could be stuck in some sort of a non-productive loop, or the problem can genuinely be too hard to solve. From this perspective, most solvers act as a block-box: Unless you're intimately familiar with their internals, it's hard to guess what might be going wrong.

If you do believe this should be "easy" to solve, you can file a ticket at: https://github.com/Z3Prover/z3/issues and have the developers take a look. I doubt this'll be very productive, but they might be able to trace the internals and at least tell if this is a genuine issue, or just simply too difficult.

The other option is to use dReal: http://dreal.github.io. Note that dReal is a delta-sat tool, i.e., the solutions are considered OK up to a certain numerical error bound, which can be specified by the user. Since the result doesn't have to be precise, it can run a lot faster and usually finds "acceptable" solutions. Of course, what acceptable means will depend on your particular problem domain, and you might have to tweak with parameters a bit. (For instance, you might have to assert some upper-lower bounds for l0 and l1, so you don't run into floating-point overflows. In dReal, "real" numbers are modeled by IEEE-double-precision-floating point values.)

So, I'd give dReal a try, and see if it works better for you. But keep in mind that the solutions will be within an error-bound, which might be just fine for your application.