<p>I can think of 2 straight forward approaches</p>

<ol>
<li>Directly add <span class="math-container">$\forall xy (x &lt; y \Rightarrow f(x) &lt; f(y))$</span>.</li>
<li>Or Akcermannize the problem and add these as axioms for all pairs of terms.</li>
</ol>

CC BY-SA 4.0
2019-10-15T13:48:15.313Z
So, if I split each variable and function into its own class, do classes that fulfill criteria 1 become merged? Similar to uninterpreted functions theory
C. Bowers
CC BY-SA 4.0
2019-10-16T19:51:37.153Z
I don't know what you mean by classes or merging. These are just additional axioms. In version 2 you just add them after you've Ackermannized everything
Mikolas
CC BY-SA 4.0
2019-10-14T11:54:28.147Z
2019-10-14T11:54:28.147Z
Mikolas
<p>I am attempting to solve a less-than theory within an SMT paradigm that involves variables assigned to reals and assumes that all the functions used in the theory are monotonic. The theory's signature has the terms denoted as T and the formulas are denoted as φ. The syntax is given as follows:</p>

<p><span class="math-container">$$T = x \mid f(T) \tag{1}$$</span>
<span class="math-container">$$φ = T &lt; T \mid ¬φ \mid φ ∧ φ \mid φ ∨ φ \tag{2}$$</span></p>

<p>An example formula in this domain is:</p>

<p><span class="math-container">$$(x &lt; y) ∧ (y &lt; z) ∧ ((f(z) &lt; f(y)) ∨ (f(x) &lt; f(z)))$$</span></p>

<p>How would I begin thinking about how to encode a general formula within the less-than theory as a SAT problem? What is the decision process and encoding algorithm? </p>

<sat><model-checking><formal-methods>
SMT solving with less-than theory and monotonic functions
C. Bowers
# SMT solving with less-than theory and monotonic functions

(Asked by: username_0 on 2019-10-13)

I am attempting to solve a less-than theory within an SMT paradigm that involves variables assigned to reals and assumes that all the functions used in the theory are monotonic. The theory's signature has the terms denoted as T and the formulas are denoted as φ. The syntax is given as follows:

$$T = x \mid f(T) \tag{1}$$
$$φ = T < T \mid ¬φ \mid φ ∧ φ \mid φ ∨ φ \tag{2}$$

An example formula in this domain is:

$$(x < y) ∧ (y < z) ∧ ((f(z) < f(y)) ∨ (f(x) < f(z)))$$

How would I begin thinking about how to encode a general formula within the less-than theory as a SAT problem? What is the decision process and encoding algorithm?

**Tags:** sat, model-checking, formal-methods


---

## 1 answers

### Answer by username_1 on 2019-10-14. Score: 1

I can think of 2 straight forward approaches

1. Directly add $\forall xy (x < y \Rightarrow f(x) < f(y))$.
2. Or Akcermannize the problem and add these as axioms for all pairs of terms.

> **Comments:**
> **username_0**: So, if I split each variable and function into its own class, do classes that fulfill criteria 1 become merged? Similar to uninterpreted functions theory  
> **username_1**: I don't know what you mean by classes or merging. These are just additional axioms. In version 2 you just add them after you've Ackermannized everything  

---

