6
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

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.
Improve this answer
$\endgroup$
2
  • $\begingroup$ 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 $\endgroup$
    – C. Bowers
    Oct 15, 2019 at 13:48
  • $\begingroup$ 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 $\endgroup$
    – Mikolas
    Oct 16, 2019 at 19:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.