<p>I'm currently investigating a family of temporal relations called 'Ordered Horn' ($OH$ for short). This class was introduced in 'Reasoning about Temporal Relations: A Maximal Tractable Subclass of Allen's Interval Algebra' by B. Nebel and H.J. Bürckert. Following this paper, we define an <em>OH clause</em> as a formula over $\mathbb{N}^k$ of the form:</p>

<blockquote>
  <p>$F_{H,R}(x_1,\ldots,x_k) = \wedge_{(i,j) \in E(H)} (x_i = x_j) \Rightarrow (x_p R x_q)$,</p>
  
  <p>for a given graph $H$ on $[k]$ and a relation $R \in \{=,\leq,\neq\}$.</p>
</blockquote>

<p>An <em>OH relation</em> is then a conjunction of OH clauses. The authors state in Theorem 5 of the paper that the satisfiability of an OH relation can be decided in polynomial time, but the algorithm doesn't seem 'self-contained' as it relies on a generic algorithm for propositional Horn theories.</p>

<p>In relation to a problem I'm currently studying, such a self-contained algorithm seems desirable but it's unclear to me whether it is possible. To tell the truth, I have an algorithm for a subclass called <em>Restricted Ordered Horn</em> (containing the relations expressible using clauses without $\neq$ in the rhs) but unfortunately it can't be adapted to the full $OH$ class.</p>

CC BY-SA 3.0
2014-04-13T17:52:41.947Z
Isn't enough to replace all pairs $(x_i\; R\; x_j)$ with $3*k^2$ new variables? (e.g. $x_1 = x_2$ becomes $y_{x_1 = x_2}$, $x_1 \neq x_2$ becomes $y_{x_1 \neq x_2}$ ...). Then you can translate $F_{H,R}$ to a 2CNF formula because $y_i \Rightarrow y_j$ becomes $\neg y_j \lor y_i$, and solve it in polynomial time. But probably there is something I'm missing regarding temporal relations (perhaps you also want consistency among relations e.g. $x_i = x_j \Rightarrow x_i \neq x_j)$?) .
Marzio De Biasi
CC BY-SA 3.0
2014-04-13T17:55:43.727Z
Um, you may be right, however I expect the 'difficulty' of the problem to be caused by the possible overlap between the lhs and the rhs of an OH clause. By the way, please note that the lhs can be more conveniently expressed by a partition instead of a graph, which suggests a more natural (?) notation $F_{P,R}$ with $P$ a partition of a subset of the variable set. I prefer this second formulation personnally, although it doesn't seem standard practice (sorry for the unintentional pun...)
NisaiVloot
<sat><proofs><temporal-logic>
A self-contained proof that OrdHorn relations are tractable?
NisaiVloot
# A self-contained proof that OrdHorn relations are tractable?

(Asked by: username_0 on 2014-04-13)

I'm currently investigating a family of temporal relations called 'Ordered Horn' ($OH$ for short). This class was introduced in 'Reasoning about Temporal Relations: A Maximal Tractable Subclass of Allen's Interval Algebra' by B. Nebel and H.J. Bürckert. Following this paper, we define an *OH clause* as a formula over $\mathbb{N}^k$ of the form:

> $F\_{H,R}(x\_1,\ldots,x\_k) = \wedge\_{(i,j) \in E(H)} (x\_i = x\_j) \Rightarrow (x\_p R x\_q)$,
>
> for a given graph $H$ on $[k]$ and a relation $R \in \{=,\leq,\neq\}$.

An *OH relation* is then a conjunction of OH clauses. The authors state in Theorem 5 of the paper that the satisfiability of an OH relation can be decided in polynomial time, but the algorithm doesn't seem 'self-contained' as it relies on a generic algorithm for propositional Horn theories.

In relation to a problem I'm currently studying, such a self-contained algorithm seems desirable but it's unclear to me whether it is possible. To tell the truth, I have an algorithm for a subclass called *Restricted Ordered Horn* (containing the relations expressible using clauses without $\neq$ in the rhs) but unfortunately it can't be adapted to the full $OH$ class.

**Tags:** sat, proofs, temporal-logic

> **Comments:**
> **username_1**: Isn't enough to replace all pairs $(x_i\; R\; x_j)$ with $3*k^2$ new variables? (e.g. $x_1 = x_2$ becomes $y_{x_1 = x_2}$, $x_1 \neq x_2$ becomes $y_{x_1 \neq x_2}$ ...). Then you can translate $F_{H,R}$ to a 2CNF formula because $y_i \Rightarrow y_j$ becomes $\neg y_j \lor y_i$, and solve it in polynomial time. But probably there is something I'm missing regarding temporal relations (perhaps you also want consistency among relations e.g. $x_i = x_j \Rightarrow x_i \neq x_j)$?) .  
> **username_0**: Um, you may be right, however I expect the 'difficulty' of the problem to be caused by the possible overlap between the lhs and the rhs of an OH clause. By the way, please note that the lhs can be more conveniently expressed by a partition instead of a graph, which suggests a more natural (?) notation $F_{P,R}$ with $P$ a partition of a subset of the variable set. I prefer this second formulation personnally, although it doesn't seem standard practice (sorry for the unintentional pun...)  

---

## 0 answers

