# Temporal Logic for Social Networks

Vitor Machado Electronic address<EMAIL_ADDRESS>System Engineering and
Computer Science Program
Federal University of Rio de Janeiro  Mario Benevides Electronic address:
<EMAIL_ADDRESS>Computing Institute
Fluminense Federal University

###### Abstract

This paper introduces a logic with a class of social network models that is
based on standard Linear Temporal Logic (LTL), leveraging the power of
existing model checkers for the analysis of social networks. We provide a
short literature overview, and then define our logic and its axiomatization,
present some simple motivational examples of both models and formulas, and
show its soundness and completeness via a translation into propositional
formulas. Lastly, we briefly discuss model checking and time complexity
analysis.

##  1 Introduction

Social networks are a growing topic of study since the Internet social network
services boom starting in the late 1990’s with networks such as Friendster,
MySpace, LinkedIn, and others, and more recently Facebook. These services
allow people from all over the world to interact in meaningful ways, and as
such, have gained tremendous importance in popular culture in recent years.
They also impose some challenges, such as the spreading of false information,
usually referred to as “fake news”.

In a broader sense, these networks are commonly defined by a set of entities
(individuals, communities or societies), relations between pairs of entities,
and a set of social interactions. For instance, in Facebook, an entity is a
person, user of the service; the relations between pairs of entities are the
friendship relations and the social interactions are posts which appear on the
user’s timeline.

Our goal in this paper is to develop a logic based on LTL, denoted LTL-SN for
social network models without unadoption. Semantics are standard LTL, but we
are interested in models with social network properties of adoption, where an
agent adopts the behavior when the majority of its friends have the behavior.

The roadmap is as follows: In the following subsection we briefly go over some
of the literature that inspired or served as a basis for this work, providing
an overview of the past and current tendencies in the study social networks
with such frameworks. In chapter 2 we introduce the language and its
semantics, present some simple examples of model evolution and formulas, and
in chapter 3 we present some important definitions that lead on to the
axiomatization and finally its soundness and completeness proofs in chapter 4.
In chapter 5 we briefly discuss model checking and its time complexity, and
then present our closing words and future works in chapter 6.

###  1.1 Literature overview

Papers [6, 10], seminal works in social networks theory, deal with how a group
of agents should reach consensus by assessing the probabilities that each
agent assigns to a given proposition, and that informed disagreements are
therefore irrational behavior.

A threshold-model is presented in [1, 11], in which nodes influenced by their
neighbours can adopt one out of several alternatives. It focuses on
establishing conditions for adoption of a “product” by a node, and whether the
process has a unique outcome or not, or an unavoidable one. Nodes have
neighbours and are always aware of their product adoptions. Nodes have a
threshold $\theta$, and will adopt a product if more than $\theta$ of its
neighbours have adopted or not. The paper focuses strictly on these dynamics
and outcome conditions, and does not provide a logic formalism.

In [11] a different approach to threshold models is taken by constructing the
dynamics using action models and product update. The paper proposes an action
model approach to the updates, which works by applying the product between the
network graph and a graph that encodes the decision rules, and is uniformly
followed by all agents.

The paper [13] investigates the phenomenon of peer pressure, by introducing a
model where a person’s preferences are changed in response to the preferences
of a “peer group”. Relationships among agents are defined with the “facebook
logic” (symmetric relation of “friendship”, $\sim_{w}$, in a state $w$).

Private and public opinions are considered under the dynamics of social
influence in [4]. It provides rules for “strong” and “weak” influence, and
also rules for when an agent will express its true inner opinions or a
different external opinion. Agents are capable of evolving their epistemic
knowledge to infer the inner opinions of others, by discarding states which
are contradictory to the rules of social influence.

In [2] a “minimal” threshold-model based logic is presented, in the sense that
it does not use static modalities or hybrid logic for its diffusion process.
The authors go on to introduce an epistemic version of this logic, where
agents must have sufficient information about the behaviors of their
neighbours before adopting the behavior, as standard in epistemic logics. This
framework serves as the main inspiration for the work we present here.

##  2 Language and semantics

In this section we present the language of LTL-SN, define certain properties
of its models and its semantics.

######  Definition 1 (Language).

The language of LTL-SN is given by the following BNF:

$\varphi\vcentcolon=\top\mid
N_{ab}\mid\beta_{a}\mid\neg\varphi\mid\varphi_{1}\land\varphi_{2}\mid
X\varphi\mid\varphi_{1}U\varphi_{2}$

where $a,b\in\mathcal{A}$,

We use the standard abbreviations $\bot\equiv\neg\top$,
$\varphi\lor\phi\equiv\neg(\neg\varphi\land\neg\phi)$,
$\varphi\rightarrow\phi\equiv\neg(\varphi\land\neg\phi)$, $F\varphi\equiv\top
U\varphi$ and $G\varphi\equiv\neg F\neg\varphi$.

######  Definition 2 (Model).

A model is a tuple ${\cal M}=(\mathcal{A},N,\theta,I)$, where

  * •

$\mathcal{A}$ is a finite set of agents;

  * •

$N$ is a neighborhood function $N:\mathcal{A}\mapsto 2^{\mathcal{A}}$ such
that $N$ is irreflexive, serial and symmetric;

  * •

$\theta\in[0,1]$ is a uniform adoption threshold;

  * •

$I$ is an initial behavior set;

######  Definition 3 (Relation $\leq$).

Let $\leq$ be the binary relation over $2^{\mathcal{A}}\times
2^{\mathcal{A}}$, where

$B\leq B^{\prime}\ \text{iff}\
B^{\prime}=B\cup\left\\{a\in\mathcal{A}:\frac{\lvert N(a)\cap B\rvert}{\lvert
N(a)\rvert}>\theta\right\\}$

######  Definition 4 (Behaviors).

$\mathcal{B}\subseteq 2^{\mathcal{A}}$ is the set of behavior sets.

######  Definition 5 (Path on $\mathcal{M}$).

We define a path $b=b_{0},b_{1},b_{2},\ldots$ on a model
$\mathcal{M}=(\mathcal{A},N,\theta,I)$ to be such that $b_{0}=I$ and
$b_{i}\leq b_{i+1}$.

######  Lemma 1 (Path uniqueness).

There is exactly one path $b$ such that $b_{0}=I$.

###### Proof.

Follows directly from the fact that for any $b_{i}$ the relation $\leq$
defines strictly one $b_{i+1}$ such that $b_{i}\leq b_{i+1}$. ∎

Given lemma 1, we can define satisfaction for a model directly over paths.

######  Definition 6 (Satisfaction).

Given a model $\mathcal{M}=(\mathcal{A},N,\theta,I)$ and its path $b$. The
notion of satisfaction of formulas in $\mathcal{M}$ at a position $i$ is
defined as follows:

$\begin{array}[]{lll}\mathcal{M},i\models\beta_{a}&\text{iff}&a\in b_{i}\\\
\mathcal{M},i\models N_{ax}&\text{iff}&x\in N_{a}\\\
\mathcal{M},i\models\neg\varphi&\text{iff}&\mathcal{M},i\not\models\varphi\\\
\mathcal{M},i\models\varphi_{1}\land\varphi_{2}&\text{iff}&\mathcal{M},i\models\varphi_{1}\
\text{and}\ \mathcal{M},i\models\varphi_{2}\\\ \mathcal{M},i\models
X\varphi&\text{iff}&\mathcal{M},i+1\models\varphi\\\
\mathcal{M},i\models\varphi U\psi&\text{iff}&\text{there exists a}\ n\geq 0\
\text{such that}\\\ &&\mathcal{M},i+n\models\psi\ \text{and}\
\mathcal{M},i+j\models\varphi\ \text{for all}\ 0\leq j<n\end{array}$

All LTL operators, plus propositional operators $N_{ax}$ and $\beta_{a}$
defined in a standard way.

######  Definition 7 (Validity).

$\models\varphi$ iff $\mathcal{M},i\models\varphi$ for all models
$\mathcal{M}$ and positions $i$.

###  2.1 Examples

In figure 1 the behavior starts with agent $a$, and spreads through the entire
network, while in figure 2 a slightly different network setting (agents $d$
and $e$ are related) creates a “cluster” that resists the behavior.

Notice the formula
$(N_{bd}\land\beta_{b})\lor(N_{fd}\land\beta_{f})\rightarrow X\beta_{d}$ holds
in both of them (though vacuously in figure 2), and that it determines how
agent $d$ is able to incorporate the behavior itself. A generalization of
formulas like this one will be used in the axiomatization present in section
3.

For an example of an Until formula, consider $\neg(b_{d}\land b_{e}\land
b_{f})Ub_{d}$. It holds in figure 1, and expresses the fact that agent $d$
will not adhere to the behavior until one of its friends does. Notice it does
not hold in figure 2 because $d$ never gets to incorporate the behavior.
Considering the previous statement, it is easy to see that, for instance,
$G\neg\beta_{d}$ holds only in figure 2.

ptptaptbptcptdpteptfptptptptptptpt

ptptaptbptcptdpteptfptptptptptptpt

ptptaptbptcptdpteptfptptptptptptpt

ptptaptbptcptdpteptfptptptptptptpt

ptptaptbptcptdpteptfptptptptptptpt

Figure 1: This figure presents a social network (with $\theta=1/3$) with some
agents and the evolution of a behavior. Nodes are agents, and the edges
represent the relation between them. Each figure, ordered from left to right
and top to bottom, represents a distinct position as the network evolves. The
behavior eventually dominates the network.

ptptaptbptcptdpteptfptptptptptptptpt

ptptaptbptcptdpteptfptptptptptptptpt

Figure 2: Propagation of the behavior is stopped by a cluster of agents
($\theta=1/3$).

##  3 Axioms for the LTL-SN system

In this section the axioms of LTL-SN are presented. This formalism is based on
reduction axioms, and this strategy allows us to ultimately reduce formulas
into propositional logic. However before we can do that, we need to define a
few abbreviations and enunciate some useful properties.

First, we will define the “Majority” abbreviation, just as is defined in [2].
This formula determines whether an agent will adopt the behavior in the next
position of the path, because it holds when a fraction of at least $\theta$ of
its neighbors have already adopted the behavior.

######  Definition 8 (Majority).

An abbreviation representing “majority”:

$\beta_{N(a)\geq\theta}\coloneqq\bigvee\limits_{\mathcal{G}\subseteq\mathcal{N}\subseteq\mathcal{A}:\frac{\lvert\mathcal{G}\rvert}{\lvert\mathcal{N}\rvert}\geq\theta}\left(\bigwedge\limits_{b\in\mathcal{N}}N_{ab}\land\bigwedge\limits_{b\not\in\mathcal{N}}\neg
N_{ab}\land\bigwedge\limits_{b\in\mathcal{G}}\beta_{b}\right)$

We also define an expansion that is equivalent to the Until operator, and
demonstrate that both are indeed semantically equivalent. This expansion is a
key part of the reduction axiomatization.

######  Definition 9 (Until expansion).

Let $\varphi U\psi$ be a formula. We define its Until expansion steps as

$\displaystyle u^{0}(\varphi U\psi)$ $\displaystyle\coloneqq\psi$
$\displaystyle u^{i}(\varphi U\psi)$ $\displaystyle\coloneqq(\varphi\land
Xu^{i-1})$

Then, its Until expansion $EXP_{U}(\varphi U\psi)$ in a model with agent set
$\mathcal{A}$ is defined as

$EXP_{U}(\varphi U\psi)\coloneqq\bigvee\limits_{0\leq
i\leq\lvert\mathcal{A}\rvert}u^{i}(\varphi U\psi)$

Before we can show equivalence of the entire Until expansion, we demonstrate
that its first $n$ steps are equivalent to the Until operator if and only if
the right-hand side holds before the next $n$ positions (or vacuously never at
all). After that, we also determine that the longest distance from the current
position at which this can happen has to be less than
$\lvert\mathcal{A}\rvert$ positions ahead. With both of these, we are able to
prove equivalence of the complete Until expansion.

######  Lemma 2 (Until expansion step satisfaction).

$\mathcal{M},i\models u^{n}(\varphi U\psi)$ if and only if
$\mathcal{M},i+n\models\psi$ and $\mathcal{M},i+j\models\varphi$ for all
$0\leq j<n$.

###### Proof.

We will abbreviate $u^{n}(\varphi U\psi)$ as $u^{n}$ for this proof. The proof
goes by induction on $n$.

Base case ($n=0$):

It is trivial to see that $\mathcal{M},i\models u^{0}$ if and only if
$\mathcal{M},i\models\psi$, and there is no $j$ such that $0\leq j<n$.

Induction hypothesis ($n=k$):

$\mathcal{M},i\models u^{k}$ if and only if $\mathcal{M},i+k\models\psi$, and
$\mathcal{M},i+j\models\varphi$ for all $0\leq j<k$.

Induction step ($n=k+1$):

Assume $\mathcal{M},i\models u^{k+1}$.

By definition we have that $\mathcal{M},i\models\varphi\land Xu^{k}$, if and
only if $\mathcal{M},i\models\varphi$ and $\mathcal{M},i\models Xu^{k}$.
$\mathcal{M},i\models Xu^{k}$ if and only if $\mathcal{M},i+1\models u^{k}$.

Without loss of generality, we can rename $i$ to $i+1$ in the induction
hypothesis, and then we have $\mathcal{M},i+1\models u^{k}$ if and only if
$\mathcal{M},i+1+k\models\psi$, and $\mathcal{M},i+1+j\models\varphi$ for all
$0\leq j<k$.

$\mathcal{M},i+1+j\models\varphi$ for all $0\leq j<k$ and
$\mathcal{M},i\models\varphi$ can be rewritten as
$\mathcal{M},i+j\models\varphi$ for all $0\leq j<k+1$.

Therefore we are able to conclude that $\mathcal{M},i+(k+1)\models\psi$ and
$\mathcal{M},i+j\models\varphi$ for all $0\leq j<k+1$, and that finishes our
proof. ∎

######  Lemma 3 (Fixed-point).

Let $b=b_{0},b_{1},b_{2},\ldots,b_{n}$ be a path. For some
$i<\lvert\mathcal{A}\rvert$ a fixed-point $b_{i}=b_{i+1}$ is reached.

###### Proof.

This follows directly from the fact that $\mathcal{A}$ is finite and
$b_{i}\subseteq b_{i+1}$ for all $i$ by definition. The slowest possible
diffusion scenario is where $\lvert b_{0}\rvert=1$ and only one agent adopts
the behavior per position on the path until the fixed-point is reached. It
follows directly that the fixed-point will have to be reached for some
$i<\lvert\mathcal{A}\rvert$. ∎

######  Lemma 4 (Until expansion soundness).

$\models\varphi U\psi\leftrightarrow EXP_{U}(\varphi U\psi)$

###### Proof.

By definition, $EXP_{U}(\varphi U\psi)=u^{0}(\varphi U\psi)\lor u^{1}(\varphi
U\psi)\lor\ldots\lor u^{\lvert\mathcal{A}\rvert}(\varphi U\psi)$.

For any model $\mathcal{M}$ and position $j$, by lemma 2 we know that a term
$u^{i}$ holds if and only if $\psi$ holds in position $j+i$. By lemma 3 we
know that if $\varphi U\psi$ holds, $\psi$ must hold at some position $i$ such
that $0\leq j+i\leq\lvert\mathcal{A}\rvert+j$. Therefore $\models\varphi
U\psi$ if and only if $\models EXP_{U}(\varphi U\psi)$. ∎

Network axioms
---
$\neg N_{aa}$ | Irreflexivity
$N_{ab}\leftrightarrow N_{ba}$ | Symmetry
$\bigvee\limits_{b\in\mathcal{A}}N_{ab}$ | Seriality
Reduction axioms
$XN_{ab}\leftrightarrow N_{ab}$ | Red.Ax.$X$.$N$
$X\beta_{a}\leftrightarrow\beta_{a}\lor\beta_{N(a)}\geq\theta$ | Red.Ax.$X$.$\beta$
$\varphi U\psi\leftrightarrow EXP_{U}(\varphi U\psi)$ | Red.Ax.$U$
LTL axioms
All classical propositional tautologies |
$G(\varphi\rightarrow\psi)\rightarrow(G\varphi\rightarrow G\psi)$ | A1
$\neg X\varphi\leftrightarrow X\neg\varphi$ | A2
$X(\varphi\rightarrow\psi)\rightarrow(X\varphi\rightarrow X\psi)$ | A3
$G(\varphi\rightarrow X\varphi)\rightarrow(\varphi\rightarrow G\varphi)$ | A4
$(\varphi U\psi)\leftrightarrow\psi\lor(\varphi\land X(\varphi U\psi))$ | A5
$(\varphi U\psi)\rightarrow F\psi$ | A6
$\varphi U(\psi_{1}\lor\psi_{2})\leftrightarrow\varphi U\psi_{1}\lor\varphi U\psi_{2}$ | A7
$X(\varphi\land\psi)\leftrightarrow X\varphi\land X\psi$ | A8
$\displaystyle{\frac{\varphi\qquad\varphi\rightarrow\psi}{\psi}}$ | MP
$\displaystyle{\frac{\vdash\varphi}{\vdash G\varphi}}$ | NG
$\displaystyle{\frac{\vdash\varphi}{\vdash X\varphi}}$ | NX
Table 1: LTL-SN axioms.

LTL axioms are as seen on [5]. Notice that for completeness of this particular
class of models, only axioms $A2$, $A3$, $A8$ and the rules of inference $MP$
and $NX$ were used. The others were kept merely for reference.

######  Proposition 1 (Next rule).

The following inference rule is admissible:

$\displaystyle{\frac{\vdash\phi\leftrightarrow\psi}{\vdash
X\phi\leftrightarrow X\psi}}$

######  Proposition 2 (Replacement of equivalents).

If $\vdash\phi_{1}\leftrightarrow\phi_{2}$, then
$\vdash[\phi_{1}/\psi]\chi\leftrightarrow[\phi_{2}/\psi]\chi$.

The proof of proposition 1 follows straightforward from axiom A3 and inference
rules NX and MP. The proof of proposition 2 follows by induction on the
construction of $\chi$. These proofs are rather standard in LTL literature
[3].

##  4 Soundness and completeness

Since the formulas of LTL-SN are evaluated over conventional LTL paths (or
“flows of time” [8, 12]), all standard LTL axioms are also sound in this
logic.

######  Lemma 5 (Soundness).

Let $\mathcal{M}$ be an arbitrary LTL-SN model and $B\in\mathcal{B}$ a
behavior set.

###### Proof.

Consider each case:

  * •

All network axioms follow directly from definition 2;

  * •

$\mathcal{M},i\models XN_{ab}\leftrightarrow N_{ab}$ follows directly from the
fact that $\leq$ never alters the network structure;

  * •

$\mathcal{M},i\models\varphi U\psi\leftrightarrow EXP_{U}(\varphi U\psi)$
follows directly from lemma 4;

  * •

For $\mathcal{M},i\models
X\beta_{a}\leftrightarrow\beta_{a}\lor\beta_{N(a)}\geq\theta$, consider
$B=b_{i}$ and a $B^{\prime}$ such that $B\leq B^{\prime}$.

$\mathcal{M},i\models X\beta_{a}$ iff $\mathcal{M},i+1\models\beta_{a}$ iff
$a\in B^{\prime}=B\cup\left\\{b\in\mathcal{A}:\frac{\lvert N(b)\cap
B\rvert}{\lvert N(b)\rvert}>\theta\right\\}$ iff
$\mathcal{M},i\models\beta_{a}$ or $a\in\left\\{b\in\mathcal{A}:\frac{\lvert
N(b)\cap B\rvert}{\lvert N(b)\rvert}>\theta\right\\}$.

It can be shown that the large disjunct in definition 8 is satisfied iff
$a\in\left\\{b\in\mathcal{A}:\frac{\lvert N(b)\cap B\rvert}{\lvert
N(b)\rvert}>\theta\right\\}$ just as in [2].

Hence $\mathcal{M},i\models X\beta_{a}$ iff $\mathcal{M},i\models\beta_{a}$ or
$\mathcal{M},i\models\beta_{N(A)\geq\theta}$.

∎

###  4.1 Completeness

The strategy for this completeness proof is a two-step translation of LTL-SN
formulas into propositional formulas. The first step replaces Until operators,
and the second step replaces Next operators. The proofs of equivalence of each
step goes by induction.

######  Definition 10 (Until Translation).

$\displaystyle t_{u}(N_{ab})$ $\displaystyle=N_{ab}$ $\displaystyle
t_{u}(\beta_{a})$ $\displaystyle=\beta_{a}$ $\displaystyle
t_{u}(\varphi\land\psi)$ $\displaystyle=t_{u}(\varphi)\land t_{u}(\psi)$
$\displaystyle t_{u}(\neg\varphi)$ $\displaystyle=\neg t_{u}(\varphi)$
$\displaystyle t_{u}(X\varphi)$ $\displaystyle=Xt_{u}(\varphi)$ $\displaystyle
t_{u}(\varphi U\psi)$ $\displaystyle=t_{u}(EXP_{U}(\varphi U\psi))$

Next lemma assures that every formula is equivalent to another formula without
any occurrence of the $until$ operator.

######  Lemma 6.

$\vdash\varphi\leftrightarrow t_{u}(\varphi)$

###### Proof.

Proof by induction on the length $|\varphi|=n$ of the formula $\varphi$.

Base case ($n=1$): $\varphi=N_{ab}$ or $\varphi=\beta_{a}$

This is straightforward from definition 10.

Induction hypothesis ($|\varphi|\leq n$):

We have four cases:

  1. 1.

$\varphi=\neg\psi$: we have that $t_{u}(\neg\psi)=\neg t_{u}(\psi)$.

By the I. H., $\vdash\psi\leftrightarrow t_{u}(\psi)$ and
$\vdash\neg\psi\leftrightarrow\neg t_{u}(\psi)$. Thus
$\vdash\varphi\leftrightarrow t_{u}(\neg\psi)$.

  2. 2.

$\varphi=\varphi_{1}\land\varphi_{2}$: we have that
$t_{u}(\varphi_{1}\land\varphi_{2})=t_{u}(\varphi_{1})\land
t_{u}(\varphi_{2})$.

By the I. H., $\vdash\varphi_{1}\leftrightarrow t_{u}(\varphi_{1})$ and
$\vdash\varphi_{2}\leftrightarrow t_{u}(\varphi_{2})$.
Thus $\vdash\varphi_{1}\land\varphi_{2}\leftrightarrow t_{u}(\varphi_{1})\land
t_{u}(\varphi_{2})$ and
$\vdash\varphi_{1}\land\varphi_{2}\leftrightarrow
t_{u}(\varphi_{1}\land\varphi_{2})$.

  3. 3.

$\varphi=X\psi$: we have that $t_{u}(X\psi)=Xt_{u}(\psi)$.

By the I. H., $\vdash\psi\leftrightarrow t_{u}(\psi)$ and
Using using Next rule (proposition 1), $\vdash X\psi\leftrightarrow
Xt_{u}(\psi)$.
Thus $\vdash\varphi\leftrightarrow t_{u}(X\psi)$.

  4. 4.

$\varphi=\varphi_{1}U\varphi_{2}$: we have that
$t_{u}(\varphi_{1}U\varphi_{2})=t_{u}(EXP_{U}(\varphi_{1}U\varphi_{2}))$.

Claim 1: $\vdash t_{u}(EXP_{U}(\varphi_{1}U\varphi_{2}))\leftrightarrow
EXP_{U}(t_{u}(\varphi_{1})Ut_{u}(\varphi_{2}))$

Proof: $EXP_{U}(t_{u}(\varphi_{1})Ut_{u}(\varphi_{2}))=\bigvee\limits_{0\leq
i\leq\lvert\mathcal{A}\rvert}u^{i}(t_{u}(\varphi_{1})Ut_{(}\varphi_{2}))$

= $u^{0}\lor u^{1}\lor...=t_{u}(\varphi_{2})\lor(t(\varphi_{1})\land
Xt_{u}(\varphi_{2}))\lor...$

Using 1., 2. and 3., we can bring the translation operator outside yielding
$\vdash t_{u}(EXP_{U}(\varphi_{1}U\varphi_{2}))\leftrightarrow
EXP_{U}(t_{u}(\varphi_{1})Ut_{u}(\varphi_{2}))$.

Returning to the proof of 4., we have
$t_{u}(\varphi_{1}U\varphi_{2})=t_{u}(EXP_{U}(\varphi_{1}U\varphi_{2}))\\\
=EXP_{U}(t_{u}(\varphi_{1})Ut_{u}(\varphi_{2}))$ by Claim 1. Using axiom
Red.Ax.$U$, we have $\vdash
EXP_{U}(t_{u}(\varphi_{1})Ut_{u}(\varphi_{2}))\leftrightarrow(t_{u}(\varphi_{1})Ut_{u}(\varphi_{2}))$

By the I. H., $\vdash\varphi_{1}\leftrightarrow t_{u}(\varphi_{1})$ and
$\vdash\varphi_{2}\leftrightarrow t_{u}(\varphi_{2})$. And so
$\vdash
EXP_{U}(t_{u}(\varphi_{1})Ut_{u}(\varphi_{2}))\leftrightarrow(\varphi_{1}U\varphi_{2})$.

Using Claim 1,we obtain $\vdash
t_{u}(EXP_{U}(\varphi_{1}U\varphi_{2}))\leftrightarrow(\varphi_{1}U\varphi_{2})$.
Thus,
$\vdash
t_{u}(\varphi_{1}U\varphi_{2})\varphi\leftrightarrow(\varphi_{1}U\varphi_{2})$.

∎

######  Definition 11 (Translation).

Using the reduction axioms it is possible to translate an LTL-SN formula with
no Until occurrences into propositional logic.

$\displaystyle t(N_{ab})$ $\displaystyle=N_{ab}$ $\displaystyle t(\beta_{a})$
$\displaystyle=\beta_{a}$ $\displaystyle t(\varphi\land\psi)$
$\displaystyle=t(\varphi)\land t(\psi)$ $\displaystyle t(\neg\varphi)$
$\displaystyle=\neg t(\varphi)$ $\displaystyle t(XN_{ab})$
$\displaystyle=N_{ab}$ $\displaystyle t(X\beta_{a})$
$\displaystyle=t(\beta_{a}\lor\beta_{N(a)}\geq\theta)$ $\displaystyle
t(X(\varphi\land\psi))$ $\displaystyle=t(X\varphi\land X\psi)$ $\displaystyle
t(X\neg\varphi)$ $\displaystyle=t(\neg X\varphi)$ $\displaystyle t(XX\varphi)$
$\displaystyle=t(Xt(X\varphi))$

Translation inspired by the ones from [7, 9].

######  Definition 12 (Cost measure).

$\displaystyle c(\beta_{a})$ $\displaystyle=1$ $\displaystyle c(N_{ab})$
$\displaystyle=1$ $\displaystyle c(\neg\varphi)$ $\displaystyle=1+c(\varphi)$
$\displaystyle c(\varphi_{1}\land\varphi_{2})$
$\displaystyle=1+max(c(\varphi_{1}),c(\varphi_{2}))$ $\displaystyle
c(X\beta_{a})$ $\displaystyle=4+2\cdot\lvert\mathcal{A}\rvert^{2}$
$\displaystyle c(X\psi)$ $\displaystyle=2\cdot c(\psi)$

where $X\psi$ matches any formula besides those of form $X\beta_{a}$.

######  Lemma 7 (Cost of majority abbreviation).

The cost of the majority abbreviation $c(\beta_{N(a)}\geq\theta)$ in a model
with agent set $\mathcal{A}$ is $2\cdot\lvert\mathcal{A}\rvert^{2}$.

###### Proof.

The outer disjunction ranges over two groups,
$\mathcal{G}\subseteq\mathcal{N}\subseteq\mathcal{A}$, therefore in the worst
case there will be as many terms as $\lvert\mathcal{A}\rvert^{2}$ for each
possible combinations of both. Now analyzing each term, the first two
conjunctions contribute at most $\lvert\mathcal{A}\rvert$ propositions, and
the last conjunction another $\lvert\mathcal{A}\rvert$. Therefore each term
contributes, in the worst case, a cost of $2\cdot\lvert\mathcal{A}\rvert$.
Therefore, the total cost is $2\cdot\lvert\mathcal{A}\rvert^{2}$. ∎

######  Lemma 8 (Translation costs).

For all $\varphi$, $\psi$:

$\displaystyle 1.\ c(\varphi)$ $\displaystyle\geq c(\psi)\ \text{if}\ \psi\in
Sub(\varphi)$ $\displaystyle 2.\ c(XN_{ab})$ $\displaystyle>c(N_{ab})$
$\displaystyle 3.\ c(X\beta_{a})$
$\displaystyle>c(\beta_{a}\lor\beta_{N(a)}\geq\theta)$ $\displaystyle 4.\
c(X(\varphi\land\psi))$ $\displaystyle>c(X\varphi)\land c(X\psi)$
$\displaystyle 5.\ c(X\neg\varphi)$ $\displaystyle>\neg c(X\varphi)$
$\displaystyle 6.\ c(XX\varphi)$ $\displaystyle>c(Xt(X\varphi))$

###### Proof.

We analyze case by case:

Case $c(\varphi)\geq c(\phi)$ if $\phi\in Sub(\varphi)$:

By induction on $\varphi$.

Base case: if $\varphi$ is $\beta_{a}$ or $N_{ab}$, its complexity is $1$ and
it is its only subformula.

Induction hypothesis: $c(\varphi)\geq c(\phi)$ if $\phi\in Sub(\varphi)$.

Induction step:

  * •

Negation ($\neg\varphi$): $\phi$ is a subformula of $\neg\varphi$, therefore
$\phi$ is either $\neg\varphi$ itself or a subformula of $\varphi$. In the
first case it follows directly that $c(\neg\varphi)\geq c(\phi)$. In the
second case, we have that $c(\neg\varphi)=1+c(\varphi)$, and since $\phi$ is a
subformula of $\varphi$, it follow directly by the I. H. that
$c(\neg\varphi)\geq c(\phi)$.

  * •

Conjunction ($\varphi\land\varphi^{\prime}$): $\phi$ is a subformula of
$\varphi\land\varphi^{\prime}$, therefore $\phi$ is either
$\varphi\land\varphi^{\prime}$ itself or a subformula of $\varphi$ or
$\varphi^{\prime}$. In the first case it follows directly that
$c(\varphi\land\varphi^{\prime})\geq c(\phi)$. In the second case, we have
that $c(\varphi\land\varphi^{\prime})=1+max(c(\varphi),c(\varphi^{\prime}))$,
and since $\phi$ is a subformula of either $\varphi$ or $\varphi^{\prime}$, it
follow directly by the I. H. that $c(\varphi\land\varphi^{\prime})\geq
c(\phi)$.

Case $c(XN_{ab})>c(N_{ab})$:

$\displaystyle c(XN_{ab})$ $\displaystyle=2\cdot c(N_{ab})=2$ and
$\displaystyle c(N_{ab})$ $\displaystyle=1$

Case $c(X\beta_{a})>c(\beta_{a}\lor\beta_{N(a)}\geq\theta)$:

$\displaystyle c(X\beta_{a})$
$\displaystyle=4+2\cdot\lvert\mathcal{A}\rvert^{2}$ and $\displaystyle
c(\beta_{a}\lor\beta_{N(a)}\geq\theta)$
$\displaystyle=c(\neg(\neg\beta_{a}\land\neg\beta_{N(a)}\geq\theta))$
$\displaystyle=1+c(\neg\beta_{a}\land\neg\beta_{N(a)}\geq\theta)$
$\displaystyle=2+max(c(\neg\beta_{a}),c(\neg\beta_{N(a)}\geq\theta))$
$\displaystyle=2+max(1+c(\beta_{a}),1+c(\beta_{N(a)}\geq\theta))$
$\displaystyle=2+max(2,1+c(\beta_{N(a)}\geq\theta))$
$\displaystyle=2+max(2,1+2\cdot\lvert\mathcal{A}\rvert^{2})$
$\displaystyle=3+2\cdot\lvert\mathcal{A}\rvert^{2}$

$3+2\cdot\lvert\mathcal{A}\rvert^{2}$ is less than
$4+2\cdot\lvert\mathcal{A}\rvert^{2}$.

Case $c(X(\varphi\land\psi))>c(X\varphi\land X\psi)$:

$\displaystyle c(X(\varphi\land\psi))$ $\displaystyle=2\cdot
c(\varphi\land\psi)=2\cdot(1+max(c(\varphi),c(\psi)))$ $\displaystyle=2+2\cdot
max(c(\varphi),c(\psi))$ and $\displaystyle c(X\varphi\land X\psi)$
$\displaystyle=1+max(c(X\varphi),c(X\psi))=1+max(2\cdot c(\varphi),2\cdot
c(\psi))$ $\displaystyle=1+2\cdot max(c(\varphi),c(\psi))$

$1+2\cdot max(c(\varphi),c(\psi))$ is less than $2+2\cdot
max(c(\varphi),c(\psi))$.

Case $c(X\neg\varphi)>c(\neg X\varphi)$:

$\displaystyle c(X\neg\varphi)$ $\displaystyle=2\cdot
c(\neg\varphi)=2\cdot(1+c(\varphi))$ $\displaystyle=2+2\cdot c(\varphi)$ and
$\displaystyle c(\neg X\varphi)$ $\displaystyle=1+c(X\varphi)=1+2\cdot
c(\varphi)$

$1+2\cdot c(\varphi)$ is less than $2\cdot(1+c(\varphi))$.

Case $c(XX\varphi)>c(Xt(X\varphi))$:

$\displaystyle c(XX\varphi)$ $\displaystyle=2\cdot c(X\varphi)$ and
$\displaystyle c(Xt(X\varphi))$ $\displaystyle=2\cdot c(t(X\varphi))$

Now we show $c(X\varphi)>c(t(X\varphi))$ by induction on the length of
$\varphi$.

Base case: if $\varphi$ has length $1$, then it is either $\beta_{a}$ or
$N_{ab}$:

$\displaystyle c(X\varphi)$ $\displaystyle=2\cdot 1=2$ and $\displaystyle
c(t(X\varphi))$ $\displaystyle=c(N_{ab})=1$ or $\displaystyle c(t(X\varphi))$
$\displaystyle=c(\beta_{a})=1$

Induction hypothesis: $c(X\varphi)>c(t(X\varphi))$ for
$\lvert\varphi\rvert\leq n$.

Induction step:

Case $\varphi=\neg\phi$:

$\displaystyle c(X\varphi)$ $\displaystyle=c(X\neg\phi)=c(\neg
X\phi)=1+c(X\phi)$ and $\displaystyle c(t(X\varphi))$
$\displaystyle=c(t(X\neg\phi))=c(t(\neg X\phi))=c(\neg t(X\phi))$
$\displaystyle=1+c(t(X\phi))$

By I. H., we can conclude $1+c(X\phi)>1+c(t(X\phi))$, therefore
$c(X\varphi)>c(t(X\varphi))$.

Case $\varphi=\phi_{1}\land\phi_{2}$:

$\displaystyle c(X\varphi)$ $\displaystyle=c(X(\phi_{1}\land\phi_{2}))=2\cdot
c(\phi_{1}\land\phi_{2})$
$\displaystyle=2\cdot(1+max(c(\phi_{1}),c(\phi_{2})))=2+2\cdot
max(c(X\phi_{1}),c(X\phi_{2}))$ and $\displaystyle c(t(X\varphi))$
$\displaystyle=c(t(X(\phi_{1}\land\phi_{2})))=c(t(X\phi_{1}\land X\phi_{2}))$
$\displaystyle=c(t(X\phi_{1})\land
t(X\phi_{2}))=1+max(c(t(X\phi_{1})),c(t(X\phi_{2})))$

By I. H., we can conclude
$2+2\cdot
max(c(X\phi_{1}),c(X\phi_{2}))>1+max(c(t(X\phi_{1})),c(t(X\phi_{2})))$,
therefore $c(X\varphi)>c(t(X\varphi))$.

Case $\varphi=X\phi$:

$\displaystyle c(X\varphi)$ $\displaystyle=c(XX\phi)=2\cdot c(X\phi)$ and
$\displaystyle c(t(X\varphi))$
$\displaystyle=c(t(XX\phi))=c(t(Xt(X\phi)))=\Box$

By I. H., we know $c(Xt(X\phi))>\Box$. $c(Xt(X\phi))=2\cdot c(t(X\phi))$. By
I. H. we know $2\cdot c(X\phi)>2\cdot c(t(X\phi))>\Box$, therefore
$c(X\varphi)>c(t(X\varphi))$. ∎

######  Lemma 9 (Translation equivalence).

$\vdash\varphi\leftrightarrow t(\varphi)$

###### Proof.

By induction on $c(\varphi)$.

Base case: $\varphi$ is either $\beta_{a}$ or $N_{ab}$, translation keeps them
unchanged and therefore $\vdash\varphi\leftrightarrow t(\varphi)$.

Induction hypothesis: For all $\varphi$ such that $c(\varphi)<n:\
\vdash\varphi\leftrightarrow t(\varphi)$.

Induction step: Case for negation and conjunction: straightforward from lemma
8 item 1.

Case $XN_{ab}$: This case follows from the $Red.Ax.X.N$ axiom, item 2 of lemma
8 and the I. H..

Case $X\beta_{a}$: This case follows from the $Red.Ax.X.\beta$ axiom, item 3
of lemma 8 and the I. H..

Case $X(\varphi\land\psi)$: This case follows from the $A8$ axiom, item 4 of
lemma 8 and the I. H..

Case $X\neg\varphi$: This case follows from the $A2$ axiom, item 5 of lemma 8
and the I. H..

Case $XX\varphi$: By I. H. we know $\vdash X\varphi\leftrightarrow
t(X\varphi)$. Therefore we can replace into $Xt(X\varphi)$ by proposition 2,
and it follows from item 6 of lemma 8. ∎

######  Theorem 1 (Completeness).

For every $\varphi\in\mathcal{LTL-SN}$:

$\models\varphi\ \text{implies}\ \vdash\varphi$

###### Proof.

Suppose $\models\varphi$. By lemma 9 and since the proof system is sound, we
have that $\models t(\varphi)$. The formula $t(\varphi)$ is propositional,
therefore $\mathcal{PROP}\vdash t(\varphi)$ by completeness of propositional
logic. We also have that $\mathcal{LTL-SN}\vdash t(\varphi)$ since
$\mathcal{PROP}$ is a subsystem of LTL-SN. Again by lemma 9 we have that
$\mathcal{LTL-SN}\vdash\varphi$. ∎

##  5 Model Checking

In this section we analyse the computational complexity of the model checking
problem.

######  Definition 13.

The model checking problem consist of, given a formula $\phi$ and a finite
LTL-SN model ${\cal M}=(\mathcal{A},N,\theta,I)$, determining the set ${\cal
S}(\phi)=\\{i\mid b_{i}\in b~{}\mathrm{and}~{}{\cal M},i\models\phi\\}$

Next, we present the model checking algorithm for LTL-SN. Let $label(i)$
denote the set of sub-formulas that hold at path position $i$. We start by
initializing $label(i):=\\{\beta_{a}\mid a\in b_{i}\\}\cap\\{N_{ab}\mid b\in
N_{a}\\}$ for all path positions $i$.

Algorithm 1 procedure Check($\phi$)

while $|\phi|\geq 1$ do

if $\phi=(\lnot\phi_{1})$ then

$Check(\phi_{1})$; $CheckNOT(\phi_{1})$

else if $\phi=(\phi_{1}\land\phi_{2})$ then

$Check(\phi_{1})$; $Check(\phi_{2})$; $CheckAND(\phi_{1},\phi_{2})$

else if $\phi=X\phi_{1}$ then

$Check(\phi_{1})$; $CheckX(\phi_{1})$

else if $\phi=\phi_{1}U\phi_{2}$ then

$Check(\phi_{1})$;$Check(\phi_{2})$; $CheckU(\phi_{1},\phi_{2})$

end if

end while

Algorithm 2 procedure CheckNOT($\phi$)

for all $i$ do

if $\phi\not\in label(i)$ then

$label(i):=label(i)\cup\\{(\lnot\phi)\\}$

end if

end for

Algorithm 3 procedure CheckAND($(\phi_{1}\land\phi_{2}$)

for all $i$ do

if $\phi_{1}\in label(i)$ and $\phi_{2}\in label(i)$ then

$label(i):=label(i)\cup\\{(\phi_{1}\land\phi_{2})\\}$

end if

end for

Algorithm 4 procedure CheckX($\phi_{1}$)

$T:=\\{i~{}|~{}\phi_{1}\in label(i)\\}$

while $T\not=\emptyset$ do

choose $i\in T$

$T:=T\setminus\\{i\\}$

if $X\phi_{1}\not\in label(i-1)$ then

$label(i-1):=label(i-1)\cup\\{X\phi_{1}\\}$

end if

end while

Algorithm 5 procedure CheckEU($\alpha_{1}$,$\alpha_{2}$)

$T:=\\{i~{}|~{}\phi_{2}\in label(i)\\}$

for all $i\in T$ do

$label(i):=label(i)\cup\\{E(\alpha_{1}\mathcal{U}\alpha_{2})\\}$

end for

while $T\neq\emptyset$ do

choose maximum$~{}i\in T$

$T:=T\backslash\\{i\\}$

while $\phi_{1}\in label(i-1)$ do

if $E(\phi_{1}\mathcal{U}\phi_{2})\not\in label(i-1)$ then

$label(i-1):=label(i-1)\cup\\{E(\phi_{1}\mathcal{U}\phi_{2})\\}$

$i:=i-1$

$T:=T\backslash\\{i\\}$

end if

end while

end while

######  Theorem 2.

Given a LTL-SN model ${\cal M}=(\mathcal{A},N,\theta,I)$ and formula $\phi$.
The computational complexity of the model checking problem is
$O(\mid\phi\mid\times\mid\mathcal{A}\mid)$, i.e., linear in the size of the
formula times the size of the set of agents.

###### Proof.

By lemma 1, there exists a unique path such that $b_{0}=I$. By lemma 3, this
path $b_{0},...,b_{n}$ reaches a fixed-point such that $n<|\mathcal{A}|$.

The algorithm Check($\phi$) is called once for each sub-formula of $\phi$
which is $O(|\phi|)$ and each time it activates the algorithms CheckNOT,
CheckAND, CheckX and CheckU. The algorithm CheckX, in the worse case, has to
visit all $b_{i}$, which is $O(|\mathcal{A}|)$ The CheckU, starts with the
greatest $i$ where $\phi_{2}$ holds, and then it goes labelling states smaller
than i, where $\phi_{1}$ holds, with $\phi_{1}U\phi_{2}$. In worse case, it
has to search the whole model which is also $O(|\mathcal{A}|)$. The algorithms
CheckNOT, CheckAND take constant time. Thus, the complexity of Check($\phi$)
is $O(|\mathcal{A}|\times|\phi|)$. In order to o build the set $S(\phi)$ we
only need to search $label(i)$, for all $0\leq i<|\mathcal{A}|$, and check if
$\phi\in label(i)$. ∎

##  6 Conclusion and future works

The paper presented a class of models for the study of social networks, based
on threshold models as seen across the literature. With this, we have
developed a logic with the same operators as LTL, but for a restricted class
of models focused specifically on the study of social networks, proved its
soundness and its completeness via a translation argument, and briefly
discussed model checking complexity. With this framework one is able to
capitalize on existing model checking solutions for LTL, which we believe is a
good incentive to pursue this line of work.

Given the previous conclusion, a natural future work is to explore these model
checkers and analyze the evolution of some network instances and compare them
against data from real social networks.

In regard to the logic itself, we also believe it would be interesting to
pursue a branching paths model, where agents may or may not adopt a behavior
after each step. This would further leverage the expressive power of LTL,
however a sound and complete axiomatization will require some more work, as a
reduction into propositional logic may not work anymore.

###  6.1 Acknowledgements

We would like to thank the research agencies CNPq, CAPES and FAPERJ for their
support.

## References

  * [1] Apt, K.R., Markakis, E.: Diffusion in social networks with competing products. In: Persiano, G. (ed.) Algorithmic Game Theory. pp. 212–223. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)
  * [2] Baltag, A., Christoff, Z., Kræmmer Rendsvig, R., Smets, S.: Dynamic epistemic logics of diffusion and prediction in social networks. Studia Logica (07 2018). https://doi.org/10.1007/s11225-018-9804-x
  * [3] Burgess, J.P., et al.: Axioms for tense logic. i.“since”and“until”. Notre Dame Journal of Formal Logic 23(4), 367–374 (1982)
  * [4] Christoff, Z., Hansen, J.U., Proietti, C.: Reflecting on social influence in networks. J. of Logic, Lang. and Inf. 25(3–4), 299–333 (Dec 2016). https://doi.org/10.1007/s10849-016-9242-y, https://doi.org/10.1007/s10849-016-9242-y
  * [5] Dam, M.: Lecture notes in temporal logic (1 2021), http://www.csc.kth.se/~mfd/Courses/Temporal_logic/course_description.php
  * [6] DeGroot, M.H.: Reaching a consensus. Journal of the American Statistical Association 69(345), 118–121 (1974), http://www.jstor.org/stable/2285509
  * [7] Ditmarsch, H.v., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Springer Publishing Company, Incorporated, 1st edn. (2007)
  * [8] Finger, M., Gabbay, D.M.: Adding a temporal dimension to a logic system. Journal of Logic, Language, and Information 1(3), 203–233 (1992), http://www.jstor.org/stable/40180020
  * [9] Kooi, B., Benthem, J.: Reduction axioms for epistemic actions. Preliminary Proceedings of AiML-2004 (01 2004)
  * [10] Lehrer, K.: When rational disagreement is impossible. Noûs 10(3), 327–332 (1976), http://www.jstor.org/stable/2214612
  * [11] Rendsvig, R.K.: Diffusion, influence and best-response dynamics in networks: An action model approach. CoRR abs/1708.01477 (2017), http://arxiv.org/abs/1708.01477
  * [12] Venema, Y.: Temporal Logic, chap. 10, pp. 203–223. John Wiley and Sons, Ltd (2017). https://doi.org/https://doi.org/10.1002/9781405164801.ch10, https://onlinelibrary.wiley.com/doi/abs/10.1002/9781405164801.ch10
  * [13] Zhen, L., Seligman, J.: A logical model of the dynamics of peer pressure. Electronic Notes in Theoretical Computer Science 278, 275 – 288 (2011). https://doi.org/https://doi.org/10.1016/j.entcs.2011.10.021, http://www.sciencedirect.com/science/article/pii/S1571066111001496, proceedings of the 7th Workshop on Methods for Modalities (M4M’2011) and the 4th Workshop on Logical Aspects of Multi-Agent Systems (LAMAS’2011)


# Orthogonal Dissection into Few Rectangles

David Eppstein Department of Computer Science, University of California,
Irvine. Research supported in part by NSF grant CCF-2212129.

###### Abstract

We describe a polynomial time algorithm that takes as input a polygon with
axis-parallel sides but irrational vertex coordinates, and outputs a set of as
few rectangles as possible into which it can be dissected by axis-parallel
cuts and translations. The number of rectangles is the rank of the Dehn
invariant of the polygon.

##  1 Introduction

Slicing an orthogonal polygon horizontally through each vertex partitions it
into rectangles, but may use more rectangles than necessary. Instead, a
partition into a minimum number of rectangles can be found in polynomial time,
even for polygons with holes. The algorithm finds axis-parallel segments
through pairs of non-convex vertices, and uses bipartite matching to find a
maximum independent set in the intersection graph of segments. The resulting
independent slices, with one additional slice through each remaining non-
convex vertex, minimize the number of rectangles [7, 14, 16, 6].

What if we allow sliced pieces to be rejoined? Slicing a polygon into pieces
and rejoining them into another polygon is called _dissection_. For example,
the Greek cross of Fig. 1 requires three rectangles when partitioned, but has
a three-piece dissection into one rectangle, as shown. In fact, every polygon
(orthogonal or not) can be dissected into every other polygon of the same
area; this is the _Wallace–Bolyai–Gerwien theorem_ [2, 9, 11, 20]. Therefore,
a dissection into one rectangle always exists. However, this dissection may
rotate pieces and use non-axis-aligned cuts, unnatural for orthogonal
polygons. Instead, we ask: if we consider dissections that use only axis-
parallel slices, translations, and rejoining of the sliced pieces, without
rotations, how few rectangles can we dissect a given shape into? For instance,
the figure demonstrates that the answer for the Greek cross is one: it can be
dissected into a single rectangle. We call this restricted class of
dissections _orthogonal dissections_.111It would be natural to allow also
$90^{\circ}$-rotations, but our results do not directly extend to dissections
that allow such rotations.

Figure 1: Dissection of a Greek cross into a rectangle, using only axis-
parallel cuts and translation of pieces.

Polyominoes such as the Greek cross always have an orthogonal dissection into
one rectangle: just subdivide into some number $n$ of squares and rearrange
into a $1\times n$ rectangle. However, we consider polygons with irrational
coordinates, for which an orthogonal dissection into a single rectangle may
not exist. To address the computational issues that this entails, we assume
that all coordinates are presented as rational linear combinations of a
_rational basis_ , a set of real numbers for which no nontrivial rational
linear combination sums to zero. Our main result is an algorithm that in
polynomial time computes the minimum number of rectangles into which a given
orthogonal polygon can be dissected, and constructs a family of rectangles of
that minimum size into which it may be dissected. As we show, this has strong
implications for the possibility of dissecting a polygon into a prototile that
can tile the plane: such a dissection exists if and only if the minimum number
of rectangles is one or two.

The main technical tool that we use for this task is a form of the _Dehn
invariant_. The Dehn invariant is a value living in an infinite-dimensional
tensor space, usually used for three-dimensional polyhedral dissection
problems. One polyhedron can be dissected into another if and only if they
have the same areas and Dehn invariants, and a polyhedron can be dissected to
tile space if and only if its Dehn invariant is zero [3, 5, 12, 19]. Another
version of the Dehn invariant has also been used for orthogonal dissection of
rectangles to rectangles, in order to prove that such a dissection exists if
and only if the two rectangles have equal areas and rationally related sides
[1, 4, 17, 18]. For instance, because the Greek cross of Fig. 1 (scaled to
form a pentomino, with side length one) has an orthogonal dissection into a
rectangle with dimensions $2\times 2\,\tfrac{1}{2}$, it cannot also be
orthogonally dissected into a $\sqrt{5}\times\sqrt{5}$ square. (Instead, it
can be dissected into a square using only two straight but not axis-parallel
cuts [8].)

Our key insight is that, as order-two tensors, Dehn invariants have
significant structure beyond merely being equal or unequal to each other or
zero. In particular, like matrices, they have a rank, and this rank is
geometrically meaningful. We prove that, for the orthogonal Dehn invariant,
the rank equals the minimum number of rectangles that can be obtained from an
orthogonal dissection. For the Dehn invariant of polyhedra, we do not have as
precise a relation, but the rank of the Dehn invariant (if nonzero) provides a
lower bound on the minimum number of edges in a polyhedron to which the given
polyhedron can be dissected.

##  2 Model of computation

We consider inputs that are _orthogonal polygons_ , bounded regions of the
plane whose boundary consists of finitely many axis-parallel line segments,
allowing polygons with holes. We assume that the input specifies the
coordinates of each vertex (endpoint of a boundary segment). Because the
problems we consider are nontrivial only for polygons with irrational
coordinates, it is necessary to say something about how those coordinates are
represented and how we compute with them. We assume that the input is
described in terms of a _rational basis_ , finitely many real numbers with the
property that if a linear combination of basis elements with rational-number
coefficients adds to zero, all coefficients must be zero.222A note on
terminology: A rational basis does not generally consist of rational numbers.
On the contrary, at most one member of the basis can be rational. We allow
different bases for the $x$-coordinates and the $y$-coordinates (an $x$-basis
and a $y$-basis) or a single combined basis. Each vertex coordinate is a
rational linear combination of basis elements, represented as a vector of
rational-number coefficients, one for each basis element. The size of the
input is the number of rational coefficients needed to describe all of the
polygon vertices: the product of the number of vertices with the sum of the
sizes of the $x$-basis and $y$-basis.

To compute the minimum number of rectangles in an orthogonal dissection, no
additional information about the basis elements is necessary. Our algorithm
for this version of the problem uses only rational-number arithmetic, and
performs a polynomial number of arithmetic operations: essentially, only
Gaussian elimination applied to a matrix whose coefficients are quadratic
combinations of input coefficients. However, we need additional assumptions
that allow computation with basis elements in order to verify that the input
describes a polygon without edge crossings, or to construct the rectangles
into which it can be dissected. To do these things, we need the following
additional primitive operations:

  * •

Find the sign of a a rational combination of basis elements, or of a rational
combination of products of $x$-basis elements and $y$-basis elements.

  * •

Given any two rational combinations of basis elements, or of products of
$x$-basis elements and $y$-basis elements, find a rational number between
them.

We are not aware of past use of this specific computational model. However,
exact computation using algebraic numbers is common in computational geometry
implementation libraries [15, 13], and it is standard to represent such
numbers as rational combinations of roots of a Galois polynomial, a special
case of a rational basis. We have stated our results in a more general model
that does not specify the algebraic nature of the numbers, so that they can be
applied as well to coordinates involving transcendental numbers such as $\pi$
and $e$.

##  3 The orthogonal Dehn invariant

In terms of the given rational basis, the Dehn invariant $\mathcal{D}(P)$ of
an orthogonal polygon $P$ can be described as a matrix of rational numbers,
with rows indexed by $y$-basis elements and columns indexed by $x$-basis
elements, constructed as follows:

  * •

Express the given polygon as a linear combination of rectangles $R_{i}$. For
instance, if coordinate comparisons are available, we may slice the polygon
horizontally through each non-convex vertex. If comparisons are unavailable,
we may instead choose the line through one horizontal side as a base and
consider the family of signed rectangles between each other horizontal side
and this base line.

  * •

Express the width $w_{i}$ and height $h_{i}$ of each rectangle $R_{i}$ as a
linear combination of basis elements with rational coefficients. The width is
the difference of $x$-coordinates of right and left sides of the rectangle,
the height is the difference of $y$-coordinates of top and bottom sides, and
the difference of two linear combinations of basis elements produces another
linear combination.

  * •

Construct a matrix $M_{i}$, the outer product of the expressions for $w_{i}$
and $h_{i}$. The coefficient of this matrix, for the column corresponding to
an $x$-basis element $x_{j}$ and the row corresponding to a $y$-basis element
$y_{k}$, is a rational number, the product of the coefficient of $x_{j}$ in
$w_{i}$ and the coefficient of $y_{k}$ in $h_{i}$.

  * •

The Dehn invariant of the polygon is the sum of matrices $\sum_{i}M_{i}$.

Figure 2: Three rectangles with dimensions $2^{2/3}\times 1$, $2^{1/3}\times
2^{1/3}$, and $1\times 2^{2/3}$ (yellow), and a polygon formed by gluing them
together (blue)

For example, for the blue polygon in Fig. 2 and the rational basis
$\\{1,2^{1/3},2^{2/3}\\}$, this computation would yield as the Dehn invariant
the matrix

$\begin{pmatrix}0&0&1\\\ 0&1&0\\\ 1&0&0\end{pmatrix},$

as can be seen from its dissection into yellow rectangles in the figure. These
have basis elements as widths and heights, and they each contribute a single 1
coefficient to the total.

Instead of using a specific basis, one can describe the same thing in a basis-
free way by writing that the Dehn invariant is an element of the tensor
product of $\mathbb{Q}$-vector spaces
$\mathbb{R}\otimes_{\mathbb{Q}}\mathbb{R}$, and can be determined as a sum of
elements of this tensor product:333The Dehn invariant is often written as an
element of a tensor product of abelian groups, rather than of vector spaces,
using the notation $\mathbb{R}\otimes_{\mathbb{Z}}\mathbb{R}$ or, for the
polyhedral invariant, $\mathbb{R}\otimes_{\mathbb{Z}}\mathbb{R}/\mathbb{Z}$.
The group notation makes more sense for some contexts; for instance, it works
for the polyhedral invariant in hyperbolic or spherical geometry, where linear
scaling of polyhedra is not possible. But for our use of tensor rank, vector
space notation is more convenient. For the equivalence of matrices and tensors
see [10].

$\mathcal{D}(P)=\sum_{i}h_{i}\otimes w_{i}.$

It is an invariant of $P$, in the sense that its value (either thought of as a
matrix for a specific basis or as a tensor) does not depend on the
decomposition into rectangles used to compute it, and remains unchanged under
orthogonal dissections; see Section 4.

In contrast to the polyhedral Dehn invariant, the area of an orthogonal
polygon $P$ can be recovered from its Dehn invariant under any basis, as the
sum

$\sum_{j}\sum_{k}\mathcal{D}(P)_{kj}x_{j}y_{k}$

of products of matrix coefficients, $x$-basis elements, and $y$-basis
elements. In this sense, it is meaningful to speak of the area of a Dehn
invariant, rather than the area of a polygon.

##  4 Invariance of the Dehn invariant

Previous works on the orthogonal Dehn invariant only appear to have considered
it with regard to rectangles, rather than for orthogonal polygons more
generally. Therefore, for completeness, we prove that it is an invariant of
orthogonal polygons under dissection, although we believe this to be implicit
in previous work [1, 4, 17, 18]. Throughout this section, we use the abstract
tensor space formulation of the orthogonal Dehn invariant; everything carries
directly over to the formulation in any particular basis, according to
standard principles on the invariance of linear algebra under different
choices of basis.

######  Lemma 4.1.

Let $R$ be a rectangle with height $h$ and width $w$. Suppose $R$ is
subdivided arbitrarily by vertical and horizontal lines into a rectangular
grid of smaller rectangles of heights $h_{j}$ and widths $w_{k}$, as depicted
in Fig. 3. For all such subdivisions, $h\otimes w=\sum h_{j}\otimes w_{k}$.

Figure 3: Illustration for Lemma 4.1: subdividing a rectangle into a grid of
smaller rectangles does not change its Dehn invariant.

######  Proof 4.2.

This follows immediately from the facts that $\sum h_{j}=h$ and that $\sum
w_{k}=w$, and from the bilinearity of tensors.

######  Lemma 4.3.

Let $P$ be any orthogonal polygon. Then regardless of how $P$ is subdivided
into rectangles $R_{i}$ of height $h_{i}$ and width $w_{i}$, the value $\sum
h_{i}\otimes w_{i}$ will be unchanged. That is, $\mathcal{D}(P)=\sum
h_{i}\otimes w_{i}$ is well-defined as an invariant of $P$.

######  Proof 4.4.

Consider any two different subdivisions into rectangles $R_{i}$ and
$R^{\prime}_{i}$, and refine both subdivisions into a common subdivision by
extending vertical and horizontal lines through all vertices of both $R_{i}$
and $R^{\prime}_{i}$. By Lemma 4.1, this refinement does not change the sum
over the rectangles in either subdivision. Because both of the sums coming
from the initially given subdivisions are equal to the sum coming from their
common refinement, they must be equal to each other.

######  Lemma 4.5.

If two orthogonal polygons $P$ and $P^{\prime}$ are related by an orthogonal
dissection, then $\mathcal{D}(P)=\mathcal{D}(P^{\prime})$. That is, the Dehn
invariant remains invariant under orthogonal dissections.

######  Proof 4.6.

We can refine any orthogonal dissection into a dissection for which all pieces
are rectangles, and use those rectangles to calculate $\mathcal{D}(P)$ and
$\mathcal{D}(P^{\prime})$. Translating a rectangle obviously does not change
its height or width, so the result follows from Lemma 4.3.

##  5 The rank of the Dehn invariant

Any tensor has a rank, the minimum number of terms needed to express it as a
sum of tensor products. The Dehn invariants we are considering are order-two
tensors over the field of rational numbers, and for any order-two tensor over
any field, the rank of the tensor equals the rank of any matrix representing
it for any basis over that field. As the rank of a matrix, it equals the
minimum number of terms in an expression of the matrix as a sum of outer
products of vectors [10]. Therefore, the rank of the Dehn invariant is just
the rank of the matrix computed in Section 3. It does not depend on the basis
chosen to construct this matrix, and it can be computed using any standard
algorithm for matrix rank, such as Gaussian elimination.

If an orthogonal polygon $P$ has an orthogonal dissection into $r$ rectangles
with height $h_{i}$ and width $w_{i}$, we have seen that its Dehn invariant
can be expressed as

$\mathcal{D}(P)=\sum_{i=1}^{r}h_{i}\otimes w_{i}.$

This is an expression as a sum of $r$ products, so the Dehn invariant has rank
at most $r$. Conversely, if an orthogonal polygon $P$ has a Dehn invariant
with rank $r$, then it has an expression of exactly this form. However, not
all terms of such an expression may be interpreted as describing rectangles.
To come from a rectangle, a term $h_{i}\otimes w_{i}$ must have $h_{i}\cdot
w_{i}>0$, in which case it can come from any rectangle of height
$q\cdot|h_{i}|$ and width $|w_{i}|/q$ for any positive rational number $q$.
All of these different rectangles produce the same value $h_{i}\otimes w_{i}$.
But if the product $h_{i}\cdot w_{i}$ is a negative number, then $h_{i}\otimes
w_{i}$ cannot be the Dehn invariant of a rectangle or of any polygon, because
it would have negative area. For this reason, the rank of the Dehn invariant
lower bounds the number of rectangles that can be obtained in an orthogonal
dissection, but it requires an additional argument to prove that these two
numbers are equal.

##  6 Geometric realizability

In the case of the polyhedral Dehn invariant, not every tensor in the space
describing these invariants comes from the Dehn invariant of a polyhedron.
There exists a surjective homomorphism of groups from the tensor space
$\mathbb{R}\otimes_{\mathbb{Z}}\mathbb{R}/\mathbb{Z}$ onto the group
$\Omega^{1}_{\mathbb{R}/\mathbb{Q}}$ of Kähler differentials, such that the
tensors coming from Dehn invariants are exactly those mapped to the group
identity. The preimages of nonzero Kähler differentials are tensors that do
not come from Dehn invariants [5]. In contrast, for the orthogonal Dehn
invariant, the only obstacle to geometric realizability is area:

Figure 4: Illustration for Lemma 6.1: realizing each term in a tensor by a
rectangle of height near one, forming the difference of the positive and
negative rectangles, and repartitioning the result into rectangles, produces a
set of $r$ rectangles having a given Dehn invariant of rank $r$.

######  Lemma 6.1.

Let $D=\sum_{i=1}^{r}h_{i}\otimes w_{i}$ be a tensor of rank $r$ in
$\mathbb{R}\otimes_{\mathbb{Q}}\mathbb{R}$, and suppose that the putative area
$a(D)=\sum_{i=1}^{r}h_{i}\cdot w_{i}$ is positive. Then $D$ is the Dehn
invariant of a disjoint union of $r$ rectangles.

######  Proof 6.2.

Partition the range of indices $[1,r]$ into two subsets $I^{+}$ and $I^{-}$,
where $i\in I^{+}$ if $h_{i}\cdot w_{i}>0$ and in $i^{-}$ otherwise. (Because
each term contributes to the rank, it is not possible for $h_{i}\cdot w_{i}$
to equal zero.) Let $a^{+}=\sum_{i\in I^{+}}h_{i}\cdot w_{i}$ and
$a^{-}=-\sum_{i\in I^{+}}h_{i}\cdot w_{i}$, so that $a(D)=a^{+}-a^{-}$. By
assumption this is positive. We may assume without loss of generality that
both sets of indices are non-empty: $I^{+}$ non-empty is needed to make $a(D)$
positive, and if $I^{-}$ is empty then we can represent $D$ using the disjoint
union of rectangles of height $|h_{i}|$ and width $|w_{i}|$ without any
additional construction. We can find two rational numbers $\alpha$ and
$\varepsilon>0$ such that $a^{-}<\alpha<a^{+}$, with
$a^{-}<\alpha(1-\varepsilon)$ and
$a^{+}>\alpha(1+\varepsilon)$.444Computationally, this uses the assumption
from our model of computation that we can find a rational number between two
products of combinations of basis elements. These numbers are illustrated with
the dashed blue axis-parallel lines in Fig. 4.

Let $A$ be a rectangle with unit height and with width $\alpha$. For each
index $i\in I^{+}$, find a positive rational number $q_{i}$ such that
$1<q_{i}\cdot|h_{i}|<1+\varepsilon$, and construct a rectangle of height
$q_{i}\cdot|h_{i}|$ and width $|w_{i}|/q_{i}$, whose Dehn invariant is
$h_{i}\otimes w_{i}$. Arranging these rectangles side by side on a common
baseline produces an orthogonal polygon $P^{+}$ whose height varies between
$1$ and $1+\varepsilon$, whose area is $a^{+}$, and whose Dehn invariant is
$\sum_{i\in I^{+}}h_{i}\otimes w_{i}$. In order to achieve area $a^{+}$ with
height everywhere less than $1+\varepsilon$, $P^{+}$ must have width greater
than $a^{+}/(1+\varepsilon)<\alpha$, so it completely covers $A$. These side-
by-side rectangles are shown in yellow in the top part of Fig. 4.

In the same way, for each index $i\in I^{-}$, find a positive rational number
$q_{i}$ such that $1-\varepsilon<q_{i}\cdot|h_{i}|<1$, and construct a
rectangle of height $q_{i}\cdot|h_{i}|$ and width $|w_{i}|/q_{i}$, whose Dehn
invariant is $h_{i}\otimes w_{i}$. Arranging these rectangles side by side on
a common baseline produces an orthogonal polygon $P^{-}$ whose area is $a^{-}$
and whose Dehn invariant is $-\sum_{i\in I^{+}}h_{i}\otimes w_{i}$, entirely
within $A$, the red rectangles in the top part of Fig. 4.

Arranging $P^{+}$ and $P^{-}$ so they share the same bottom left vertex, and
computing the set-theoretic difference $P^{+}\setminus P^{-}$, produces a
polygon $P$ whose Dehn invariant is $D$. It can be sliced vertically at each
vertex whose $x$-coordinate is intermediate between its smallest and largest
$x$-coordinate, as shown in the bottom part of Fig. 4. There are $r-1$ slices
(one for each side where two rectangles from $I^{+}$ meet, and one for each
left side of a rectangle from $I^{-}$), so the result is a set of $r$
rectangles with total Dehn invariant $D$, as required.

##  7 Dissectability

Long after the work of Dehn, Sydler proved that the polyhedral Dehn invariant
is a complete invariant: any two polyhedra with the same volumes and Dehn
invariants can be dissected to each other [19]. We need an analogous result
for the orthogonal Dehn invariant. We do not bound the number of pieces in a
dissection; a polynomial bound is not possible, because even the trivial
dissection of a $1\times n$ rectangle into an $n\times 1$ rectangle requires
$n$ pieces, a non-polynomial number.

######  Theorem 7.1.

Any two orthogonal polygons with the same Dehn invariant have an orthogonal
dissection.

Figure 5: Illustration for Theorem 7.1. The horizontal red lines are (from top
to bottom) $y=\varepsilon^{+}$, $y=0$, and $y=-\varepsilon^{-}$; the vertical
lines are (left to right) $x=0$ and $x=\min\\{c_{i}^{+},c_{i}^{-}\\}$. Slicing
the rectangles in $R_{i}^{+}$ (yellow) and $R_{i}^{-}$ (blue) by these lines
dissects them into a family of rectangles whose heights do not depend on
$\hat{y}$ (the bottom blue and yellow rectangles) together with a single
rectangle whose coefficient of $\hat{y}$ is $\pm 1$ (red).

######  Proof 7.2.

We may assume without loss of generality that the two polygons $P_{1}$ and
$P_{2}$ have already been dissected into (different) disjoint sets of
rectangles $R_{1}$ and $R_{2}$. We use induction on the size of rational bases
for the heights and widths of these rectangles (which may be a superset of a
basis for the Dehn invariant). As a base case, if these bases have size one,
all rectangles have heights and widths that are rational multiples of each
other. In this case we can scale the $x$ and $y$ coordinates separately to
clear denominators in these coordinates and make all rectangle side lengths
integers, allowing a dissection using unit squares.

Otherwise, by the symmetry of heights and widths, we can assume without loss
of generality that the $y$-basis has at least two elements; let $\hat{y}$ be
one of them. For each rectangle in $R_{1}$ and $R_{2}$, of width $w_{i}$ and
height $h_{i}$ let $q_{i}$ be the coefficient of $\hat{y}$ in the expansion of
$h_{i}$ as a rational combination of basis elements. Whenever $q_{i}\neq 0$,
apply the base case of the theorem (for the one-element bases $\\{w_{i}\\}$
and $\\{h_{i}\\}$) to dissect that rectangle into another rectangle of width
$q_{i}\cdot w_{i}$ and height $h_{i}/q_{i}$. After this step, for all
rectangles in $R_{1}$ and $R_{2}$, the coefficient of $\hat{y}$ in the
rectangle height belongs to $\\{-1,0,1\\}$. Let $R_{i}^{+}$ be the rectangles
in $R_{i}$ for which this coefficient is $1$, $R_{i}^{-}$ be the rectangles
for which it is $-1$, and $R_{i}^{0}$ be the rectangles for which it is $0$.
By composition of dissections, a dissection of these modified sets of
rectangles into each other will lead to a dissection of $P_{1}$ and $P_{2}$
into each other.

For each of $P_{1}$ and $P_{2}$, translate the rectangles of $R_{i}^{+}$ so
they are placed side by side, with their bottom sides all placed on the
$x$-axis, with the left side of the leftmost rectangle placed on the $y$-axis.
Similarly translate the rectangles of $R_{i}^{-}$ so they are side by side,
with their top sides all placed along the $x$-axis, and again with the left
side of the leftmost rectangle placed on the $y$-axis. Let $\varepsilon$ be
the smallest height of any rectangle in either $R_{1}$ or $R_{2}$. Choose two
numbers $0<\varepsilon^{+}<\varepsilon$ and $0<\varepsilon^{-}<\varepsilon$,
so that both of these numbers are expressible as a rational combination of
elements of the $y$-basis, with the coefficient of $\hat{y}$ in
$\varepsilon^{+}$ equal to $1$ and the coefficient of $\hat{y}$ in
$\varepsilon^{-}$ equal to $-1$. (The ability to make this choice hinges on
the fact that the rational multiples of any remaining basis element are dense
in the real number line.) Let $c_{i}^{+}$ be the $x$-coordinate of the right
end of the rightmost rectangle in the placement of $R_{i}^{+}$, and define
$c_{i}^{-}$ symmetrically.

Now that the rectangles have been placed in this way, slice them by the
horizontal lines $y=\varepsilon^{+}$ and $y=-\varepsilon^{-}$. This leaves a
hexagonal region between these two lines, which we dissect into two rectangles
by slicing it with the vertical line $x=\min\\{c_{i}^{+},c_{i}^{-}\\}$ (two
different lines, one for $R_{1}$ and the other for $R_{2}$). The dissection is
shown in Fig. 5.

The rectangles in $R_{i}^{0}$, the remaining parts of rectangles in
$R_{i}^{+}$ above the line $x=\varepsilon^{+}$, and the remaining parts of
rectangles in $R_{i}^{-}$ below the line $x=\varepsilon^{-}$, all have heights
whose rational expansion in terms of the $y$-basis does not use $\hat{y}$. The
rectangle to the left of the vertical slice line, and between the two
horizontal slice lines, has height $\varepsilon^{+}+\varepsilon^{-}$; here,
the coefficients of $\hat{y}$ cancel leaving a rectangle height whose
expansion in terms of the basis does not use $\hat{y}$. This leaves all
dependence on $\hat{y}$ concentrated in one remaining rectangle, to the left
of the vertical slice line, with height $\varepsilon^{+}$ or $\varepsilon^{-}$
and width $|c_{i}^{+}-c_{i}^{-}|$. Let $\hat{w}_{i}$ denote this width.

Because all remaining pieces except this rectangle have heights that do not
depend on $\hat{y}$, it follows that the coefficients of $\mathcal{D}(P_{i})$,
in the row of the coefficient matrix corresponding to basis element $\hat{y}$,
are exactly the coefficients in the rational expansion of $\hat{w}_{i}$ for a
rectangle of height $\varepsilon^{+}$, or the negation of those coefficients
for a rectangle of height $\varepsilon^{-}$. By the assumption that
$\mathcal{D}(P_{1})=\mathcal{D}(P_{2})$, these matrix coefficients must be
equal. The widths $\hat{w}_{1}$ and $\hat{w}_{2}$ of the rectangles can be
recovered, up to their signs, as the number represented by these coefficients
using the $y$-basis. It is not possible for the two signs to be different,
because both $\hat{w}_{1}$ and $\hat{w}_{2}$ are non-negative. Therefore, the
two remaining rectangles must both have the same height, $\varepsilon^{+}$ or
$\varepsilon^{-}$, and the same width, $\hat{w}_{1}=\hat{w}_{2}$, and need no
more dissection to be transformed into each other.

We have shown that $P_{1}$ and $P_{2}$ can be dissected into two congruent
rectangles whose height expansion uses $\hat{y}$, and into a larger number of
additional rectangles whose height expansion does not use $\hat{y}$. These
remaining rectangles have a smaller basis for their heights and (because we
have removed a congruent rectangle from each polygon) have equal Dehn
invariants. The result follows from the induction hypothesis.

##  8 Putting the pieces together

We are now ready to prove our main results:

######  Theorem 8.1.

The minimum number of rectangles into which an orthogonal polygon can be
dissected by axis-parallel cuts and translation equals the rank of its
orthogonal Dehn invariant.

######  Proof 8.2.

This number of rectangles is lower-bounded by the rank, by the discussion in
Section 5. If the rank is $r$, then there exists a set of $r$ rectangles with
the same invariant as the polygon, by Lemma 6.1. The given polygon can be
dissected into these rectangles, by Theorem 7.1.

######  Theorem 8.3.

We can compute the minimum number of rectangles into which an orthogonal
polygon can be dissected, given a representation for its coordinates over a
rational basis, in a polynomial number of rational-arithmetic operations. We
can construct a minimal set of rectangles into which it can be dissected, in a
polynomial number of operations using arithmetic over the given rational
basis.

######  Proof 8.4.

To compute the rank, we compute the Dehn invariant as described in Section 3,
and apply any polynomial-time algorithm for computing the rank of a rational-
number matrix, such as Gaussian elimination. To construct the rectangles, we
follow the steps in the proof of Lemma 6.1, which uses only a polynomial
number of operations involving comparing linear combinations of basis elements
and finding rational approximations to them.

We remark that, as well as counting rectangles, the rank of the orthogonal
Dehn invariant can also count vertices. Every set of $r$ disjoint rectangles
can be glued together to form an orthogonal polygon with $2r+2$ vertices, and
every orthogonal polygon with this many vertices can be sliced at its non-
convex vertices into $r$ rectangles. Therefore, the minimum number of vertices
that a polygon of Dehn rank $r$ can be orthogonally dissected into is $2r+2$.

##  9 Dissection into prototiles

Another use of the polyhedral Dehn invariant, besides dissection of one shape
into another, involves tiling. Any polyhedron that tiles space must have Dehn
invariant zero, and any polyhedron with Dehn invariant zero can be dissected
into a different polyhedron that tiles space. For the axis-parallel polygonal
Dehn invariant we study, things don’t work out quite so neatly. The Greek
cross can tile, but has nonzero Dehn invariant. More, any axis-parallel
polygon can be cut into multiple rectangles, and these can tile space
aperiodically by grouping them into rows of the same type of rectangle (Fig.
6). So the Dehn invariant cannot be used to prove that such a thing is
impossible, because it is always possible. If we could rotate pieces, we could
also rearrange certain sets of more than two rectangles, such as the three
rectangles of Fig. 2, into a single-piece axis-parallel hexagon that could
tile the plane periodically (Fig. 7).

Figure 6: Construction of a non-periodic tiling from an arbitrary dissection
into rectangles

However, for the orthogonal dissections considered here, without rotation, the
rank of the Dehn invariant does produce a limitation on the ability to tile
periodically without rotation:

######  Theorem 9.1.

An orthogonal polygon $P$, or any finite number of copies of $P$, has an
orthogonal dissection to a prototile that can tile the plane periodically if
and only if the rank of its Dehn invariant is at most two.

######  Proof 9.2.

If the rank of the Dehn invariant is one, $P$ can be dissected to a rectangle,
which tiles periodically. If the rank is two, $P$ can be dissected into two
rectangles, and reassembled into a hexagon, which (like the prototiles of Fig.
7) tile periodically.

Figure 7: With orthogonal rotations of pieces, the polygon of Fig. 2 can be
dissected to form the prototile of a periodic tiling of the plane.

Combining $n$ copies of $P$ multiplies the Dehn invariant by the scalar $n$,
which does not change the rank. Every periodic tiling of the plane has a
fundamental region in the shape of an axis-parallel hexagon, like the
prototiles of Fig. 7. (Because it tiles by translation, this fundamental
region may combine a finite number of prototiles of the tiling.) If copies of
$P$ could be dissected to the prototile of a tiling, they could also be
dissected to this fundamental region, which has Dehn invariant at most two.

In particular, as a shape whose Dehn invariant has rank three, the orthogonal
polygon of Fig. 2 has no orthogonal dissection to a prototile for a periodic
tiling of the plane.

##  10 Conclusions

We have shown that the rank of the orthogonal Dehn invariant of an orthogonal
polygon controls the number of rectangles into which it can be dissected by
axis-parallel slices and translation, leading to a polynomial time algorithm
to compute this number of rectangles or to construct an optimal set of
rectangles into which it can be dissected. The dissection itself may require a
non-polynomial number of pieces. The number of rectangles, in turn, controls
the ability to dissect a polygon into a shape that tiles the plane. One
natural question for future research is whether these results can be extended
to dissections that allow $90^{\circ}$ rotations.

The rank of the polyhedral Dehn invariant, similarly, provides a lower bound
on the number of edges of a polyhedron into which a given polyhedron may be
dissected, because every polyhedron’s Dehn invariant is defined as a sum of
tensors over its edges, with rank at most the number of edges in the sum. It
is tempting to guess that this lower bound provides a constant-factor
approximation to the minimum number of edges in a dissection, but we have been
unable to prove this. What would be needed is a construction of a polyhedron
with a given Dehn invariant and with a number of edges proportional to the
rank of the invariant, analogous to Lemma 6.1, but this is made more difficult
by the fact that not all tensors are realizable as polyhedral Dehn invariants.

Order-two tensors have additional invariants beyond their rank, obtained as
the coefficients of the characteristic polynomial or as any function of those
coefficients. (The rank can be obtained in this way from the difference in
degrees of the highest-degree and lowest-degree nonzero coefficients.) Our
work naturally raises the question: which of these invariants are meaningful
for dissection problems, and what do they mean?

## References

  * [1] David Benko.  A new approach to Hilbert’s third problem.  American Mathematical Monthly, 114(8):665–676, 2007.  doi:10.1080/00029890.2007.11920458.
  * [2] Wolfgang Bolyai.  Transmutatio figurarum quoad areas; et hinc reductio earum ad formam rectae.  In Tentamen iuventutem studiosam in elementa matheseos purae elementaris ac sublimioris methodo intuitiva evidentiaque huic propria introducendi, cum appendici triplici, volume 2, pages 108–111. Sumptibus Academiae Scientiarum Hungaricae, 2nd edition, 1904.  URL: https://archive.org/details/wolfgangibolyai01akadgoog/page/108/mode/2up.
  * [3] Max Dehn.  Ueber den Rauminhalt.  Mathematische Annalen, 55(3):465–478, 1901.  doi:10.1007/BF01448001.
  * [4] Max Dehn.  Über Zerlegung von Rechtecken in Rechtecke.  Mathematische Annalen, 57:314–332, 1903.  doi:10.1007/BF01444289.
  * [5] Johan L. Dupont.  Scissors congruences, group homology and characteristic classes, volume 1 of Nankai Tracts in Mathematics.  World Scientific, River Edge, New Jersey, 2001.  doi:10.1142/9789812810335.
  * [6] David Eppstein.  Graph-theoretic solutions to computational geometry problems.  In Christophe Paul and Michel Habib, editors, Graph-Theoretic Concepts in Computer Science, 35th International Workshop, WG 2009, Montpellier, France, June 24–26, 2009, Revised Papers, volume 5911 of Lecture Notes in Computer Science, pages 1–16, 2009.  doi:10.1007/978-3-642-11409-0_1.
  * [7] L. Ferrari, P. V. Sankar, and J. Sklansky.  Minimal rectangular partitions of digitized blobs.  Computer Vision, Graphics, and Image Processing, 28(1):58–71, 1984.  doi:10.1016/0734-189X(84)90139-7.
  * [8] Greg N. Frederickson.  Dissections: Plane & Fancy.  Cambridge University Press, 1997.  For the Greek cross to square dissection, see pp. 105–106.  doi:10.1017/CBO9780511574917.
  * [9] Paul Gerwien.  Zerschneidung jeder beliebigen Anzahl von gleichen geradlinigen Figuren in dieselben Stücke.  Journal für die reine und angewandte Mathematik, 10:228–234, January 1833.  doi:10.1515/crll.1833.10.228.
  * [10] Wolfgang Hackbusch.  Tensor Spaces and Numerical Tensor Calculus, volume 42 of Springer Series in Computational Mathematics.  Springer, 2012.  See in particular the identification of matrices with tensors on pp. 5, and 55–56, and the equivalence of multiple definitions of matrix rank on p. 23.  doi:10.1007/978-3-642-28027-6.
  * [11] W. H. Jackson.  Wallace’s theorem concerning plane polygons of the same area.  American Journal of Mathematics, 34(4):383–390, October 1912\.  doi:10.2307/2370498.
  * [12] Børge Jessen.  The algebra of polyhedra and the Dehn–Sydler theorem.  Mathematica Scandinavica, 22(2):241–256, 1968.  URL: https://www.jstor.org/stable/24489773, doi:10.7146/math.scand.a-10888.
  * [13] Menelaos I. Karavelas.  Exact geometric and algebraic computations in CGAL.  In Komei Fukuda, Joris van der Hoeven, Michael Joswig, and Nobuki Takayama, editors, Mathematical Software – ICMS 2010, Third International Congress on Mathematical Software, Kobe, Japan, September 13–17, 2010, Proceedings, volume 6327 of Lecture Notes in Computer Science, pages 96–99. Springer, 2010.  doi:10.1007/978-3-642-15582-6_20.
  * [14] Witold Lipski, Jr., Elena Lodi, Fabrizio Luccio, Cristina Mugnai, and Linda Pagli.  On two-dimensional data organization II.  Fundamenta Informaticae, 2:245–260, 1979.  doi:10.3233/FI-1978-2116.
  * [15] Kurt Mehlhorn and Stefan Schirra.  Exact computation with leda_real – theory and geometric applications.  In Götz Alefeld, Jiří Rohn, Siegfried Rump, and Tetsuro Yamamoto, editors, Symbolic Algebraic Methods and Verification Methods, pages 163–172. Springer, 2001.  doi:10.1007/978-3-7091-6280-4_16.
  * [16] T. Ohtsuki.  Minimum dissection of rectilinear regions.  In Proc. IEEE Int. Symp. Circuits and Systems, pages 1210–1213, 1982.
  * [17] Jeroen Spandaw.  Dissecting cuboids into cuboids.  American Mathematical Monthly, 111(5):425–429, 2004.  doi:10.2307/4145269.
  * [18] John Stillwell.  5.6: The Dehn invariant.  In Numbers and geometry, Undergraduate Texts in Mathematics, pages 161–165. Springer-Verlag, New York, 1998.  doi:10.1007/978-1-4612-0687-3.
  * [19] Jean-Pierre Sydler.  Conditions nécessaires et suffisantes pour l’équivalence des polyèdres de l’espace euclidien à trois dimensions.  Commentarii Mathematici Helvetici, 40:43–80, 1965.  doi:10.1007/bf02564364.
  * [20] William Wallace and John Lowry.  Question 269.  In Thomas Leybourn, editor, New Series of the Mathematical Repository, volume 3, pages 44–46. W. Glendinning, London, 1814.  URL: https://archive.org/details/mathematicalrep00leybgoog/page/n54.