# Extracting Temporal Event Relation with Syntax-guided Graph Transformer

Shuaicheng Zhang♣, Qiang Ning♠, Lifu Huang♣
♣Virginia Tech, ♠Amazon
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Extracting temporal relations (e.g., before, after, and simultaneous) among
events is crucial to natural language understanding. One of the key challenges
of this problem is that when the events of interest are far away in text, the
context in-between often becomes complicated, making it challenging to resolve
the temporal relationship between them. This paper thus proposes a new Syntax-
guided Graph Transformer network (SGT) to mitigate this issue, by (1)
explicitly exploiting the connection between two events based on their
dependency parsing trees, and (2) automatically locating temporal cues between
two events via a novel syntax-guided attention mechanism. Experiments on two
benchmark datasets, Matres and TB-Dense, show that our approach significantly
outperforms previous state-of-the-art methods on both end-to-end temporal
relation extraction and temporal relation classification; This improvement
also proves to be robust on the contrast set of Matres. The code is publicly
available at https://github.com/VT-NLP/Syntax-Guided-Graph-Transformer.

##  1 Introduction

Temporal relationship, e.g., Before, After, and Simultaneous, is important for
understanding the process of complex events and reasoning over them.
Extracting temporal relationship automatically from text is thus an important
component in many downstream applications, such as summarization Jiang et al.
(2011); Ng et al. (2014), dialog understanding and generation Ritter et al.
(2010); Sun et al. (2021), reading comprehension Harabagiu and Bejan (2005);
Sun et al. (2018); Ning et al. (2020); Huang et al. (2019) and future event
prediction Li et al. (2021); Lin et al. (2022). While event mentions can often
be detected reasonably well Lin et al. (2020); Huang and Ji (2020); Wang et
al. (2021, 2022), extracting event-event relationships, especially temporal
relationship, still remains challenging Chen et al. (2021).

Figure 1: Examples of temporal relation annotations. Event mentions are
boldfaced, the temporal relations between these events are listed below each
sentence, and the temporal cues deciding those temporal relations are
highlighted in red.  Figure 2: Architecture overview. The tokens highlighted
with red and blue colors in the Input Sentence show the source and target
events to be detected. The bold edges in the Input Graph Structure indicate
the triples from the dependency path between the source and target event
mentions as well as their surrounding context, and are considered by the
syntax-guided attention.

Recent studies Han et al. (2019b); Ning et al. (2017); Vashishtha et al.
(2019); Wang et al. (2020a) have shown improved performance in temporal
relation extraction by leveraging the contextual representations learned from
pre-trained language models Devlin et al. (2018); Liu et al. (2019). However,
one remaining challenge of this task is that it requires accurate
characterization of the connection between two event mentions and the cues
indicating their temporal relationship, especially when the context is wide
and complicated. For instance, by manually examining 200 examples of human
annotated temporal relations from the Matres Ning et al. (2018) dataset, we
find that about 52% of the temporal cues111Temporal cues refer to the words of
which the semantic meaning or related syntactic relations can determine the
temporal relation of two event mentions.  come from the connection between two
event mentions (e.g., S1 in Fig. 1), 39% from their surrounding contexts (S2
in Fig. 1) and the remaining 9% from others, e.g., event co-reference or
subordinate clause structures (S3 in Fig. 1).

Syntactic features, such as dependency parsing trees, have proved to be
effective in characterizing the connection of two event mentions in pre-neural
methods Chambers (2013); Chambers et al. (2014); Mirza and Tonelli (2016).
However, how to make use of these features has been under-explored since the
adoption of neural methods in this field. This paper closes this gap with a
novel Syntax-guided Graph Transformer (SGT) network – in addition to the
attention heads in a typical Graph Transformer, we bring in a new attention
mechanism that specifically looks at the path from a source node to a target
node over dependency parsing trees. SGT thus not only learns event
representations as in a typical Graph Transformer, but also provides a way to
represent syntactic dependency information between a pair of events (for
temporal relation extraction, this means attending to the aforementioned
temporal cues). We conduct experiments on two benchmark datasets, Matres Ning
et al. (2018) and TB-Dense Cassidy et al. (2014) on both end-to-end temporal
relation extraction and classification, which demonstrate the effectiveness of
SGT over previous state-of-the-art methods. Experiments on the contrast set
Gardner et al. (2020) of Matres further proves the robustness of our approach.

##  2 Approach

Figure 2 shows the overview of our approach. Given an input sentence
$\tilde{s}=[w_{1},w_{2},...,w_{n}]$ with $n$ tokens, we aim to detect a set of
event mentions $\\{e_{1},e_{2},...\\}$ where each event mention $e_{i}$ may
contain one or multiple tokens by leveraging the contextual representations
learned from a pre-trained BERT Devlin et al. (2018) encoder. Then, following
previous studies Ning et al. (2019, 2017); Han et al. (2019b); Wang et al.
(2020a), we consider each pair of event mentions that are detected from one or
two continuous sentences, and predict their temporal relationship.

To effectively capture the temporal cues between two event mentions, we build
a dependency graph from one or two input sentences and design a new Syntax-
guided Graph Transformer network to automatically learn a new contextual
representation for each event mention by considering the triples that they are
locally involved as well as the triples along the dependency path of the two
event mentions within the dependency graph. Finally, the two event mention
representations are concatenated to predict their temporal relationship.

###  2.1 Sequence Encoder

Given an input sentence $\tilde{s}=[w_{1},w_{2},...,w_{n}]$, we apply the same
tokenizer as BERT Devlin et al. (2018) to get all the subtokens. Then, we feed
the sequence of subtokens as input to a pre-trained BERT model to get a
contextual representation for each token $w_{i}$. If a token $w_{i}$ is split
into multiple subtokens, we use the contextual representation of the first
subtoken to represent $w_{i}$. To enrich the contextualized representations,
for each token, we create a one-hot Part-of-Speech (POS) tag vector and
concatenate it with BERT contextual embeddings. In this way, we obtain a final
representation $\boldsymbol{c}_{i}$222We use bold lower case symbols to denote
vectors. for each $w_{i}$. These representations will be later used for event
mention detection and also as the initial representations to our syntax-guided
graph transformer network.

###  2.2 Event Detection

To detect event mentions from the sentence, we take the contextual
representation of each word as input to a binary linear classifier to
determine whether it is an event mention or not, which is optimized by
minimizing the following binary cross-entropy loss:

$\displaystyle\tilde{\boldsymbol{y}}_{i}=\text{softmax}(\boldsymbol{W}_{eve}\boldsymbol{c}_{i}+\boldsymbol{b}_{eve})$
$\displaystyle\mathcal{L}_{eve}=-\sum_{\tilde{s}\in\mathcal{S}}\sum_{i=1}^{|\tilde{s}|}\sum_{\pi\in\\{0,1\\}}\alpha_{\pi}y_{i,\pi}\log(\tilde{y}_{i,\pi})$

where $\mathcal{L}_{eve}$ denotes the cross-entropy loss for event detection.
$\mathcal{S}$ is the set of sentences in the training dataset. $\alpha_{\pi}$
is a weight coefficient for each class (0 or 1) to mitigate the data imbalance
problem and $\alpha_{0}+\alpha_{1}=1$. $y_{i,\pi}$ is a binary indicator to
show whether $\pi$ is the same as the groundtruth binary label ($y_{i,\pi}=1$)
or not ($y_{i,\pi}=0$). $\tilde{y}_{i,\pi}$ denotes the probability of the
$i$-th token in $s$ being predicted with a binary class label $\pi$.
$\boldsymbol{W}_{eve}$ and $\boldsymbol{b}_{eve}$ are learnable parameters.

###  2.3 Syntax-guided Graph Transformer

From the example sentences in Fig. 1, the temporal cues for characterizing the
temporal relationship between two event mentions mainly come from their
surrounding contexts as well as their connections from their syntactic
dependency path. However, a sequence encoder usually fails to capture such
information, especially when the context between two event mentions is
complicated, thus we further design a new Syntax-guided Graph Transformer
(SGT) network.

Given a source event $e_{s}$ and a target event $e_{t}$ detected from one or
two continuous sentences, we apply a public dependency
parser333https://spacy.io/api/dependencyparser to parse each sentence into a
tree-graph and connect the graphs of two continuous sentences with an
arbitrary cross-sentence edge Peng et al. (2017); Cheng and Miyao (2017)
pointing from the root node of the preceding sentence to the root node of the
following one, and obtain a graph $G=(V,E).$ For each node $v_{i}$, we use
$\mathcal{N}_{i}^{in}=\\{(v_{k},r_{ki},v_{i})\in E|v_{k},v_{i}\in V\\}$ and
$\mathcal{N}^{out}_{i}=\\{(v_{i},r_{ij},v_{j})\in E|v_{i},v_{j}\in V\\}$ to
denote all the neighbor triples of $v_{i}$ with in-going and out-going edges
respectively, $r\in\Upsilon$ where $\Upsilon$ is the label set for syntactic
dependency relation, and use
$\mathcal{P}_{ij}=\\{(v_{i},r_{ig},v_{g}),...,(v_{h},r_{hj},v_{j})\\}$ as the
triple set along the path from $v_{i}$ to $v_{j}$.

#### Node Representation Initialization

For each node $v_{i}$ in graph $G$, we map it to a particular token
$w_{i^{{}^{\prime}}}$ from the original sentence and obtain a contextual
representation $\boldsymbol{c}_{i^{{}^{\prime}}}$ from the BERT encoder. Then,
we learn an initial node representation for each node $v_{i}$ as:

$\displaystyle\boldsymbol{h}^{0}_{i}=\boldsymbol{W}_{e}\boldsymbol{c}_{i^{{}^{\prime}}}+\boldsymbol{b}_{e}$

where $\boldsymbol{W}_{e}$ and $\boldsymbol{b}_{e}$ are learnable parameters.

#### Graph Multi-head Self-attention

Following transformer model Vaswani et al. (2017); Wang et al. (2020b), we
adapt the multi-head self-attention to learn a contextual representation for
each node in the graph $G$. Each node $v_{i}$ in graph $G$ is associated with
a set of neighbor triples $\mathcal{N}^{in}_{i}\cup\mathcal{N}^{out}_{i}$ and
a node representation $\boldsymbol{h}_{i}^{l-1}$ where $l$ is the index of a
layer in our transformer architecture. To perform self-attention, we first
apply a linear transformation to obtain a query vector based on each node
$v_{i}$, and employ another two linear transformations to get the key and
value vectors based on the node’s neighbor triples:

$\displaystyle\boldsymbol{Q}^{l}_{i}=\boldsymbol{W}_{q}^{m}\boldsymbol{h}^{l-1}_{i}$
$\displaystyle\boldsymbol{K}^{l}_{ij}=\boldsymbol{W}_{k}^{m}\boldsymbol{R}^{l-1}_{ij}$
$\displaystyle\boldsymbol{U}^{l}_{ij}=\boldsymbol{W}_{u}^{m}\boldsymbol{R}^{l-1}_{ij}$
$\displaystyle\boldsymbol{R}^{l-1}_{ij}=\boldsymbol{W}_{r}^{m}(\boldsymbol{h}^{l-1}_{i}\bigparallel\boldsymbol{r}_{ij}\bigparallel\boldsymbol{h}^{l-1}_{j})+\boldsymbol{b}_{r}^{m}$

where $m$ is the index of a particular head. $\boldsymbol{Q}^{l}_{i}$ denotes
a query vector corresponding to node $v_{i}$, $\boldsymbol{K}^{l}_{ij}$ and
$\boldsymbol{U}^{l}_{ij}$ is a key and value vector respectively, and both of
them are learned from a triple
$(v_{i},r_{ij},v_{j})\in\mathcal{N}^{in}_{i}\cup\mathcal{N}^{out}_{i}$, which
is represented as $\boldsymbol{R}_{ij}$. $m$ is the index of a particular
head. $\bigparallel$ denotes the concatenation operation.
$\boldsymbol{r}_{ij}$ denotes the representation of a particular relation
$r_{ij}$ between $v_{i}$ and $v_{j}$, which is randomly initialized and
optimized by the model. $\boldsymbol{W}_{q}^{m}$, $\boldsymbol{W}_{k}^{m}$,
$\boldsymbol{W}_{u}^{m}$, $\boldsymbol{W}_{r}^{m}$ and
$\boldsymbol{b}_{r}^{m}$ are learnable parameters.

For each node $v_{i}$, we then perform self-attention over all the neighbor
triples that it is involved, and compute a new context representation with
multiple attention heads:

$\displaystyle\boldsymbol{g}_{i}^{l}=(\bigparallel^{M}_{m}\boldsymbol{\text{Head}}^{m}_{i})\boldsymbol{W}_{o}$
$\displaystyle\boldsymbol{\text{Head}}^{m}_{i}=\text{softmax}(\frac{\boldsymbol{Q}^{l}_{i}(\boldsymbol{K}^{l})^{\top}}{\sqrt{d_{k}}})\boldsymbol{U}^{l}$

where $\boldsymbol{g}_{i}^{l}$ is the aggregated representation computed over
all neighbor triples of node $v_{i}$ with $M$ attention heads at $l$-th layer.
$\boldsymbol{g}_{i}^{l}$ will be later used to learn the updated
representation of node $v_{i}$. $\sqrt{d_{k}}$ is the scaling factor denoting
the dimension size of each key vector. $\boldsymbol{W}_{o}$ is a learnable
parameter.

#### Syntax-guided Attention

To automatically find the indicative temporal cues for two event mentions from
their connection as well as surrounding contexts, we design a new syntax-
guided attention mechanism. For two event nodes $v_{s}$ and $v_{t}$, we first
extract the set of nodes from the dependency path between $v_{s}$ and $v_{t}$
(including $v_{s}$ and $v_{t}$), which is denoted as $\Theta_{st}$. We then
get all the triples from the dependency path between $v_{s}$ and $v_{t}$ as
well as the triples that any node from $\Theta_{st}$ is involved, which are
denoted as
$\Phi_{st}=\cup_{v_{i}\in\Theta_{st}}\\{\mathcal{N}^{in}_{i}\cup\mathcal{N}^{out}_{i}\\}\cup\mathcal{P}_{st}$.
To compute the syntax-guided attention over all the triples from $\Phi_{st}$,
we apply three linear transformations to get the query, key and value vectors
where the query vector is obtained from the representation of two event
mentions, and key and value vectors are computed from the triples in
$\Phi_{st}$:

$\displaystyle\tilde{\boldsymbol{Q}}^{l}_{st}=\tilde{\boldsymbol{W}}_{q}^{m}\cdot(\boldsymbol{h}^{l-1}_{s}\bigparallel\boldsymbol{h}^{l-1}_{t})^{x}$
$\displaystyle\tilde{\boldsymbol{K}}^{l}_{ij}=\tilde{\boldsymbol{W}}_{k}^{m}\tilde{\boldsymbol{R}}^{l-1}_{ij}$
$\displaystyle\tilde{\boldsymbol{U}}^{l}_{ij}=\tilde{\boldsymbol{W}}_{u}^{m}\tilde{\boldsymbol{R}}^{l-1}_{ij}$
$\displaystyle\tilde{\boldsymbol{R}}^{l-1}_{ij}=\tilde{\boldsymbol{W}}_{r}^{m}(\boldsymbol{h}^{l-1}_{i}\bigparallel\boldsymbol{r}_{ij}\bigparallel\boldsymbol{h}^{l-1}_{j})+\tilde{\boldsymbol{b}}_{r}$

where $m$ is the index of a particular head,
$\tilde{\boldsymbol{Q}}^{l}_{st},\tilde{\boldsymbol{K}}^{l}_{ij},\tilde{\boldsymbol{U}}^{l}_{ij}$
denote the query, key and value vectors respectively.
$\tilde{\boldsymbol{R}}^{l-1}_{ij}$ is the representation of a triple
$(v_{i},r_{ij},v_{j})\in\Phi_{st}$. $\tilde{\boldsymbol{W}}_{q}^{m}$,
$\tilde{\boldsymbol{W}}_{k}^{m}$, $\tilde{\boldsymbol{W}}_{v}^{m}$ and
$\tilde{\boldsymbol{W}}_{r}^{m}$ are learnable parameters.

Given the query vector, we then compute the attention distribution over all
triples from $\Phi_{st}$ and get an aggregated representation to denote the
meaningful temporal features captured from the connection between two event
mentions and their surrounding contexts.

$\displaystyle\tilde{\boldsymbol{g}}_{st}^{l}=(\bigparallel^{M}_{m}\tilde{\text{Head}}^{m}_{st})\cdot\tilde{\boldsymbol{W}}_{p}$
$\displaystyle\tilde{\text{Head}}^{m}_{st}=\text{softmax}(\frac{\tilde{\boldsymbol{Q}}^{l}_{st}(\tilde{\boldsymbol{K}}^{l})^{\top}}{\sqrt{d_{k}}})\cdot\tilde{\boldsymbol{U}}^{l}$

where $\tilde{\boldsymbol{g}}_{st}^{l}$ is the aggregated temporal related
information from all the triples in $\Phi_{st}$ based on the syntax-guided
attention at $l$-th layer. $\boldsymbol{W}_{p}$ is a learnable parameter.

#### Node Representation Fusion

Each event node in graph $G$ will receive two representations learned from the
multi-head self-attention and syntax-guided attention, thus we further fuse
the two representations for both the source node $v_{s}$ and the target node
$v_{t}$:

$\displaystyle\boldsymbol{\hat{h}}_{s}^{l}=\tilde{\boldsymbol{W}}_{f}(\boldsymbol{g}_{s}^{l}\bigparallel\tilde{\boldsymbol{g}}_{st}^{l})\;,\;\;\boldsymbol{\hat{h}}_{t}^{l}=\tilde{\boldsymbol{W}}_{f}(\tilde{\boldsymbol{g}}_{st}^{l}\bigparallel\boldsymbol{g}_{t}^{l})$

where $\boldsymbol{g}_{s}^{l}$ and $\boldsymbol{g}_{t}^{l}$ denote the context
representations learned from the multi-head self-attention for $v_{s}$ and
$v_{t}$. $\tilde{\boldsymbol{g}}_{st}^{l}$ denotes the representation learned
from the triples from $\Phi_{st}$ using syntax-guided attention.
$\boldsymbol{\hat{h}}_{s}^{l}$ and $\boldsymbol{\hat{h}}_{t}^{l}$ are the
fused representations of $v_{s}$ and $v_{t}$, respectively.
$\tilde{\boldsymbol{W}}_{f}$ is a learnable parameter.

For each non-event node $v_{i}$, which only receives a context representation
$\boldsymbol{g}_{i}^{l}$ learned from the multi-head self-attention, we apply
a linear projection and get a new node representation:

$\displaystyle\boldsymbol{\hat{h}}_{i}^{l}=\boldsymbol{W}_{t}\boldsymbol{g}_{i}^{l}$

Our Syntax-guided Graph Transformer encoder is composed of a stack of multiple
layers, while each layer consists of the two attention mechanisms and the
fusion sub-layer. We use residual connection followed by LayerNorm for each
layer to get the final representations of all the nodes:

$\displaystyle\boldsymbol{H}^{l}=\text{LayerNorm}(\boldsymbol{\hat{H}}^{l}+\boldsymbol{H}^{l-1})$

###  2.4 Temporal Relation Prediction

To predict the temporal relation between two event mentions $e_{s}$ and
$e_{t}$, we concatenate the final hidden states of $v_{s}$ and $v_{t}$
obtained from the Syntax-guided Graph Transformer network, and apply a
Feedforward Neural Network (FNN) to predict their relationship

$\displaystyle\tilde{\boldsymbol{y}}_{st}=\text{softmax}(\boldsymbol{W}_{z}(\boldsymbol{h}^{L}_{s}\bigparallel\boldsymbol{h}^{L}_{t})+\boldsymbol{b}_{t})$

where $\tilde{\boldsymbol{y}}_{st}$ denotes the probabilities over all
possible temporal relations between event mentions $e_{s}$ and $e_{t}$.

The training objective is to minimize the following cross-entropy loss
function:

$\displaystyle\mathcal{L}_{rel}=-\sum_{st\in\Delta}\sum_{x\in
X}\beta_{x}y_{st,x}\text{log}(\tilde{y}_{st,x}))$

where $\Delta$ denotes the total set of event pairs for temporal relation
prediction and $X$ denotes the whole set of relation labels. $y_{st,x}$ is a
binary indicator (0 or 1) to show whether $x$ is the same as the groundtruth
label ($y_{st,x}=1$) or not ($y_{st,x}=0$). We also assign a weight
$\beta_{x}$ to each class to mitigate the label imbalance issue.

##  3 Experiment

###  3.1 Experimental Setup

We perform experiments on two public benchmark datasets for temporal relation
extraction: (1) TB-Dense Cassidy et al. (2014), which is a densely annotated
dataset with 6 types of relations: Before, After, Simultaneous, Includes,
Is_included and Vague. (2) Matres Ning et al. (2018), which annotates verb
event mentions along with 4 types of temporal relations: Before, After,
Simultaneous and Vague. Additionally, we use POS tag information from Matres
provided by Ning et al. (2019). For TB-Dense, we use spacy annotation for
predicting POS tag information which is based on Universal POS tag
set444https://spacy.io/api/data-formats. For both benchmark datasets, we use
the same train/dev/test splits as previous studies Ning et al. (2019, 2017);
Han et al. (2019a, b). Note that, for evaluation, similar as previous work, we
disregard the Vague relation from both datasets (in the evaluation phase, we
simply remove all ground truth Vague relation pairs). In addition, we will
only consider event pairs from adjacent sentences due to the fact that it will
require an exponential number of annotations if we also consider event pairs
from non-adjacent sentences, which is beyond the scope of this study. Table 1
shows statistics of the two datasets and Table 2 shows the label distribution.

Corpora | Train | Dev | Test
---|---|---|---
TB-Dense | # Documents | 22 | 5 | 9
# Relation Pairs | 4,032 | 629 | 1,427
Matres | # Documents | 255 | 20 | 25
# Relation Pairs | 13K | 2.6K | 837
Table 1: Data statistics for TB-Dense and Matres Labels | TB-Dense | Matres
---|---|---
Before | 384 | 26.9% | 417 | 49.8%
After | 274 | 19.2% | 266 | 31.8%
Includes | 56 | 3.9% | - | -
Is_Included | 53 | 3.7% | - | -
Simultaneous | 22 | 1.5% | 31 | 3.7%
Vague | 638 | 44.7% | 133 | 15.9%
Table 2: Label distribution for TB-Dense and Matres. For each dataset, the
first column shows the number of instances of each relation type while the
second column shows the percentage.

#### Implementation Details

For fair comparisons with previous baseline approaches, we use the pre-trained
bert-large-cased
model555https://huggingface.co/transformers/pretrained_models.html for fine-
tuning and optimize our model with BertAdam. We optimize the parameters with
grid search: training epoch 10, learning rate
$\in\\{3e\text{-}6,1e\text{-}5\\}$, training batch size $\in\\{16,32\\}$,
encoder layer size $\in\\{4,12\\}$, number of heads $\in\\{1,8\\}$. During
training, we first optimize the event extraction module for 5 epochs to warm
up, and then jointly optimize both event extraction and temporal relation
extraction modules using gold event pairs for another 5 epochs.

###  3.2 Results

Dataset |  Model | Pre-trained Model | Event Detection | Relation Extraction
---|---|---|---|---
TB-Dense |  HNP19 Han et al. (2019b) | BERT Base | 90.9 | 49.4
Our Approach | BERT Base | 91.0 | 51.8
Matres |  CogCompTime2.0 Ning et al. (2019) | BERT Base | 85.2 | 52.8
HNP19 Han et al. (2019b) | BERT Base | 87.8 | 59.6
Our Approach | BERT Base | 90.5 | 62.3

Table 3: Comparison of various approaches on joint event and relation
extraction with F-score (%). Note that HPN19 fixes BERT embeddings but relies
on BiLSTM to capture the contextual features.

Dataset | Model | Pre-trained Model | Relation Classification (F-score %)
---|---|---|---
TB-Dense | LSTM Cheng and Miyao (2017) | BERT Base | 62.2
HNP19 Han et al. (2019b) | BERT Base | 64.5
Our Approach | BERT Base | 66.7
PSL Zhou et al. (2020) | RoBERTa Large | 65.2
DEER Han et al. (2021) | RoBERTa Large | 66.8
Our Approach | BERT Large | 67.1
Matres | CogCompTime2.0 Ning et al. (2019) | BERT Base | 71.4
LSTM Cheng and Miyao (2017) | BERT Base | 73.4
HNP19 Han et al. (2019b) | BERT Base | 75.5
Our Approach | BERT Base | 79.3
HMHD20 Wang et al. (2020a) | RoBERTa Large | 78.8
DEER Han et al. (2021) | RoBERTa Large | 79.3
Our Approach | BERT Large | 80.3

Table 4: Comparison of various approaches on temporal relation classification
with gold event mentions as input.

We evaluate SGT against two public benchmark datasets under two settings: (1)
joint event and temporal relation extraction (Table 3); (2) temporal relation
classification, where the gold event mentions are known beforehand (Table 4).
Note in the “joint” setting, we adopt the same strategy proposed in Han et al.
(2019b): we first train the event extraction module, and then jointly optimize
both event extraction and temporal relation extraction (using gold event pairs
as input to ensure training quality) modules. Overall, we observe that our
approach significantly outperforms baseline systems in both settings, with up
to 7.9% absolute F-score gain on Matres and 2.4% on TB-Dense.

From Table 3, we see that our approach achieves better performance on event
detection than baseline methods though they are based on the same BERT
encoder. This is possibly because, during joint training, our approach
leverages the dependency parsing trees, which improves the contextual
representations of the BERT encoder. In Table 4, unlike other models which are
based on larger contextualized embeddings such as RoBERTa, our approach with
BERT base achieves comparable performance, and further surpasses the state-of-
the-art baseline methods using BERT-large embeddings, which demonstrate the
effectiveness of our Syntax-guided Graph Transformer network.

Some studies Ning et al. (2019); Han et al. (2019b); Wang et al. (2020a); Zhou
et al. (2020) focus on resolving the inconsistency in terms of the symmetry
and transitivity of the temporal relations. For example, if event A and event
B are predicted as Before, event B and event C are predicted as Before, then
if event A and event C are predicted as Vague or After, it will be considered
as inconsistent. However, our approach shows consistent predictions with few
inconsistent cases when Simultaneous relation is involved. This analysis also
demonstrates that our approach can correctly capture the temporal cues between
two event mentions.

Model |  Original Test |  Contrast |  Consistency
---|---|---|---
CogCompTime2.0 Ning et al. (2019) |  73.2 |  63.3 |  40.6
Our Approach |  77.0 |  64.8 |  49.8

Table 5: Evaluation on the contrast set of Matres. Original Test indicates the
accuracy on 100 examples sampled from the original Matres test set following
Gardner et al. (2020). Contrast shows the accuracy score on 401 examples
perturbed from the original 100 examples. Consistency is defined as the
percentage of the original 100 examples for which the model’s predictions of
the perturbed examples are all correct in the contrast set. Figure 3:
Comparison of the predictions from BERT, BERT-GT and our approach.

We also examine the correctness and robustness of our approach on a contrast
set of Matres Gardner et al. (2020), which is created with small manual
perturbation based on the original test set of Matres in a meaningful way,
such as rephrasing the sentence or simply changing a word of the sentence to
alter the relation type. The contrast set provides a local view of a model’s
decision boundary, thus it can be used to more accurately evaluate a model’s
true linguistic capabilities. Table 5 shows that our approach significantly
outperforms the baseline model on both the original test set and the
corresponding contrast set. The contrast consistency in Table 5 also indicates
how well a model’s decision boundary aligns with the actual decision boundary
of the test instances, based on which we can see that by explicitly capturing
temporal cues, our approach is more accurate and robust than the baseline
method.

#### Ablation Study

We further conduct ablation studies to compare the performance of our approach
with two ablated versions of our method: (1) BERT with Graph Transformer
(BERT-GT), for which we remove the syntaxic-guided attention and only rely on
the standard multi-head self-attention to obtain graph-based contextual
representations of two event mentions and then predict their relation; (2)
BERT, where we further remove the Graph Transformer, and only use the pre-
trained BERT language model to encode the sentence and predict the temporal
relationship of two event mentions based on their contextual representations.

Ablation | F-score (%) | Gain (%)
---|---|---
BERT-SGT | 79.3 | 0
BERT-GT | 77.5 | -2.0
BERT | 75.5 | -3.8
Table 6: Ablation study on Matres. We use BERT base as the comparison basis.

Table 6 also shows that by adding Graph Transformer, BERT-GT achieves 2.0%
absolute F-score improvement over the BERT baseline model, demonstrating the
benefit of dependency parsing trees to temporal relation prediction. By
further adding the new syntax-guided attention into Graph Transformer, the
absolute improvement on F-score (1.8%) shows the effectiveness of our new
Syntax-guided Graph Transformer and the importance of capturing temporal cues
from the connection of two event mentions as well as their surround contexts.

Figure 3 shows two examples as qualitative analysis. In S1, BERT mistakenly
predicts the temporal relation as Before probably because it’s confused by the
context word Before. However, by incorporating the dependency graph,
especially the triples {worked, prep, Before}, {Before, pcomp, retiring} and
the path between the two event mentions,
worked$\rightarrow$prep$\rightarrow$Before$\rightarrow$pcomp$\rightarrow$retiring,
both BERT-GT and our approach correctly determine the relation as After. In
S2, both BERT and BERT-GT mistakenly predict the temporal relation as Before
as the context between the two event mentions is very wide and complicated,
and these two event mentions are not close within the dependency graph.
However, by explicitly considering and understanding the connection between
the two event mentions,
$\textit{sought}_{e_{1}}$$\rightarrow$on$\rightarrow$Marmara$\rightarrow$was$\rightarrow$part$\rightarrow$Flotilla
$\rightarrow$sought${}_{e_{2}}$, our approach correctly predicts the temporal
relation between the two event mentions.

###  3.3 SGT on Temporal Cues

To analyze the source of temporal cues for relation prediction, we randomly
sample 100 correct event relation predictions given gold event mentions from
Matres and select the triple that has the highest temporal attention weight
from the last layer of the Syntax-guided Graph Transformer network as a
temporal cue candidate. We manually evaluate the validity of each temporal cue
candidate, and further analyze if the cue is from the dependency path between
two event mentions, their surrounding context, or both. Our analysis shows
that about 64% of the temporal cues are valid, 37% of them come from the
dependency path, 17% are from local context, and the remaining 10% are from
both. This verifies our initial observation that most of the temporal cues are
from the dependency path between two event mentions as well as their
surrounding context. It also demonstrates the effectiveness of our new syntax-
guided attention mechanism.

###  3.4 Impact of Wide Context

We further illustrate the impact of context width to both baseline model and
our approach. For fair comparison, we use three context width category,
[context length $<$ 10, 10 $<$ context length $<$ 20, context length $>$ 20 ].
As we can see in Fig. 4, the first category has 267 pairs, the second category
has 343 pairs and the third category has 817 pairs. From our results, we
observe that the BERT baseline cannot predict the temporal relation of two
event mentions with wide context but rather working well when the event
mentions are close to each other. Our model overall performs slightly worse in
the second category but in general is very good at predicting the temporal
relationship for the event mentions with short and context width. This also
proves the benefit of syntactic parsing trees to the prediction of temporal
relationship. For the second category where the context length is within [10,
20], the performance of our approach slightly drops due to two reasons: (1)
the training samples within this range are not as sufficient as the other two
categories; (2) for most event pairs from this category, their dependency path
is very long and there is no explicit temporal indicative features within
their context or dependency path, making it more difficult for the model to
predict their temporal relationship.

Figure 4: Context width analysis on TB-Dense. The X axis shows the number of
tokens between two events mentions. The left Y axis shows the data
distribution of each width category indicating with blue bars. The right Y
axis denotes the micro F-score for each width category. Figure 5: Types of
remaining errors

###  3.5 Remaining Errors

We randomly sample 100 classification errors from the output of our approach
and categorize them into four categories. As Figure 5 shows, the first
category is due to the complex or ambiguous context (54% of the total errors).
The second category is due to the complicated subordinate clause structure,
especially the clauses that are related to quote or reported speech, e.g., S2
in Figure 5. The third error category is that our approach cannot correctly
differentiate the actual events from the hypothetical and intentional events,
while in most cases, the temporal relation among hypothetical and intentional
events is annotated as Vague. The last category is due to the lack of
sufficient annotation. We observe that none of the Simultaneous relation can
be correctly predicted for Matres dataset as the percentage of Simultaneous
(3.7%) is much lower than other relation types. In TB-Dense dataset, labels
are even more imbalanced as the percentage of Vague relation is over 50% while
the percentage of Includes, Is_Included and Simultaneous are all less than 4%.

##  4 Related Work

Early studies on temporal relation extraction mainly model it as a pairwise
classification problem Mani et al. (2006); Verhagen et al. (2007); Verhagen
and Pustejovsky (2008); Verhagen et al. (2010); Bethard et al. (2016);
MacAvaney et al. (2017) and rely on hand-crafted features and rules Verhagen
and Pustejovsky (2008); Bethard et al. (2007) to extract temporal event
relations. Recently, deep neural networks Dligach et al. (2017); Tourille et
al. (2017) and large-scale pre-trained language models Han et al. (2019a,
2021); Wang et al. (2020a); Zhou et al. (2020) are further employed and show
state-of-the-art performance.

Similar to our approach, several studies Ling and Weld (2010); Nikfarjam et
al. (2013); Mirza and Tonelli (2016); Meng et al. (2017); Cheng and Miyao
(2017); Huang et al. (2017) also explored syntactic path between two events
for temporal relation extraction. Different from previous work, our approach
considers three important sources of temporal cues: local context, denoting
the neighbors of each event node within the dependency graph; connection of
two event mentions, which is based on the dependency path between two event
mentions; and rich semantics of concepts and dependency relations, for
example, the dependency relation nmod between two event mentions usually
indicates a Before relationship. All these indicative features are
automatically selected and aggregated with the multi-head self-attention and
our new syntax-guided attention mechanism.

Our work is also related to the variants of Graph Neural Networks (GNN) Kipf
and Welling (2016); Veličković et al. (2018); Zhou et al. (2018), especially
Graph Transformer Yun et al. (2019); Chen et al. (2019); Hu et al. (2020);
Wang et al. (2020b). Different from previous GNNs which aim to capture the
context from neighbors of each node within the graph, in our task, we aim to
select and capture the most meaningful temporal cues for two event mentions
from their connections within the graph as well as their surrounding contexts.

##  5 Conclusion

Temporal relationship between events is important for understanding stories
described in natural language text, and a main challenge is how to discover
and make use of the connection between two event mentions, especially when the
event pair is far apart in text. This paper proposes a novel Syntax-guided
Graph Transformer (SGT) that represents the connection between an event pair
via additional attention heads over dependency parsing trees. Experiments on
benchmarking datasets, Matres, TB-Dense, and a contrast set of Matres, show
that our approach significantly outperforms previous state-of-the-art methods
in a variety of settings, including event detection, temporal relation
classification (where events are given), and temporal relation extraction
(where events are predicted). In the future, we will investigate the potential
of this approach to other relation extraction tasks.

## Acknowledgements

We thank the anonymous reviewers and area chair for their valuable time and
constructive comments. We also thank the support from the Amazon Research
Awards.

## References

  * Bethard et al. (2007) S. Bethard, J. H. Martin, and S. Klingenstein. 2007.  Timelines from text: Identification of syntactic temporal relations.  In _International Conference on Semantic Computing (ICSC 2007)_ , pages 11–18.
  * Bethard et al. (2016) Steven Bethard, Guergana Savova, Wei-Te Chen, Leon Derczynski, James Pustejovsky, and Marc Verhagen. 2016.  Semeval-2016 task 12: Clinical tempeval.  In _Proceedings of the 10th International Workshop on Semantic Evaluation (SemEval-2016)_ , pages 1052–1062.
  * Cassidy et al. (2014) Taylor Cassidy, Bill McDowell, Nathanel Chambers, and Steven Bethard. 2014.  An annotation framework for dense event ordering.  Technical report, CARNEGIE-MELLON UNIV PITTSBURGH PA.
  * Chambers (2013) Nathanael Chambers. 2013.  NavyTime: Event and time ordering from raw text.  In _Second Joint Conference on Lexical and Computational Semantics (*SEM), Volume 2: Proceedings of the Seventh International Workshop on Semantic Evaluation (SemEval 2013)_ , pages 73–77, Atlanta, Georgia, USA. Association for Computational Linguistics.
  * Chambers et al. (2014) Nathanael Chambers, Taylor Cassidy, Bill McDowell, and Steven Bethard. 2014.  Dense event ordering with a multi-pass architecture.  _Transactions of the Association for Computational Linguistics_ , 2:273–284.
  * Chen et al. (2019) Benson Chen, Regina Barzilay, and Tommi Jaakkola. 2019.  Path-augmented graph transformer network.  _arXiv preprint arXiv:1905.12712_.
  * Chen et al. (2021) Muhao Chen, Hongming Zhang, Qiang Ning, Manling Li, Heng Ji, Kathleen McKeown, and Dan Roth. 2021.  Event-centric natural language processing.  In _Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Natural Language Processing: Tutorial Abstracts_ , pages 6–14, Online. Association for Computational Linguistics.
  * Cheng and Miyao (2017) Fei Cheng and Yusuke Miyao. 2017.  Classifying temporal relations by bidirectional lstm over dependency paths.  In _Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers)_ , pages 1–6.
  * Devlin et al. (2018) Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. 2018.  Bert: Pre-training of deep bidirectional transformers for language understanding.  _arXiv preprint arXiv:1810.04805_.
  * Dligach et al. (2017) Dmitriy Dligach, Timothy Miller, Chen Lin, Steven Bethard, and Guergana Savova. 2017\.  Neural temporal relation extraction.  In _Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 2, Short Papers_ , pages 746–751.
  * Gardner et al. (2020) Matt Gardner, Yoav Artzi, Victoria Basmov, Jonathan Berant, Ben Bogin, Sihao Chen, Pradeep Dasigi, Dheeru Dua, Yanai Elazar, Ananth Gottumukkala, Nitish Gupta, Hannaneh Hajishirzi, Gabriel Ilharco, Daniel Khashabi, Kevin Lin, Jiangming Liu, Nelson F. Liu, Phoebe Mulcaire, Qiang Ning, Sameer Singh, Noah A. Smith, Sanjay Subramanian, Reut Tsarfaty, Eric Wallace, Ally Zhang, and Ben Zhou. 2020.  Evaluating models’ local decision boundaries via contrast sets.  In _Findings of the Association for Computational Linguistics: EMNLP 2020_ , pages 1307–1323, Online. Association for Computational Linguistics.
  * Han et al. (2019a) Rujun Han, I-Hung Hsu, Mu Yang, Aram Galstyan, Ralph Weischedel, and Nanyun Peng. 2019a.  Deep structured neural network for event temporal relation extraction.  In _Proceedings of the 23rd Conference on Computational Natural Language Learning (CoNLL)_ , pages 666–106, Hong Kong, China. Association for Computational Linguistics.
  * Han et al. (2019b) Rujun Han, Qiang Ning, and Nanyun Peng. 2019b.  Joint event and temporal relation extraction with shared representations and structured prediction.  In _Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP)_ , pages 434–444, Hong Kong, China. Association for Computational Linguistics.
  * Han et al. (2021) Rujun Han, Xiang Ren, and Nanyun Peng. 2021.  ECONET: Effective continual pretraining of language models for event temporal reasoning.  In _Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing_ , pages 5367–5380, Online and Punta Cana, Dominican Republic. Association for Computational Linguistics.
  * Harabagiu and Bejan (2005) Sanda Harabagiu and Cosmin Adrian Bejan. 2005.  Question answering based on temporal inference.  In _Proceedings of the AAAI-2005 workshop on inference for textual question answering_ , pages 27–34.
  * Hu et al. (2020) Ziniu Hu, Yuxiao Dong, Kuansan Wang, and Yizhou Sun. 2020.  Heterogeneous graph transformer.  In _Proceedings of The Web Conference 2020_ , pages 2704–2710.
  * Huang et al. (2019) Lifu Huang, Ronan Le Bras, Chandra Bhagavatula, and Yejin Choi. 2019.  Cosmos qa: Machine reading comprehension with contextual commonsense reasoning.  _arXiv preprint arXiv:1909.00277_.
  * Huang and Ji (2020) Lifu Huang and Heng Ji. 2020.  Semi-supervised new event type induction and event detection.  In _Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP)_ , pages 718–724.
  * Huang et al. (2017) Lifu Huang, Avirup Sil, Heng Ji, and Radu Florian. 2017.  Improving slot filling performance with attentive neural networks on dependency structures.  _arXiv preprint arXiv:1707.01075_.
  * Jiang et al. (2011) Yexi Jiang, Chang-Shing Perng, and Tao Li. 2011.  Natural event summarization.  In _Proceedings of the 20th ACM international conference on Information and knowledge management_ , pages 765–774.
  * Kipf and Welling (2016) Thomas N Kipf and Max Welling. 2016.  Semi-supervised classification with graph convolutional networks.  _arXiv preprint arXiv:1609.02907_.
  * Li et al. (2021) Manling Li, Sha Li, Zhenhailong Wang, Lifu Huang, Kyunghyun Cho, Heng Ji, Jiawei Han, and Clare Voss. 2021.  The future is not one-dimensional: Complex event schema induction by graph modeling for event prediction.  In _Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing_ , pages 5203–5215.
  * Lin et al. (2022) Li Lin, Yixin Cao, Lifu Huang, Shuang Li, Xuming Hu, Lijie Wen, and Jianmin Wang. 2022.  Inferring commonsense explanations as prompts for future event generation.  _arXiv preprint arXiv:2201.07099_.
  * Lin et al. (2020) Ying Lin, Heng Ji, Fei Huang, and Lingfei Wu. 2020.  A joint neural model for information extraction with global features.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 7999–8009.
  * Ling and Weld (2010) Xiao Ling and Daniel Weld. 2010.  Temporal information extraction.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , volume 24.
  * Liu et al. (2019) Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer, and Veselin Stoyanov. 2019.  Roberta: A robustly optimized bert pretraining approach.  _arXiv preprint arXiv:1907.11692_.
  * MacAvaney et al. (2017) Sean MacAvaney, Arman Cohan, and Nazli Goharian. 2017.  Guir at semeval-2017 task 12: a framework for cross-domain clinical temporal information extraction.  In _Proceedings of the 11th International Workshop on Semantic Evaluation (SemEval-2017)_ , pages 1024–1029.
  * Mani et al. (2006) Inderjeet Mani, Marc Verhagen, Ben Wellner, Chungmin Lee, and James Pustejovsky. 2006.  Machine learning of temporal relations.  In _Proceedings of the 21st International Conference on Computational Linguistics and 44th Annual Meeting of the Association for Computational Linguistics_ , pages 753–760.
  * Meng et al. (2017) Yuanliang Meng, Anna Rumshisky, and Alexey Romanov. 2017.  Temporal information extraction for question answering using syntactic dependencies in an LSTM-based architecture.  In _Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing_ , pages 887–896, Copenhagen, Denmark. Association for Computational Linguistics.
  * Mirza and Tonelli (2016) Paramita Mirza and Sara Tonelli. 2016.  Catena: Causal and temporal relation extraction from natural language texts.  In _Proceedings of COLING 2016, the 26th International Conference on Computational Linguistics: Technical Papers_ , pages 64–75.
  * Ng et al. (2014) Jun Ping Ng, Yan Chen, Min-Yen Kan, and Zhoujun Li. 2014.  Exploiting timelines to enhance multi-document summarization.  In _Proceedings of the 52nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 923–933.
  * Nikfarjam et al. (2013) Azadeh Nikfarjam, Ehsan Emadzadeh, and Graciela Gonzalez. 2013.  Towards generating a patient’s timeline: extracting temporal relationships from clinical notes.  _Journal of biomedical informatics_ , 46:S40–S47.
  * Ning et al. (2017) Qiang Ning, Zhili Feng, and Dan Roth. 2017.  A structured learning approach to temporal relation extraction.  In _Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing_ , pages 1027–1037, Copenhagen, Denmark. Association for Computational Linguistics.
  * Ning et al. (2019) Qiang Ning, Sanjay Subramanian, and Dan Roth. 2019.  An improved neural baseline for temporal relation extraction.  In _Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP)_ , pages 6203–6209, Hong Kong, China. Association for Computational Linguistics.
  * Ning et al. (2020) Qiang Ning, Hao Wu, Rujun Han, Nanyun Peng, Matt Gardner, and Dan Roth. 2020.  TORQUE: A reading comprehension dataset of temporal ordering questions.  In _Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP)_ , pages 1158–1172, Online. Association for Computational Linguistics.
  * Ning et al. (2018) Qiang Ning, Hao Wu, and Dan Roth. 2018.  A multi-axis annotation scheme for event temporal relations.  In _ACL_.
  * Peng et al. (2017) Nanyun Peng, Hoifung Poon, Chris Quirk, Kristina Toutanova, and Wen-tau Yih. 2017\.  Cross-sentence n-ary relation extraction with graph lstms.  _Transactions of the Association for Computational Linguistics_ , 5:101–115.
  * Ritter et al. (2010) Alan Ritter, Colin Cherry, and William B Dolan. 2010.  Unsupervised modeling of twitter conversations.  In _Human Language Technologies: The 2010 Annual Conference of the North American Chapter of the Association for Computational Linguistics_ , pages 172–180.
  * Sun et al. (2021) Yajing Sun, Yong Shan, Chengguang Tang, Yue Hu, Yinpei Dai, Jing Yu, Jian Sun, Fei Huang, and Luo Si. 2021.  Unsupervised learning of deterministic dialogue structure with edge-enhanced graph auto-encoder.  In _Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021_ , pages 13869–13877. AAAI Press.
  * Sun et al. (2018) Yawei Sun, Gong Cheng, and Yuzhong Qu. 2018.  Reading comprehension with graph-based temporal-casual reasoning.  In _Proceedings of the 27th International Conference on Computational Linguistics_ , pages 806–817.
  * Tourille et al. (2017) Julien Tourille, Olivier Ferret, Aurelie Neveol, and Xavier Tannier. 2017.  Neural architecture for temporal relation extraction: A bi-lstm approach for detecting narrative containers.  In _Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers)_ , pages 224–230.
  * Vashishtha et al. (2019) Siddharth Vashishtha, Benjamin Van Durme, and Aaron Steven White. 2019.  Fine-grained temporal relation extraction.  In _Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics_ , pages 2906–2919, Florence, Italy. Association for Computational Linguistics.
  * Vaswani et al. (2017) Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. 2017.  Attention is all you need.  _arXiv preprint arXiv:1706.03762_.
  * Veličković et al. (2018) Petar Veličković, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Liò, and Yoshua Bengio. 2018.  Graph Attention Networks.  _International Conference on Learning Representations_.  Accepted as poster.
  * Verhagen et al. (2007) Marc Verhagen, Robert Gaizauskas, Frank Schilder, Mark Hepple, Graham Katz, and James Pustejovsky. 2007.  Semeval-2007 task 15: Tempeval temporal relation identification.  In _Proceedings of the fourth international workshop on semantic evaluations (SemEval-2007)_ , pages 75–80.
  * Verhagen and Pustejovsky (2008) Marc Verhagen and James Pustejovsky. 2008.  Temporal processing with the tarsqi toolkit.  In _COLING 2008: Companion Volume: Demonstrations_ , pages 189–192.
  * Verhagen et al. (2010) Marc Verhagen, Roser Sauri, Tommaso Caselli, and James Pustejovsky. 2010.  Semeval-2010 task 13: Tempeval-2.  In _Proceedings of the 5th international workshop on semantic evaluation_ , pages 57–62.
  * Wang et al. (2020a) Haoyu Wang, Muhao Chen, Hongming Zhang, and Dan Roth. 2020a.  Joint constrained learning for event-event relation extraction.  In _Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP)_ , pages 696–706, Online. Association for Computational Linguistics.
  * Wang et al. (2021) Sijia Wang, Mo Yu, Shiyu Chang, Lichao Sun, and Lifu Huang. 2021.  Query and extract: Refining event extraction as type-oriented binary decoding.  _arXiv preprint arXiv:2110.07476_.
  * Wang et al. (2022) Sijia Wang, Mo Yu, and Lifu Huang. 2022.  The art of prompting: Event detection based on type specific prompts.  _arXiv preprint arXiv:2204.07241_.
  * Wang et al. (2020b) Tianming Wang, Xiaojun Wan, and Hanqi Jin. 2020b.  Amr-to-text generation with graph transformer.  _Transactions of the Association for Computational Linguistics_ , 8:19–33.
  * Yun et al. (2019) Seongjun Yun, Minbyul Jeong, Raehyun Kim, Jaewoo Kang, and Hyunwoo J Kim. 2019.  Graph transformer networks.  _Advances in neural information processing systems_ , 32.
  * Zhou et al. (2018) Jie Zhou, Ganqu Cui, Zhengyan Zhang, Cheng Yang, Zhiyuan Liu, Lifeng Wang, Changcheng Li, and Maosong Sun. 2018.  Graph neural networks: A review of methods and applications.  _arXiv preprint arXiv:1812.08434_.
  * Zhou et al. (2020) Yichao Zhou, Yu Yan, Rujun Han, J Harry Caufield, Kai-Wei Chang, Yizhou Sun, Peipei Ping, and Wei Wang. 2020.  Clinical temporal relation extraction with probabilistic soft logic regularization and global inference.  _arXiv preprint arXiv:2012.08790_.


11institutetext: TU Wien, Vienna, Austria 22institutetext: SRI International,
Menlo Park, CA, USA
22email<EMAIL_ADDRESS>
# MCSat-based Finite Field Reasoning in the Yices2 SMT Solver

Thomas Hader 11 Daniela Kaufmann 11 Ahmed Irfan 22
Stéphane Graham-Lengrand 22 Laura Kovács 11

###### Abstract

This system description introduces an enhancement to the Yices2 SMT solver,
enabling it to reason over non-linear polynomial systems over finite fields.
Our reasoning approach fits into the model-constructing satisfiability (MCSat)
framework and is based on zero decomposition techniques, which find finite
basis explanations for theory conflicts over finite fields. As the MCSat
solver within Yices2 can support (and combine) several theories via theory
plugins, we implemented our reasoning approach as a new plugin for finite
fields and extended Yices2’s frontend to parse finite field problems, making
our implementation the first MCSat-based reasoning engine for finite fields.
We present its evaluation on finite field benchmarks, comparing it against
cvc5. Additionally, our work leverages the modular architecture of the MCSat
solver in Yices2 to provide a foundation for the rapid implementation of
further reasoning techniques for this theory.

###### Keywords:

SMT solving MCSat finite fields polynomial arithmetic

##  1 Introduction

Satisfiability Modulo Theories (SMT) solving plays a crucial role in automated
reasoning as it combines the power of Boolean satisfiability (SAT) with
various mathematical background theories [3]. This connection enables the
automated verification and synthesis of systems [16] that require reasoning in
more expressive logical theories, for example real/integer arithmetic.

State-of-the-art SMT solvers employ a combination of Boolean level reasoning
and theory-specific algorithms. This is achieved either through the use of the
CDCL(T) paradigm [20] or the model-constructing satisfiability (MCSat)
approach [15, 11]. The MCSat algorithm lifts the Boolean-level CDCL algorithm
to the theory level, while keeping the search theory independent. This
approach is particularly effective for handling complex arithmetic theories.
For instance, Yices2 [5] uses the MCSat approach to handle non-linear
arithmetic constraints.

Finite fields offer an ideal framework for modeling bounded machine
arithmetic, particularly relevant in the context of contemporary cryptosystems
utilized in system security and post-quantum cryptography. Current
methodologies, for instance, develop private and secure systems using zero-
knowledge (ZK) proofs [7] or authenticate blockchain technologies like smart
contracts [21]. Verifying applications in such areas require efficient SMT
solvers that support reasoning over finite field arithmetic, e.g.,
verification of a compiler for ZK proofs [19].

#### Related Work.

Currently, the related work on SMT solving in finite field arithmetic is still
rather limited. Our own theoretical work [9] on MCSat approaches based on
finding zero decompositions comes with a proof-of-concept implementation that
facilitates only a very fundamental MCSat algorithm, has only limited support
of Boolean propagation, and is unable to parse SMTlib 2 [2].

The only other SMT solver that we are aware of being capable of reasoning over
finite fields is cvc5 [18, 1], which uses a classical CDCL(T) approach. As a
theory engine, Gröbner bases [4] reasoning over a set of polynomial equalities
is applied. If the derived Gröbner basis contains the constant $1$, then the
system is unsatisfiable and a conflict core for the CDCL(T) search can be
found. Otherwise, a guided enumeration of all possible solutions is performed
to search for a model.

Note that both approaches [9, 18] use complementary techniques. On the one
hand, Gröbner bases are highly engineered to find conflicts in the polynomial
input, which tends to help for unsatisfiable instances [18]. On the other
hand, a model constructing approach tends to be fast whenever there is a
solution, especially when there is a high number of models [9].

We further note that at the moment our implementation in Yices2, as well as
cvc5, is restricted to finite fields where the order (i.e. size) is prime.
This is a sufficient limitation for many applications in cryptosystems and ZK
proofs.

#### Contributions.

We present an integration of the theory of non-linear finite field arithmetic
in the Yices2 SMT solver [5], enabling it to reason over finite field
problems. This includes the following contributions which we will further
explain throughout the rest of this paper:

  * •

Adding the parsing of finite field problems to the Yices2 SMTlib 2 front-end
(Section 3).

  * •

Representing finite field polynomials as terms in Yices2 and implementing
features regarding such polynomials in the LibPoly library [12], which is the
library used for polynomials in Yices2 (Section 4).

  * •

Implementing and evaluating an MCSat theory back-end for finite field
reasoning, using existing concepts from non-linear real and bit-vector solving
from Yices2 (Section 5).

To the best of our knowledge, our work is currently the only finite field
instantiation of MCSat. While our initial theory reasoning approach follows
closely the explanation generation procedure of our previous work [9], our
implementation allows easy drop-in of an improved explanation procedure in the
future.

##  2 Preliminaries

In mathematics, a finite field is a field that contains a finite number of
elements. A finite field $\mathbb{F}_{p}$ of prime order $p$ can roughly be
seen as the representation of the integers modulo the prime $p$. We refer to
[9, 18] for details on the theory and representation of finite fields.

For SMT solving in finite fields, we are interested in the following problem:
Given a finite field $\mathbb{F}_{p}$, where $p$ is a prime number, let
$X=x_{1},\ldots x_{n}$, let $F$ be a set of polynomial constraints in
$\mathbb{F}_{p}[X]$ and $\mathcal{F}$ a formula following the logical
structure: $\mathcal{F}\quad=\quad\bigwedge_{C\subseteq F}\bigvee_{f\in
C}f\quad=\quad\bigwedge_{C\subseteq F}\bigvee_{f\in
C}\mathsf{poly}(f)\vartriangleright
0\quad\text{with}\vartriangleright\in\\{=,\neq\\}.$ _SMT solving over finite
fields:_ Does an assignment
$\nu:\\{x_{1},\dots,x_{n}\\}\rightarrow\mathbb{F}_{p}^{n}$ exist that
satisfies $\mathcal{F}$?

For example, the formula $\mathcal{F}_{1}=(x-1=0\lor y-1=0)\land(xy-1=0)$ is
satisfied by the assignment $x\mapsto 1,y\mapsto 1$ in $\mathbb{F}_{3}$;
whereas the formula $\mathcal{F}_{2}=(x-1=0\lor
y-1=0)\land(xy-1=0)\land(x-2=0)$ is unsatisfiable in $\mathbb{F}_{3}$.

#### Yices2 and MCSat.

Yices2 contains two main solvers, one based on the traditional CDCL(T)
approach [17] and one based on the MCSat approach [14, 15]. Yices2’s common
API and front-ends can automatically select which solver to use at runtime,
depending on an SMTlib 2 logic. In particular, when non-linear real or integer
arithmetic constraints are present Yices2 selects the MCSat solver. The MCSat
solver in Yices2 currently supports the theories of non-linear real arithmetic
(QF_NRA) [14] and integer arithmetic (QF_NIA) [10], bit-vectors (QF_BV) [8],
equality and uninterpreted functions (QF_EUF), arrays [6], and combinations
thereof.

In contrast to CDCL(T) that _complements_ CDCL with theory reasoning, MCSat
applies CDCL-like mechanisms to _perform_ theory reasoning. Specifically, it
explicitly and incrementally constructs models with first-order variable
assignments—maintained in a _trail_ —while maintaining the invariant that none
of the constraints evaluate to false. MCSat decides upon such assignments when
there is choice, it can propagate them when there is not, and it backtracks
upon conflict. The lemmas learned upon backtracking are based on theory-
specific explanations of conflicts and propagations. This theory-specific
reasoning is implemented through _plugins_ that provide interfaces to make
decisions, perform propagations, and produce explanations.

##  3 Usability of SMT Solving in Finite Fields

Currently, the support for finite fields in Yices2 exists on a
fork111Available at https://github.com/Ovascos/yices2 and will be merged into
the upstream code-base for the next release. It can be compiled and run
following the regular Yices2 documentation. The theory of finite fields can be
accessed using a not-yet official extension of the SMTlib 2 language (.smt2).

#### SMTlib 2 Parsing.

Extending the parser to handle finite field problems was our first extension
to Yices2. Currently, polynomials over finite fields are no official theory in
SMTlib 2 [2]. However, when implementing finite field support in cvc5 [1], an
extension was proposed in [18]. In the interest of keeping inputs and
benchmarks comparable, we aimed at a compatible implementation.

In the SMTlib 2 extension, the theory of (quantifier-free) non-linear finite
field reasoning is denoted as QF_FF. Elements can be defined using the sort
FiniteField. The sort is indexed by the order of the finite field, which is
required to be a prime number. For instance (_ FiniteField 3) defines the
finite field of order $3$. Constants are indexed with the field order to
indicate which finite field they belong in, e.g., (_ ff2 3). Note that the
integer following ff is interpreted modulo the field order. As a short-cut to
avoid rewriting the field order over and over again, the as keyword can be
used to interpret the constant in the correct field type: (as ff2 FF3) for a
defined finite field sort FF3. To specify the finite field operations ff.mul
and ff.add are available for multiplication and addition of finite field
values, respectively. Both support an arbitrary number of operators. Atoms
with finite field terms can be = with its respective meaning. For example, an
encoding of $\mathcal{F}_{1}$ can be seen in Fig. 1.

⬇

(set-logic QF_FF)

(define-sort FF3 () (_ FiniteField 3))

(declare-fun x () FF3)

(declare-fun y () FF3)

(assert (and

(or (= (ff.add x (as ff-1 FF3)) (as ff0 FF3))

(= (ff.add y (as ff-1 FF3)) (as ff0 FF3)))

(= (ff.mul x y) (as ff-1 FF3))))

(check-sat)

Figure 1: Example for an SMTlib 2 encoding of a finite field problem
$\mathcal{F}_{1}$.

##  4 Implementation Details

#### The Implementation of MCSat in Yices2.

The MCSat solver in Yices2 supports multiple theories via a notion of theory
_plugin_ that builds upon an earlier architecture [11]. An MCSat theory plugin
in Yices2 implements a number of functionalities that are given to the main
MCSat solver as function pointers. The main MCSat loop calls these functions
for theory-specific operations such as deciding or propagating the value of
variables or getting explanation lemmas, or upon certain events such as the
creation of new terms and lemmas. In return, a theory plugin can access
theory-generic mechanisms for, e.g., inspecting the MCSat trail, creating
variables and requesting to be notified of certain events like variable
assignments, as well as raising conflicts. A theory plugin is not required to
implement mechanisms for propagating theory assignments and explaining them,
but for the current theories in Yices2, such propagations have provided
noticeable speed-ups (see, e.g., [8]).

#### The Finite Field MCSat Plugin.

Before handling constraints in the finite field MCSat plugin, the input
assertions are represented as polynomial constraints. Limited preprocessing
(e.g., constant propagation) is performed at this step. Since there is no
inherent order on finite fields, polynomial constraints presented to the
plugin are either equalities $p=0$ or disequalities $p\neq 0$ for a finite
field polynomial $p$. The implementation of the finite field plugin follows an
approach similar to the plugin for non-linear arithmetic [10].

Using the MCSat trail, the finite field plugin reads which constraints must be
fulfilled at any given time (as decided or deduced by the Boolean plugin) and
tracks the assignment of values to polynomial variables. It also tracks, for
each polynomial variable, the _set of feasible values_ that the variable can
be assigned without any of the polynomial constraints evaluating to false:
Using watch lists, it detects when any of the constraints becomes _unit_ ,
i.e. when all of its variables but one have been assigned values. Upon such
detection, it computes how the constraint restricts the set of feasible values
for the last remaining variable, using regular univariate polynomial
factorization. When that set becomes empty, the plugin reports a theory
conflict to the main MCSat engine. Given a conflict core and the current
assignment, the _explanation procedure_ in the plugin generates a (globally
valid) lemma that explains the conflict in that it excludes a class of
assignments (including the current one) that all violate the conflict core.
The MCSat engine performs conflict analysis using theory explanations and
Boolean resolutions, and either backtracks if it can or concludes
unsatisfiability. On the other hand, the instance is satisfiable once all
variables are assigned a value.

#### Finite Field Explanations.

In our earlier work [9], we presented an explanation procedure for finite
fields. This approach employs subresultant regular subchains (SRS) [22]
between conflicting polynomials to provide new polynomial constraints that can
be propagated. In a nutshell, SRS can be used to construct a generalized
greatest common divisor (GCD) of polynomials that takes into account the
current partial variable assignment on the trail. The computed GCD is utilized
in a zero decomposition procedure to reduce the degree of the conflicting
polynomials until we can learn a polynomial constraint that excludes the
current partial assignment. This constraint is added as an explanation clause
to resolve the conflict. We implemented the procedure of [9] in the current
version of Yices2 using LibPoly. However, it is important to note that there
are other solving techniques for polynomial systems over finite field that
could potentially be utilized to develop an explanation method suitable for an
MCSat-based search. Furthermore, it is still an open question how different
techniques perform in an MCSat environment. That is why we have kept the
explanation procedure encapsulated in our implementation, allowing for easy
extension in order to support development and evaluation of future explanation
procedures.

##  5 Evaluation

Since finite field solving is a rather new endeavor in the world of SMT, no
extended set of SMTlib 2 benchmarks exists yet. For the evaluation we have
selected the benchmark sets presented in the papers describing the theory
behind the implementation of Yices2 and cvc5:

  1. (i)

The polynomial sets from our prior work [9], consisting of 325 instances. This
benchmarks set primarily contains finite fields up to order $211$, using two
classes of polynomial systems: _randomly generated_ as well as _crafted_
systems. The crafted benchmarks are product of (mostly) degree-1 polynomials.

  2. (ii)

Benchmarks generated using ZK proof compilers presented in [18]. Besides
polynomial equations, these 1602 benchmark instances also contain Boolean
structure. The field order varies form small ($11$) up to vast (more than
$2^{255}$).

#### Experimental Setup.

Our experiments were run on an AMD EPYC 7502 CPU with a timeout of $300$
seconds per benchmark instance. We compared our implementation of Yices2
against cvc5 version 1.1.1, which is the latest released version at the time
of writing. We are not aware of any further SMT solvers supporting the theory
of non-linear finite fields to be included in the comparison.

#### Experimental Results.

The performance comparison between the two solvers on the first benchmark set
can be seen in Fig. 2 and Fig. 3 (left). It is clear to see that the random
instances are harder to solve than the crafted instances (which have
significantly more variables). We believe that this is due to the lack of
internal structure in random polynomials. This makes symbolic handling of
those polynomial systems hard, both for Gröbner basis computation (in cvc5) as
well as SRS computation (in Yices2).

$10^{-2}$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$$10^{-2}$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$Yices2cvc5Random
benchmarks

$10^{-2}$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$$10^{-2}$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$Yices2cvc5Crafted
benchmarks

Figure 2: Runtime comparison for benchmarks from [9] (in seconds, timeout
300s)
result: sat o, unsat x; finite field order: 3 (blue), 13 (green), and 211
(orange)

Note that cvc5 performs most symbolic computation upfront (when generating the
Gröbner basis) and enumerates potential solutions in a second step (using
auxiliary Gröbner basis calls). The MCSat approach in Yices2, on the other
hand, interleaves model generation and symbolic computation during the search.
This tends to be an advantage for harder polynomial systems especially
together with small finite field orders. When the finite field order
increases, this advantage seems to vanish. For the crafted polynomial
benchmarks, Yices2 tends to be faster. We believe that this is due to the fact
that the polynomials tend to be large (in the number of monomials), but rather
easy to solve. Generating a full Gröbner basis upfront might add significant
overhead.

For the second benchmark set, many instances can be solved by both solvers
immediately (c.f. Fig. 3 right). We believe that those instances can be solved
without extensive finite field reasoning, as the benchmark set contains
Boolean structure. This enables both solvers to successfully solve benchmarks
even with vast field orders. However, once extensive algebraic reasoning is
required in finite fields of vast order (the majority of the benchmarks), the
purely symbolic approach of cvc5 in proving unsatisfiability seems to be
advantageous. An MCSat approach requires to pick actual values in a gigantic
search space, thus especially strong lemmas need to be learned in order to
prune the search space efficiently. Improving the explanation procedure is
part of our future work.

$0$$100$$200$$300$$10^{-2}$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$time (s)

$0$$500$$1{,}000$$1{,}500$$10^{-2}$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$time (s)

Figure 3: Instances solved over time (timeout 300s) by Yices2 ( blue) and cvc5
( red) from [9] (left) and [18] (right).

##  6 Summary and Outlook

In this system description we have presented the first implementation of an
MCSat-based decision procedure for non-linear finite field polynomials. We
have shown that MCSat is a feasible way of solving SMT instances over finite
fields and it compares well with SMT approaches using Gröbner bases for many
instances.

The presented tool implementation is well suited for future experiments and
the rapid development of more advanced explanation procedures that will
eliminate the current bottlenecks with regard to large finite fields.

###  6.0.1 Acknowledgements

This work was conducted during the first author’s stay at SRI International.
We acknowledge funding from the ERC Consolidator Grant ARTIST 101002685, the
TU Wien SecInt Doctoral College, the FWF SFB project SpyCoDe F8504, the WWTF
ICT22-007 grant ForSmart, the NSF award CCRI-2016597, and from SRI Internal
Research And Development funds. Any opinions, findings and conclusions or
recommendations expressed in this material are those of the author(s) and do
not necessarily reflect the views of the US Government or NSF.

###  6.0.2

The authors have no competing interests to declare that are relevant to the
content of this article.

## References

  * [1] Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , Part I. LNCS, vol. 13243, pp. 415–442. Springer (2022). https://doi.org/10.1007/978-3-030-99524-9_24
  * [2] Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)
  * [3] Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 1267–1329. IOS Press (2021). https://doi.org/10.3233/FAIA201017
  * [4] Buchberger, B.: Bruno Buchberger’s PhD Thesis 1965: An Algorithm for Finding the Basis Elements of the Residue Class Ring of a Zero Dimensional Polynomial Ideal. Journal of Symbolic Computation 41(3-4), 475–511 (2006). https://doi.org/10.1016/J.JSC.2005.09.007
  * [5] Dutertre, B.: Yices 2.2. In: Intl. Conf. on Computer Aided Verification (CAV). LNCS, vol. 8559, pp. 737–744. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_49
  * [6] Dutertre, B., Goel, A., Graham-Lengrand, S., Irfan, A., Jovanovic, D., Mason, I.A.: Yices 2 in SMT-COMP 2023 (2023)
  * [7] Goldwasser, S., Micali, S., Rackoff, C.: The Knowledge Complexity of Interactive Proof Systems. SIAM Journal on Computing 18(1), 186–208 (1989). https://doi.org/10.1137/0218012
  * [8] Graham-Lengrand, S., Jovanovic, D., Dutertre, B.: Solving bitvectors with MCSAT: explanations from bits and pieces. In: Intl. Joint Conf. on Automated Reasoning (IJCAR), Part I. LNCS, vol. 12166, pp. 103–121. Springer (2020). https://doi.org/10.1007/978-3-030-51074-9_7
  * [9] Hader, T., Kaufmann, D., Kovács, L.: SMT solving over finite field arithmetic. In: Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). EPiC Series in Computing, vol. 94, pp. 238–256. EasyChair (2023). https://doi.org/10.29007/4N6W
  * [10] Jovanovic, D.: Solving nonlinear integer arithmetic with MCSAT. In: Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol. 10145, pp. 330–346. Springer (2017). https://doi.org/10.1007/978-3-319-52234-0_18
  * [11] Jovanovic, D., Barrett, C., de Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: Intl. Conf on Formal Methods in Computer-Aided Design (FMCAD). pp. 173–180. IEEE (2013). https://doi.org/10.1109/FMCAD.2013.7027033
  * [12] Jovanovic, D., Dutertre, B.: Libpoly: A library for reasoning about polynomials. In: Intl. Workshop on Satisfiability Modulo Theories (SMT). CEUR Workshop Proceedings, vol. 1889, pp. 28–39. CEUR-WS.org (2017), https://ceur-ws.org/Vol-1889/paper3.pdf
  * [13] Jovanovic, D., de Moura, L.M.: Cutting to the chase solving linear integer arithmetic. In: Intl. Conf on Automated Deduction (CADE). LNCS, vol. 6803, pp. 338–353. Springer (2011). https://doi.org/10.1007/978-3-642-22438-6_26
  * [14] Jovanovic, D., de Moura, L.M.: Solving non-linear arithmetic. In: Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol. 7364, pp. 339–354. Springer (2012). https://doi.org/10.1007/978-3-642-31365-3_27
  * [15] de Moura, L., Jovanovic, D.: A model-constructing satisfiability calculus. In: Intl. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol. 7737, pp. 1–12. Springer (2013). https://doi.org/10.1007/978-3-642-35873-9_1
  * [16] de Moura, L.M., Bjørner, N.S.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)
  * [17] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 3452, pp. 36–50. Springer (2004). https://doi.org/10.1007/978-3-540-32275-7_3
  * [18] Ozdemir, A., Kremer, G., Tinelli, C., Barrett, C.W.: Satisfiability modulo finite fields. In: Intl. Conf. on Computer Aided Verification (CAV), Part II. LNCS, vol. 13965, pp. 163–186. Springer (2023). https://doi.org/10.1007/978-3-031-37703-7_8
  * [19] Ozdemir, A., Wahby, R.S., Brown, F., Barrett, C.W.: Bounded verification for finite-field-blasting - in a compiler for zero knowledge proofs. In: Intl. Conf. on Computer Aided Verification (CAV), Part III. LNCS, vol. 13966, pp. 154–175. Springer (2023). https://doi.org/10.1007/978-3-031-37709-9_8
  * [20] Silva, J.P.M., Sakallah, K.A.: GRASP—A New Search Algorithm for Satisfiability. In: The Best of ICCAD, pp. 73–89. Springer (2003), https://doi.org/10.1007/978-1-4615-0292-0_7
  * [21] Szabo, N.: Smart Contracts: Building Blocks for Digital Markets (1996), [Online]. Available: http://www.fon.hum.uva.nl
  * [22] Wang, D.: Elimination Methods. Springer Science & Business Media (2001)