1

The following code

(declare-fun f (Int) Real)
(declare-fun g (Int) Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-model)

returns "unknown", even though there is an obvious solution. Eliminating arguments to f and g (effectively making them constants?) results in "sat" with expected assignments. I guess, my question is: what is special about arithmetic with uninterpreted functions?

BTW, replacing * with + also results in "sat", so the issue is not about uninterpreted functions, per se, but about how they are combined.

Additional thoughts

Making the domain (very) finite does not help, e.g.,

(declare-fun f (Bool) Real)
(declare-fun g (Bool) Real)
(declare-const x Bool)
(declare-const y Bool)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-model)

returns "unknown". This is odd given that f:Bool->Real is essentially just two variables f(False) and f(True) (of course, the solver has to recognize this).

Inability to handle non-linear arithmetic over real-valued uninterpreted functions is a very severe limitation because arrays are implemented as uninterpreted functions. So, for example,

(declare-const a (Array Int Real))
(assert (= (* (select a 1) (select a 1)) 1))
(check-sat)
(get-model)

returns "unknown". In other words, any non-linear algebraic expression on real array elements involving multiplication is unsolvable:'(

Daniel Genin
  • 463
  • 5
  • 10

1 Answers1

2

It's the non-liearity introduced by the multiplication that makes the problem hard to solve, not the uninterpreted functions. In fact, you can ask the solvers why by using the get-info command:

(set-logic QF_UFNIRA)
(declare-fun f (Int) Real)
(declare-fun g (Int) Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (* (f x) (g y)) 1.0))
(check-sat)
(get-info :reason-unknown)

Here're some responses I got from various solvers:

Z3:

(:reason-unknown smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic)))

CVC4:

(:reason-unknown incomplete)

MathSAT:

(error "sat, but with non-linear terms")

So, as the solvers themselves improve and start handling more nonliear arithmetic, you might get models eventually. But, in general, nonlinear problems will always be problematic as they are undecidable when integers are involved. (Since you can code Diophantine equations using non-linear terms.)

See also How does Z3 handle non-linear integer arithmetic? for a relevant discussion from 2012.

Removing uninterpreted functions

Even if you get rid of the uninterpreted functions, you'd still be in the unknown land, so long as you mix Int and Real types and non-linear terms:

(set-logic QF_NIRA)
(declare-const f Real)
(declare-const g Real)
(declare-const x Int)
(declare-const y Int)
(assert (= (+ (* f g) (to_real (+ x y))) 1.0))
(check-sat)
(get-info :reason-unknown)

Z3 says:

(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))")

So, the issue would arise with mixed types and non-linear terms.

Community
  • 1
  • 1
alias
  • 28,120
  • 2
  • 23
  • 40
  • It seems the uniterpreted functions must have something to do with "unknown" since replacing them with constants returns "sat". – Daniel Genin Apr 05 '17 at 20:29
  • Did you still mix `Int` and `Real`? If all your types are `Real`, I can see that, but if you mix `Int` and `Real` and introduce non-linear terms, I'm sure the solver will be `unknown` land pretty quickly. See my updated answer for an example. – alias Apr 06 '17 at 02:28
  • Good point about mixing `Int` and `Real`. It looks like uninterpreted functions with domain and range `Int` can be solved for in non-linear expressions. – Daniel Genin Apr 06 '17 at 13:01
  • Quite right. However, there's hope. While there will never be a complete solver for such problems due to fundamental undecidability issues, solvers do get better in time. It wouldn't surprise me if Z3 or some other solver handled these sorts of combinations that arise in practice quite efficiently as they improve their heuristics and algorithms. – alias Apr 06 '17 at 16:56