Testing logical equivalences (and more) using Z3 Theorem Prover

#computerscience #discretemath #logic #smtsolvers

Z3 Theorem Prover is an SMT solver which can find solutions (if exists) to a wide range of problems ranging from number theory to propositional and predicate logic and conversely can also prove exhaustively that a certain statement/theorem or set of statements is always or never true. I discovered it through certain online chats quite a few months ago but quickly dismissed it after playing with it for about an hour or two, finding little practical use with it. However, having recently enrolled in a discrete math course required by my major (Computer Engineering) in my university, it proved to be a useful tool in terms of helping me understand logical reasoning and deduction in general as well as verifying the solutions to certain homework questions on propositional and predicate logic. This article aims to introduce the Z3 theorem prover and its applications in propositional and predicate logic.

To begin, visit rise4fun where you can try out the Z3 theorem prover online.

Now let us recap what a proposition is:

A proposition is a statement that is either true or false but not both.

So the following are propositions:

"I have 10 dollars in my wallet." (Either I have it [true] or I don't [false])
"Amy can write a Hello World program in Python." (Similar to above)
"Doug likes pizza." (Similar to above)

And the following are not:

"Hello, how are you?" (An open-ended question that can't be determined to be true or false)
"Get our company website up and running by the end of September." (A command)
"This statement is false." (logical paradoxes are not considered propositions)

In Z3 theorem prover, propositions are modeled as booleans (as in any programming language), or rather, Bools. So, if we want to say that "p is a(n) (arbitrary) proposition and q is a(n) (arbitrary) proposition" then we would write the following in Z3 (the line starting with a ; is a Z3 comment):

; p and q are arbitrary propositional constants
(declare-const p Bool)
(declare-const q Bool)

As you may have noticed, Z3 has a Lisp-like syntax - everything is surrounded by parentheses and every function/operator (even operators commonly written in infix notation such as + or -) is written in prefix notation. Such notation may feel unfamiliar with you if you're coming from a C-like background (e.g. C/C++/ObjC, C#/Java, JavaScript) or similar; however, don't worry as you do not need to know any Lisp to use Z3 (I don't know any Lisp either) and Z3 is quite simple and intuitive. That being said, it is possible to access Z3 through APIs in many common programming languages (e.g. Python or C) which could allow you to avoid the Lisp-like syntax completely but we won't be covering that in this article.

Currently, our Z3 "program" does nothing useful - we've declared two arbitrary propositional constants p and q but we haven't stated what we want to do with it. So let's ask Z3 to confirm whether an arbitrary proposition p could possibly be true. This is done by using an assertion: (assert p). To check whether all of our assertions can be satisfied (i.e. there exists at least a set of values for the constants we defined such that all our assertions are true), we need to add a (check-sat) below our declarations and assertions:

(declare-const p Bool)
(declare-const q Bool)
(assert p)
(check-sat)

When you run the code, you should see sat (short for "satisfiable") displayed. This means that there exists at least one set of possible values (p, q) such that our assertion p is true. So when is our assertion true? We can add a line (get-model) below our (check-sat) which displays one possible solution to our assertion:

(declare-const p Bool)
(declare-const q Bool)
(assert p)
(check-sat)
(get-model)

You should see something similar to this:

sat
(model 
  (define-fun p () Bool
    true)
)

Because we aren't asserting anything meaningful, Z3 simply states the obvious - our assertion p is true when the arbitrary proposition p is set to true. But wait - didn't we declare p as a constant? Why is it a function (define-fun) now? In fact, arbitrary constants in Z3 are treated as null-ary functions, i.e. functions accepting no arguments and returning a (constant) result.

Now let us see a not-as-trivial example - given two arbitrary propositions p and q, when is p ∧ q (read "p and q") true? In Z3, the logical conjunction ∧ is a function/operator and accepting two Bools and producing a Bool:

(declare-fun p () Bool) ; Recall that a Z3 constant is just a null-ary function returning a constant result
(declare-const q Bool)
(assert (and p q)) ; (and p q) invokes the `and` function/operator with the two arguments, p and q
(check-sat)
(get-model)

As expected, Z3 tells us that p ∧ q is true when p and q are both true. Note that (get-model) merely displays one possible solution to our assertions - we cannot conclude from the output produced that p ∧ q only when p and q are both simultaneously true:

(declare-fun p () Bool)
(declare-const q Bool)
(assert (or p q)) ; We know there are 3 cases where p ∨ q is true; how many will Z3 display?
(check-sat)
(get-model)

The output of the code example directly above only displays one of the three possible solutions - when q is false and p is true. It was possible to retrieve more than one model directly in older Z3 versions through the (next-sat) command and it is still possible to retrieve all possible solutions indirectly by accessing Z3 through an API but it will not be covered in this article as one example/counterexample is usually sufficient to make an argument.

So far we've seen that Z3 is useful in finding solutions but how can we use it to prove or disprove a certain theorem (or proposition/statement in our case)? This is achieved by asserting the negation of the statement we want to prove - if it gives unsat (short for "unsatisfiable") then our original statement is not falsifiable, i.e. it is always true. Consider p ∨ ¬p - we can easily see that it is a tautology (a proposition that is always true regardless of the truth values of its propositional variables) by looking at its truth table for various values of p so we show it in Z3 by asserting its negation:

(declare-const p Bool)
(define-fun conjecture () Bool
  (or p (not p))
) ; Our conjecture - p ∨ ¬p is a tautology
(assert (not conjecture)) ; assert its negation
(check-sat) ; displays `unsat` as expected

N.B. if a set of assertions give unsat and you try to (get-model) then it results in an error - you can try it ;)

Let's look at a more complicated example. Suppose for some propositions p, q and r, p implies q and q implies r. Then, by common sense, it follows that p must imply r. Let's try to prove it using Z3 theorem prover:

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(define-fun conjecture () Bool
  (=> (and (=> p q) (=> q r)) (=> p r)) ; (=> p q) means "p implies q"
)
(assert (not conjecture))
(check-sat) ; gives `unsat` as expected

However, when this first popped up in my head, I made the logical fallacy of thinking that saying "p implies q and q implies r" is logically equivalent to saying "p implies r". Let's disprove my conjecture using Z3 theorem prover:

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(define-fun conjecture () Bool
  ; logical equivalence/bi-implication is denoted by `=`, e.g. (= p q)
  (= (and (=> p q) (=> q r)) (=> p r))
)
(assert (not conjecture))
(check-sat) ; gives `sat`; my conjecture is falsifiable
(get-model)

It turns out that we cannot use the statements (p → q) ∧ (q → r) and p → r interchangeably for any p, q and r - specifically, when p and r are both true and q is false, the left-hand side expression gives (p → q) ∧ (q → r) ≡ (T → F) ∧ (F → T) ≡ F ∧ T ≡ F but the right-hand side expression gives p → r ≡ T → T ≡ T.

To conclude this article, let us see an example of predicate logic in Z3 theorem prover.

There are only 2 quantifiers in predicate logic - the universal quantifier ∀ and the existential quantifier ∃. So how do we express a statement like "There is exactly 1 person in this class who owns a computer" using predicate logic? My professor suggested the following during the lecture:

∃x (P(x) ∧ ∀y ((y ≠ x) → ¬P(y))) [the domain of x is all people in the class and P(x) is the statement "x owns a computer"]

I thought about it after the lecture and it dawned on me that there is probably a more succinct way of expressing that:

∃x ∀y (P(y) ↔ (y = x))

So I set out to prove it using Z3 theorem prover:

(declare-sort U) ; let U be an arbitrary domain
(declare-fun p (U) Bool) ; let p be an arbitrary predicate on members of U
(define-fun conjecture () Bool
  (=
    (exists ((x U)) (and (p x) (forall ((y U)) (=> (not (= y x)) (not (p y))))))
    (exists ((x U)) (forall ((y U)) (= (p y) (= y x))))
  )
)
(assert (not conjecture))
(check-sat)

... and it displayed unsat as I anticipated.

Thanks for reading my article - I hope this was a good introduction to theorem provers and their potential applications. Feel free to leave your feedback in the comments :)