# Propositional Logic

The pre-defined sort Bool is the sort (type) of all Boolean propositional expressions. Z3 supports the usual Boolean operators and, or, xor, not, => (implication), ite (if-then-else). Bi-implications are represented using equality =. The following example shows how to prove that if p implies q and q implies r, then p implies r. We accomplish that by showing that the negation is unsatisfiable. The command define-fun is used to define a macro (aka alias). In this example, conjecture is an alias for the conjecture we want to prove.

### Satisfiability and Validity

A formula F is valid if F always evaluates to true for any assignment of appropriate values to its uninterpreted function and constant symbols. A formula F is satisfiable if there is some assignment of appropriate values to its uninterpreted function and constant symbols under which F evaluates to true. Validity is about finding a proof of a statement; satisfiability is about finding a solution to a set of constraints. Consider a formula F with some uninterpreted constants, say a and b. We can ask whether F is valid, that is whether it is always true for any combination of values for a and b. If F is always true, then not F is always false, and then not F will not have any satisfying assignment; that is, not F is unsatisfiable. That is, F is valid precisely when not F is not satisfiable (is unsatisfiable). Alternately, F is satisfiable if and only if not F is not valid (is invalid). Z3 finds satisfying assignments (or report that there are none). To determine whether a formula F is valid, we ask Z3 whether not F is satisfiable. Thus, to check the deMorgan's law is valid (i.e., to prove it), we show its negation to be unsatisfiable.

## Cardinality Constraints

Logical disjunction `(or p q r)`

is true when at least one of the arguments `p`

, `q`

, `r`

is true. If you want to express that at least two of the arguments hold, then
it is possible to encode using formulas such as `(or (and p q) (and p r) (and q r))`

. However, you can also express the constraint directly using a *cardinality* constraint.

Dually, if at most one of the arguments should be true, you can express it as

## Pseudo Boolean Constraints

A generalization of cardinality constraints are Pseudo-Boolean formulas where the sum of Boolean variables with coefficients are bounded.

The sum `2p + q + 3r + 3s + 2t`

as at least `4`

.

The sum `2p + q + 3r + 3s + 2t`

as at most `5`

.

The sum `2p + q + 3r + 3s + 2t`

equals `5`

.

Cardinality, and Pseudo-Boolean, constraints can be much more succinct than CNF versions. Can you guess the secret formula? Hint: you can block clauses one by one for models of your failed guess, and see if you can find a pattern by counting the number of variables that are true and false.

## Unsatisfiable cores

You can created *named* assertions that are tracked when unsatisfiable core extraction is enabled. The unsatisfiable core is returned as a subset of named assertions that cannot be satisfied.