Introduction to First-Order Satisfiability
IA085: Satisfiability and Automated Reasoning
Martin Jonáš
FI MUNI, Spring 2024
Where are we?
Satisfiability modulo theories (SMT)
• x = 1 ∧ x = y + y ∧ y > 0
• is it satisfiable over reals?
• is it satisfiable over integers?
• is it satisfiable over integers represented by 8 bits?
• is it satisfiable over floating point numbers represented by 32 bits?
For next four lectures, we will be dealing mostly with quantifier-free formulas.
1 / 36
Applications
SMT solvers are widely used in practice
• planning
• scheduling
• verification of hardware
• compiler optimizations
• verification of software
• . . .
2 / 36
Applications
1 int x = read();
2 int y = read();
3 int z = read();
4 if (x > 10 && y != 0)
5 {
6 print(z / (x + y));
7 }
Contains division by zero precisely if the formula
x > 10 ∧ ¬(y = 0) ∧ x + y = 0
is satisfiable.
3 / 36
First-order logic
First-Order Logic
Propositional logic speaks only about atomic propositions
• are true or false
• have no internal structure
First-order logic speaks about objects, their properties and relations among them.
4 / 36
First-Order Logic
Propositional logic speaks only about atomic propositions
• are true or false
• have no internal structure
First-order logic speaks about objects, their properties and relations among them.
Examples
• ∃s. Human(s) ∧ Mortal(s).
• ∀s. Human(s) → Mortal(s).
• ∃x∃y. x < 5 ∧ y < 3 ∧ 2 · (x + y) > 20.
4 / 36
First-Order Logic
Propositional logic speaks only about atomic propositions
• are true or false
• have no internal structure
First-order logic speaks about objects, their properties and relations among them.
Examples
• ∃s. Human(s) ∧ Mortal(s).
• ∀s. Human(s) → Mortal(s).
• ∃x∃y. x < 5 ∧ y < 3 ∧ 2 · (x + y) > 20.
4 / 36
First-Order Logic
Propositional logic speaks only about atomic propositions
• are true or false
• have no internal structure
First-order logic speaks about objects, their properties and relations among them.
Examples
• ∃s. Human(s) ∧ Mortal(s).
• ∀s. Human(s) → Mortal(s).
• ∃x∃y. x < 5 ∧ y < 3 ∧ 2 · (x + y) > 20.
In addition to logical symbols, first-order formulas contain variables, constant
symbols, function symbols, and predicate symbols.
4 / 36
First-Order Logic – Syntax
Suppose we have
• a set ΣF = {f, g, . . .} of function symbols and
• a set ΣP = {R, S, . . .} of predicate symbols.
Each function symbol f and predicate symbol P has its arity ar(f) and ar(P).
Function symbols of arity 0 are called constants.
The set Σ = ΣF ∪ ΣP is called a signature.
Example
• ΣF = {+, −, 0, 1}
• ΣP = {=, ≤}
5 / 36
First-Order Logic – Syntax
(Σ-)Term
1. a variable – x, y, z, . . .
2. a function symbol applied to ar(f) terms – f(x), g(f(x), y), …
6 / 36
First-Order Logic – Syntax
(Σ-)Term
1. a variable – x, y, z, . . .
2. a function symbol applied to ar(f) terms – f(x), g(f(x), y), …
(Σ)-Literal
1. a predicate symbol applied to ar(P) terms – R(x), S(f(x), y), . . .
2. a negation of predicate symbol applied to ar(P) terms –
¬R(x), ¬S(f(x), y), . . .
6 / 36
First-Order Logic – Syntax
(Σ-)Term
1. a variable – x, y, z, . . .
2. a function symbol applied to ar(f) terms – f(x), g(f(x), y), …
(Σ)-Literal
1. a predicate symbol applied to ar(P) terms – R(x), S(f(x), y), . . .
2. a negation of predicate symbol applied to ar(P) terms –
¬R(x), ¬S(f(x), y), . . .
(Σ)-Formula
1. a Boolean combination of literals – (R(x) ∨ ¬R(y)) ∧ S(f(x), y), . . .
2. a quantifier applied to a formula – ∀x (R(x)) , . . ..
6 / 36
First-Order Logic – Syntactic Conventions and Terminology
Notation
• instead of +(r, s) write r + s (also for other infix function symbols)
• instead of ≤ (r, s) write r ≤ s (also for other infix predicate symbols)
• instead of 1() write 1 (also for other constants)
• instead of ∀x∀y(φ ∧ ψ) write ∀x∀y. φ ∧ ψ
Terminology
• an occurrence of a variable is free if it is not bound by a quantifier
• a formula without free occurrences of variables is closed or a sentence
7 / 36
First-Order Logic – Semantics
Is the following formula true?
∀x∃y. x < y ∧ y < x + 1
8 / 36
First-Order Logic – Semantics
Is the following formula true?
∀x∃y. x < y ∧ y < x + 1
It depends.
8 / 36
First-Order Logic – Semantics
Is the following formula true?
∀x∃y. x < y ∧ y < x + 1
It depends.
• What is the domain of x and y?
• What does the function symbol + mean?
• What does the predicate symbol < mean?
8 / 36
First-Order Logic – Semantics
Is the following formula true?
∀x∃y. x < y ∧ y < x + 1
It depends.
• What is the domain of x and y?
• What does the function symbol + mean?
• What does the predicate symbol < mean?
8 / 36
First-Order Logic – Semantics
Is the following formula true?
∀x∃y. x < y ∧ y < x + 1
It depends.
• What is the domain of x and y?
• What does the function symbol + mean?
• What does the predicate symbol < mean?
Meaning of these three things is given by a Σ-structure.
8 / 36
First-Order Logic – Structures
Σ-structure A
• determines the set of objects and behavior of functions/predicates
• a pair of
1. a non-empty set A called the universe,
2. a map (_)A
that
• to each f ∈ ΣF
assigns a function fA
: Aar(f)
→ A,
• to each R ∈ ΣP
\ {=} assigns a relation RA
⊆ Aar(R)
,
• we suppose that =A
is the identity relation.
9 / 36
First-Order Logic – Structure Examples
A =
(
A, (_)A
)
where
A = Z
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
10 / 36
First-Order Logic – Structure Examples
A =
(
A, (_)A
)
where
A = Z
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
B =
(
B, (_)B
)
where
B = {◦, •}
+B
(x, y) = y
<B
= {(◦, ◦), (•, ◦)}
1B
= •
10 / 36
First-Order Logic – Interpretation
The formulas can also contain free variables.
Valuation for a Σ-structure A = (A, (_)A)
• determines the values of the variables
• a map µ: Vars → A
Σ-interpretation
• a pair (A, µ) of a Σ-structure and a valuation
11 / 36
First-Order Logic – Evaluation
Given an interpretation I = (A, µ), we can evaluate
• each term t to a value t I
∈ A
• each formula φ to a value φ I
∈ {⊤, ⊥}
12 / 36
First-Order Logic – Evaluation
A =
(
Z, (_)A
)
where
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
13 / 36
First-Order Logic – Evaluation
A =
(
Z, (_)A
)
where
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
Given µ(x) = 1, µ(y) = 3:
• y + 1 (A,µ)
=
13 / 36
First-Order Logic – Evaluation
A =
(
Z, (_)A
)
where
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
Given µ(x) = 1, µ(y) = 3:
• y + 1 (A,µ)
= 4
• y + 1 < x (A,µ)
=
13 / 36
First-Order Logic – Evaluation
A =
(
Z, (_)A
)
where
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
Given µ(x) = 1, µ(y) = 3:
• y + 1 (A,µ)
= 4
• y + 1 < x (A,µ)
= ⊥
• (x < y) ∧ (y + 1 < x) (A,µ)
=
13 / 36
First-Order Logic – Evaluation
A =
(
Z, (_)A
)
where
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
Given µ(x) = 1, µ(y) = 3:
• y + 1 (A,µ)
= 4
• y + 1 < x (A,µ)
= ⊥
• (x < y) ∧ (y + 1 < x) (A,µ)
= ⊥
B =
(
{◦, •}, (_)B
)
where
+B
(x, y) = y
<B
= {(◦, ◦), (•, ◦)}
1B
= •
Given µ(x) = ◦, µ(y) = ◦:
• y + 1 (B,µ)
=
13 / 36
First-Order Logic – Evaluation
A =
(
Z, (_)A
)
where
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
Given µ(x) = 1, µ(y) = 3:
• y + 1 (A,µ)
= 4
• y + 1 < x (A,µ)
= ⊥
• (x < y) ∧ (y + 1 < x) (A,µ)
= ⊥
B =
(
{◦, •}, (_)B
)
where
+B
(x, y) = y
<B
= {(◦, ◦), (•, ◦)}
1B
= •
Given µ(x) = ◦, µ(y) = ◦:
• y + 1 (B,µ)
= •
• y + 1 < x (B,µ)
=
13 / 36
First-Order Logic – Evaluation
A =
(
Z, (_)A
)
where
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
Given µ(x) = 1, µ(y) = 3:
• y + 1 (A,µ)
= 4
• y + 1 < x (A,µ)
= ⊥
• (x < y) ∧ (y + 1 < x) (A,µ)
= ⊥
B =
(
{◦, •}, (_)B
)
where
+B
(x, y) = y
<B
= {(◦, ◦), (•, ◦)}
1B
= •
Given µ(x) = ◦, µ(y) = ◦:
• y + 1 (B,µ)
= •
• y + 1 < x (B,µ)
= ⊤
• (x < y) ∧ (y + 1 < x) (B,µ)
=
13 / 36
First-Order Logic – Evaluation
A =
(
Z, (_)A
)
where
+A
(x, y) = x + y
<A
= {(x, y) | x < y}
1A
= 1
Given µ(x) = 1, µ(y) = 3:
• y + 1 (A,µ)
= 4
• y + 1 < x (A,µ)
= ⊥
• (x < y) ∧ (y + 1 < x) (A,µ)
= ⊥
B =
(
{◦, •}, (_)B
)
where
+B
(x, y) = y
<B
= {(◦, ◦), (•, ◦)}
1B
= •
Given µ(x) = ◦, µ(y) = ◦:
• y + 1 (B,µ)
= •
• y + 1 < x (B,µ)
= ⊤
• (x < y) ∧ (y + 1 < x) (B,µ)
= ⊤
13 / 36
Models and Entailment
Interpretation I satisfies formula φ
• if φ I
= ⊤
• written I |= φ
14 / 36
Entailment and Validity
Formula φ entails formula ψ
• if every interpretation that satisfies φ also satisfies ψ
• written φ |= ψ
• example: f(x) = y ∧ x = z |= f(z) = y
• negative example: x < y ̸|= x + 1 < y + 1
Formula φ is valid
• if every interpretation satisfies φ
• written |= φ
• example: |= P(f(x)) ∨ ¬P(f(x))
• negative example: ̸|= x + 0 = x
15 / 36
First-Order Satisfiability
Definition
Formula φ is satisfiable if there is a Σ-interpretation (A, µ) such that (A, µ) |= φ.
16 / 36
First-Order Satisfiability
Definition
Formula φ is satisfiable if there is a Σ-interpretation (A, µ) such that (A, µ) |= φ.
Is formula (x < y) ∧ (y + 1 < x) satisfiable?
16 / 36
First-Order Satisfiability
Definition
Formula φ is satisfiable if there is a Σ-interpretation (A, µ) such that (A, µ) |= φ.
Is formula (x < y) ∧ (y + 1 < x) satisfiable? Yes.
16 / 36
First-Order Satisfiability
Definition
Formula φ is satisfiable if there is a Σ-interpretation (A, µ) such that (A, µ) |= φ.
Is formula (x < y) ∧ (y + 1 < x) satisfiable? Yes.
Solution
Pick a subset of Σ-structures in which we are interested.
This gives rise to the Satisfiability Modulo Theories
16 / 36
Satisfiability Modulo Theories (SMT)
Satisfiability Modulo Theories
Definition
A (Σ-)theory is a set of Σ-structures.
Definition
A formula φ is satisfiable modulo theory T if there is a Σ-interpretation (A, µ)
with A ∈ T such that (A, µ) |= φ.
17 / 36
Satisfiability Modulo Theories – Example
Consider the structure Z with the universe Z and the standard interpretation of
operations +, <, and 1.
The formula (x < y) ∧ (y + 1 < x) is unsatisfiable modulo theory T = {Z}.
The formula (x < y) ∧ (y < x + 2) is satisfiable modulo theory T = {Z}.
18 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
19 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
19 / 36
T-models
I = (A, µ) is T-model of φ
• if A ∈ T and φ I
= ⊤
• written I |=T φ
20 / 36
Entailment and Validity
φ T-entails ψ
• if every T-model of φ is also a T-model of ψ
• written φ |=T ψ
• example: x < y |=TLIA
x + 1 < y + 1
φ is T-valid
• if every I = (A, µ) with A ∈ T is a T-model of φ
• equivalently ⊤ |=T φ
• written |=T φ
• example: |=TLIA
x + 0 = x
21 / 36
Theories of interest
Logics in SMT-LIB
[https://smtlib.cs.uiowa.edu/logics.shtml] 22 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
23 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
23 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
23 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
• complexity of satisfiability of arbitrary formulas is in Ω(22n
) (Fischer, Rabin,
1974)
23 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
• complexity of satisfiability of arbitrary formulas is in Ω(22n
) (Fischer, Rabin,
1974)
• complexity of satisfiability of arbitrary formulas is in O(222kn
) (Oppen, 1978)
23 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
• complexity of satisfiability of arbitrary formulas is in Ω(22n
) (Fischer, Rabin,
1974)
• complexity of satisfiability of arbitrary formulas is in O(222kn
) (Oppen, 1978)
• satisfiability of quantifier-free formulas is NP-complete
23 / 36
Linear Integer Arithmetic (LIA)
• Σ = {0, 1, +, −, =, ≤}
• TLIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
• complexity of satisfiability of arbitrary formulas is in Ω(22n
) (Fischer, Rabin,
1974)
• complexity of satisfiability of arbitrary formulas is in O(222kn
) (Oppen, 1978)
• satisfiability of quantifier-free formulas is NP-complete
• satisfiability of conjunctions of literals is NP-complete
23 / 36
Linear Rational Arithmetic (LRA)
• Σ = {0, 1, +, −, =, ≤}
• TLRA is a set of a single structure with A = Q and the standard
interpretation of operations
24 / 36
Linear Rational Arithmetic (LRA)
• Σ = {0, 1, +, −, =, ≤}
• TLRA is a set of a single structure with A = Q and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
24 / 36
Linear Rational Arithmetic (LRA)
• Σ = {0, 1, +, −, =, ≤}
• TLRA is a set of a single structure with A = Q and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
24 / 36
Linear Rational Arithmetic (LRA)
• Σ = {0, 1, +, −, =, ≤}
• TLRA is a set of a single structure with A = Q and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
• complexity of satisfiability of arbitrary formulas is in Ω(2n) (Fischer, Rabin,
1974)
24 / 36
Linear Rational Arithmetic (LRA)
• Σ = {0, 1, +, −, =, ≤}
• TLRA is a set of a single structure with A = Q and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
• complexity of satisfiability of arbitrary formulas is in Ω(2n) (Fischer, Rabin,
1974)
• complexity of satisfiability of arbitrary formulas is in O(22kn
) (Ferrante,
Rackoff, 1975)
24 / 36
Linear Rational Arithmetic (LRA)
• Σ = {0, 1, +, −, =, ≤}
• TLRA is a set of a single structure with A = Q and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
• complexity of satisfiability of arbitrary formulas is in Ω(2n) (Fischer, Rabin,
1974)
• complexity of satisfiability of arbitrary formulas is in O(22kn
) (Ferrante,
Rackoff, 1975)
• satisfiability of quantifier-free formulas is NP-complete
24 / 36
Linear Rational Arithmetic (LRA)
• Σ = {0, 1, +, −, =, ≤}
• TLRA is a set of a single structure with A = Q and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x + y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable
• complexity of satisfiability of arbitrary formulas is in Ω(2n) (Fischer, Rabin,
1974)
• complexity of satisfiability of arbitrary formulas is in O(22kn
) (Ferrante,
Rackoff, 1975)
• satisfiability of quantifier-free formulas is NP-complete
• satisfiability of conjunctions of literals in P (Khachiyan, 1979) 24 / 36
Theory of Non-Linear Integer Arithmetic (NIA)
• Σ = {0, 1, +, −, ·, =, ≤}
• TNIA is a set of a single structure with A = Z and the standard interpretation
of operations
25 / 36
Theory of Non-Linear Integer Arithmetic (NIA)
• Σ = {0, 1, +, −, ·, =, ≤}
• TNIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x · y) ∧ (1 ≤ y)
25 / 36
Theory of Non-Linear Integer Arithmetic (NIA)
• Σ = {0, 1, +, −, ·, =, ≤}
• TNIA is a set of a single structure with A = Z and the standard interpretation
of operations
1 ≤ x ∧ (3 ≤ x · y) ∧ (1 ≤ y)
• satisfiability of conjunctions of quantifier-free formulas is undecidable
(Matiyasevich, 1971)
25 / 36
Non-Linear Real Arithmetic (NRA)
• Σ = {0, 1, +, −, ·, =, ≤}
• TNRA is a set of a single structure with A = R and the standard
interpretation of operations
26 / 36
Non-Linear Real Arithmetic (NRA)
• Σ = {0, 1, +, −, ·, =, ≤}
• TNRA is a set of a single structure with A = R and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x · y) ∧ (1 ≤ y)
26 / 36
Non-Linear Real Arithmetic (NRA)
• Σ = {0, 1, +, −, ·, =, ≤}
• TNRA is a set of a single structure with A = R and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x · y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable (Tarski, 1951)
26 / 36
Non-Linear Real Arithmetic (NRA)
• Σ = {0, 1, +, −, ·, =, ≤}
• TNRA is a set of a single structure with A = R and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x · y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable (Tarski, 1951)
• complexity of satisfiability of arbitrary formulas is in O(22kn
) (Collins, 1975)
26 / 36
Non-Linear Real Arithmetic (NRA)
• Σ = {0, 1, +, −, ·, =, ≤}
• TNRA is a set of a single structure with A = R and the standard
interpretation of operations
1 ≤ x ∧ (3 ≤ x · y) ∧ (1 ≤ y)
• satisfiability of arbitrary formulas is decidable (Tarski, 1951)
• complexity of satisfiability of arbitrary formulas is in O(22kn
) (Collins, 1975)
• complexity of satisfiability of conjunctions of literals in O(22kn
)
26 / 36
Arrays (A)
• Σ = {read, write, =}
• TA is a set of structures, where A is a set of arrays and elements and
– read(a, i) is interpreted as an element on index i of array a
– write(a, i, v) is interpreted as an array a after replacing element on index i by v
– equality is defined only for elements
27 / 36
Arrays (A)
• Σ = {read, write, =}
• TA is a set of structures, where A is a set of arrays and elements and
– read(a, i) is interpreted as an element on index i of array a
– write(a, i, v) is interpreted as an array a after replacing element on index i by v
– equality is defined only for elements
read(a, i) = u ∧ (read(a, i) = read(write(a, i, v), i))
27 / 36
Arrays (A)
• Σ = {read, write, =}
• TA is a set of structures, where A is a set of arrays and elements and
– read(a, i) is interpreted as an element on index i of array a
– write(a, i, v) is interpreted as an array a after replacing element on index i by v
– equality is defined only for elements
read(a, i) = u ∧ (read(a, i) = read(write(a, i, v), i))
• satisfiability of arbitrary formulas is undecidable
27 / 36
Arrays (A)
• Σ = {read, write, =}
• TA is a set of structures, where A is a set of arrays and elements and
– read(a, i) is interpreted as an element on index i of array a
– write(a, i, v) is interpreted as an array a after replacing element on index i by v
– equality is defined only for elements
read(a, i) = u ∧ (read(a, i) = read(write(a, i, v), i))
• satisfiability of arbitrary formulas is undecidable
• satisfiability of quantifier-free formulas is NP-complete
27 / 36
Arrays with Extensionality (AX)
• Σ = {read, write, =}
• TA is a set of structures where A is a set of arrays and elements and
– read(a, i) is interpreted as an element on index i of array a
– write(a, i, v) is interpreted as an array a after replacing element on index i by v
28 / 36
Arrays with Extensionality (AX)
• Σ = {read, write, =}
• TA is a set of structures where A is a set of arrays and elements and
– read(a, i) is interpreted as an element on index i of array a
– write(a, i, v) is interpreted as an array a after replacing element on index i by v
read(a, i) = u ∧ (b = write(a, i, v)) ∧ (a = b)
28 / 36
Arrays with Extensionality (AX)
• Σ = {read, write, =}
• TA is a set of structures where A is a set of arrays and elements and
– read(a, i) is interpreted as an element on index i of array a
– write(a, i, v) is interpreted as an array a after replacing element on index i by v
read(a, i) = u ∧ (b = write(a, i, v)) ∧ (a = b)
• satisfiability of arbitrary formulas is undecidable
28 / 36
Arrays with Extensionality (AX)
• Σ = {read, write, =}
• TA is a set of structures where A is a set of arrays and elements and
– read(a, i) is interpreted as an element on index i of array a
– write(a, i, v) is interpreted as an array a after replacing element on index i by v
read(a, i) = u ∧ (b = write(a, i, v)) ∧ (a = b)
• satisfiability of arbitrary formulas is undecidable
• satisfiability of quantifier-free formulas is NP-complete
28 / 36
Fixed-Size Bit-Vectors (BV)
• Σ = {+[k], ×[k], &[k], =, <u
[k], <s
[k] 1[k], 2[k]} and many more
• TBV is a set of structures where BV is a set of finite sequences of bits
(bit-vectors) and
– +[k] adds two sequences of k-bits representing unsigned integers and returns a
sequence of k-bits
– 1[k] is a sequence of k-bits that represents unsigned number 1
– . . .
29 / 36
Fixed-Size Bit-Vectors (BV)
• Σ = {+[k], ×[k], &[k], =, <u
[k], <s
[k] 1[k], 2[k]} and many more
• TBV is a set of structures where BV is a set of finite sequences of bits
(bit-vectors) and
– +[k] adds two sequences of k-bits representing unsigned integers and returns a
sequence of k-bits
– 1[k] is a sequence of k-bits that represents unsigned number 1
– . . .
x +[8] 2[8] <u
[8] x[8]
29 / 36
Fixed-Size Bit-Vectors (BV)
• Σ = {+[k], ×[k], &[k], =, <u
[k], <s
[k] 1[k], 2[k]} and many more
• TBV is a set of structures where BV is a set of finite sequences of bits
(bit-vectors) and
– +[k] adds two sequences of k-bits representing unsigned integers and returns a
sequence of k-bits
– 1[k] is a sequence of k-bits that represents unsigned number 1
– . . .
x +[8] 2[8] <u
[8] x[8]
• satisfiability of arbitrary formulas is PSPACE-complete
29 / 36
Fixed-Size Bit-Vectors (BV)
• Σ = {+[k], ×[k], &[k], =, <u
[k], <s
[k] 1[k], 2[k]} and many more
• TBV is a set of structures where BV is a set of finite sequences of bits
(bit-vectors) and
– +[k] adds two sequences of k-bits representing unsigned integers and returns a
sequence of k-bits
– 1[k] is a sequence of k-bits that represents unsigned number 1
– . . .
x +[8] 2[8] <u
[8] x[8]
• satisfiability of arbitrary formulas is PSPACE-complete
• satisfiability of quantifier-free formulas is NP-complete
29 / 36
Equality and Uninterpreted Functions (UF)
• Σ = {=, f, g, h, . . .}
• TUF is a set of all Σ-structures
30 / 36
Equality and Uninterpreted Functions (UF)
• Σ = {=, f, g, h, . . .}
• TUF is a set of all Σ-structures
x = v ∧ y = g(z) ∧ f(g(x)) ̸= f(y) ∧ z = v
30 / 36
Equality and Uninterpreted Functions (UF)
• Σ = {=, f, g, h, . . .}
• TUF is a set of all Σ-structures
x = v ∧ y = g(z) ∧ f(g(x)) ̸= f(y) ∧ z = v
• satisfiability of arbitrary formulas is undecidable
30 / 36
Equality and Uninterpreted Functions (UF)
• Σ = {=, f, g, h, . . .}
• TUF is a set of all Σ-structures
x = v ∧ y = g(z) ∧ f(g(x)) ̸= f(y) ∧ z = v
• satisfiability of arbitrary formulas is undecidable
• satisfiability of quantifier-free formulas is decidable (Ackermann, 1954)
30 / 36
Equality and Uninterpreted Functions (UF)
• Σ = {=, f, g, h, . . .}
• TUF is a set of all Σ-structures
x = v ∧ y = g(z) ∧ f(g(x)) ̸= f(y) ∧ z = v
• satisfiability of arbitrary formulas is undecidable
• satisfiability of quantifier-free formulas is decidable (Ackermann, 1954)
• satisfiability of quantifier-free formulas is NP-complete
30 / 36
Equality and Uninterpreted Functions (UF)
• Σ = {=, f, g, h, . . .}
• TUF is a set of all Σ-structures
x = v ∧ y = g(z) ∧ f(g(x)) ̸= f(y) ∧ z = v
• satisfiability of arbitrary formulas is undecidable
• satisfiability of quantifier-free formulas is decidable (Ackermann, 1954)
• satisfiability of quantifier-free formulas is NP-complete
• satisfiability of conjunctions of literals is in O(n · log(n))
30 / 36
More theories
• theory of strings (s1 ++ s2, len(s), substr(s, from, to), contains(s1, s2), . . .)
31 / 36
More theories
• theory of strings (s1 ++ s2, len(s), substr(s, from, to), contains(s1, s2), . . .)
• theory of lists,
31 / 36
More theories
• theory of strings (s1 ++ s2, len(s), substr(s, from, to), contains(s1, s2), . . .)
• theory of lists,
• theory of floating point numbers (IEEE-754),
31 / 36
More theories
• theory of strings (s1 ++ s2, len(s), substr(s, from, to), contains(s1, s2), . . .)
• theory of lists,
• theory of floating point numbers (IEEE-754),
• theory of recursive data structures,
31 / 36
More theories
• theory of strings (s1 ++ s2, len(s), substr(s, from, to), contains(s1, s2), . . .)
• theory of lists,
• theory of floating point numbers (IEEE-754),
• theory of recursive data structures,
• theory of groups,
31 / 36
More theories
• theory of strings (s1 ++ s2, len(s), substr(s, from, to), contains(s1, s2), . . .)
• theory of lists,
• theory of floating point numbers (IEEE-754),
• theory of recursive data structures,
• theory of groups,
• …
31 / 36
Standard view of theories
Theory: Standard Definitions
Definition
A (Σ-)theory is a set of closed Σ-formulas.
Definition
A formula φ is satisfiable modulo theory T if there is a Σ-interpretation I such
that
• I |= φ and
• I |= ψ for all ψ ∈ T
32 / 36
Two views of theories
Linear Natural Arithmetic
• Σ = {0, 1, +, =, ≤}
SMT definition
• T = {(N, (_)N)}, where (_)N is the obvious standard interpretation
Standard definition (Presburger axioms)
T = {∀x. ¬(0 = x + 1),
∀x∀y. x + 1 = y + 1 → x = y,
∀x. x + 0 = x,
∀x∀y. x + (y + 1) = (x + y) + 1} ∪
{(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀yP(y) | P is a formula with free variable x}
33 / 36
Two views of theories
More examples
• The theory of uninterpreted functions with equality is TUF =
34 / 36
Two views of theories
More examples
• The theory of uninterpreted functions with equality is TUF =
34 / 36
Two views of theories
More examples
• The theory of uninterpreted functions with equality is TUF = ∅
34 / 36
Two views of theories
More examples
• The theory of uninterpreted functions with equality is TUF = ∅
• The axioms of theory of arrays (McCarthy):
TA = { ∀a, i, j. (i = j → read(a, i) = read(a, j)),
∀a, v, i, j. (i = j → read(write(a, i, v), j) = v),
∀a, v, i, j. (i ̸= j → read(write(a, i, v), j) = read(a, j))}
34 / 36
Two views of theories
These two views are equivalent
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
• set of axioms ⇒ the set of Σ-structures that satisfy all the axioms
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
• set of axioms ⇒ the set of Σ-structures that satisfy all the axioms
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
• set of axioms ⇒ the set of Σ-structures that satisfy all the axioms
Sometimes, one view is better
• A set of structures satisfying axioms of Peano arithmetic is not easily
describable.
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
• set of axioms ⇒ the set of Σ-structures that satisfy all the axioms
Sometimes, one view is better
• A set of structures satisfying axioms of Peano arithmetic is not easily
describable.
• A set of axioms for NRA is infinite and complicated.
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
• set of axioms ⇒ the set of Σ-structures that satisfy all the axioms
Sometimes, one view is better
• A set of structures satisfying axioms of Peano arithmetic is not easily
describable.
• A set of axioms for NRA is infinite and complicated.
• A set of axioms for NIA is not recursive.
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
• set of axioms ⇒ the set of Σ-structures that satisfy all the axioms
Sometimes, one view is better
• A set of structures satisfying axioms of Peano arithmetic is not easily
describable.
• A set of axioms for NRA is infinite and complicated.
• A set of axioms for NIA is not recursive.
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
• set of axioms ⇒ the set of Σ-structures that satisfy all the axioms
Sometimes, one view is better
• A set of structures satisfying axioms of Peano arithmetic is not easily
describable.
• A set of axioms for NRA is infinite and complicated.
• A set of axioms for NIA is not recursive. ( , 1931)
35 / 36
Two views of theories
These two views are equivalent
• set of Σ-structures ⇒ the set of formulas that are true in all these structures
• set of axioms ⇒ the set of Σ-structures that satisfy all the axioms
Sometimes, one view is better
• A set of structures satisfying axioms of Peano arithmetic is not easily
describable.
• A set of axioms for NRA is infinite and complicated.
• A set of axioms for NIA is not recursive. (Gödel, 1931)
35 / 36
Next time
• algorithms solving SMT
• CDCL(T) algorithm
36 / 36