An operator to choose an aribirary value satisfying a predicate can be very useful.
This article assumes knowledge of first-order logic and SMT-LIB.
Sometimes when writing (or generating) an SMT-LIB query, you need to select an arbitrary value that satisfies some predicate but doesn't have a fully-specified value:
(declare-sort IntSet 0)
(declare-fun in (Int IntSet) Bool)
(declare-const S IntSet)
(declare-const T IntSet)
(declare-const result IntSet)
; Goal: compute (union S T) without asking the solver to produce a model
; for a "union" function.
;
; Oops! This won't work. There is no "choose" operation in SMT-LIB.
(assert (= result
(choose ((x IntSet))
(forall ((i Int)) (= (in i x) (or (in i S) (in i T)))))))
Formally, choose is known as Hilbert's Epsilon Operator. It can be found in some formal languages like TLA+.
The easiest way to achieve such an arbitrary choice in SMT-LIB is to introduce a new variable to represent the value chosen, and constrain it appropriately:
(declare-const choice IntSet)
(assert (forall ((i Int)) (= (in i choice) (or (in i S) (in i T)))))
; Better. :)
(assert (= result choice))
We have to decide what choose should do if no element satisfies the requirement:
(declare-const choice Int)
(define-fun P ((x Int)) Bool (and (< x 0) (> x 0)))
(assert (P choice))
(check-sat) ; unsat!?
The simplest approach is to allow such a query to return UNSAT. However, this can be confusing in large formulas, since it is difficult to distinguish between "the formula is unsatisifable because there is no legal choice for some value" or "the formula is unsatisifiable because one of your top-level constraints failed".
However, we can give the solver an "out" by letting each choice be unspecified when there is no legal value:
(declare-const choice Int)
(define-fun P ((x Int)) Bool (and (< x 0) (> x 0)))
(assert (or
(P choice)
(not (exists ((x Int)) (P x)))))
(check-sat) ; sat
Giving the solver an "out" ensures that choosing a value can never make the formula unsatisfiable, at the cost of introducing a quantifier that may cause the solver to return "unknown".
Sometimes you need to choose a value that relates some bound variables, such as the arguments in my-div below:
(declare-fun my-div ((n Int) (d Int)) Int
(choose ((result Int)) (= (* result d) n)))
Naively pulling out a single choice variable is clearly wrong:
(declare-const choice Int)
; ... but now `my-div` does not depend on its arguments!
(declare-fun my-div ((n Int) (d Int)) Int choice)
; ... and `n` and `d` are not in scope!
(assert (or
(= (* choice d) n)
(not (exists ((x Int)) (= (* x d) n)))))
The easiest way to achieve this is to define a choice function that maps each valuation for the bound variables to a choice:
(declare-fun choice (Int Int) Int)
(declare-fun my-div ((n Int) (d Int)) Int (choice n d))
(assert (forall ((n Int) (d Int))
(or
(= (* (choice n d) d) n)
(not (exists ((x Int)) (= (* x d) n))))))
This approach works for bound variables in forall, exists, and let expressions as well.
Unfortunately, this construction introduces a forall-quantifier that can easily cause the solver to return "unknown". There are some tricks you can play here to help:
my-div during constraint generation to avoid introducing universal quantifiers.(forall ... (=> path-condition ...)). I have found this can have an enormous impact, but is very tricky to get right.Do not confuse "arbitrary" with "nondeterministic".
The techniques in this article give you an arbitrary choice operator that is deterministic for each lexical occurrence. This is very different from a nondeterministic choice. A nondeterministic choice operator would give a different value each time it is "evaluated". SMT-LIB sentences are not "evaluated" by the solver, and so there is no obvious way to bolt on nondeterminism.
The construction above is also different from a true deterministic choice operator, since different choice variables can have different values, even if they are constrained in the same way. For example, a and b can take on different values even though their constraints are semantically equivalent:
; choose a : a > 0
(declare-const a Int)
(define-fun P ((x Int)) Bool (> x 0))
(assert (P a))
; choose b : b >= 0 and b != 0
(declare-const b Int)
(define-fun Q ((x Int)) Bool (and (>= x 0) (distinct x 0)))
(assert (Q b))
(assert (distinct a b))
(check-sat) ; sat
To implement true deterministic choice, you would need to add an assertion to the solver along the lines of "for all predicates P and Q, if P and Q are semantically equivalent, then the values chosen according to P and accoding to Q are equal". This is a second-order axiom, but it can be specialized for each P and Q that are used in your formula to produce a first-order constraint:
; ... define "a" and "b" as above
; "forall" P & Q : (P <-> Q) -> (choose P = choose Q)
(assert (=>
(forall ((x Int)) (= (P x) (Q x)))
(= a b)))
Usually this isn't worth it. For more discussion, see the 2015 article "Compiling Hilbert's Epsilon Operator" by Rustan Leino.