# Using Symmetries to Lift Satisfiability Checking

Pierre Carbonnelle1, Gottfried Schenner2, Maurice Bruynooghe1, Bart Bogaerts3,
Marc Denecker1

###### Abstract

We analyze how symmetries can be used to compress structures (also known as
interpretations) onto a smaller domain without loss of information. This
analysis suggests the possibility to solve satisfiability problems in the
compressed domain for better performance. Thus, we propose a 2-step novel
method: (i) the sentence to be satisfied is automatically translated into an
equisatisfiable sentence over a “lifted” vocabulary that allows domain
compression; (ii) satisfiability of the lifted sentence is checked by growing
the (initially unknown) compressed domain until a satisfying structure is
found. The key issue is to ensure that this satisfying structure can always be
expanded into an uncompressed structure that satisfies the original sentence
to be satisfied.

We present an adequate translation for sentences in typed first-order logic
extended with aggregates. Our experimental evaluation shows large speedups for
generative configuration problems. The method also has applications in the
verification of software operating on complex data structures. Further
refinements of the translation are left for future work.

##  1 Introduction

In made-to-order manufacturing, the _configuration problem_ is the problem of
finding a configuration of components that satisfies the customer requirements
and feasibility constraints (Felfernig et al. 2014). Such problems can be
solved by choosing a formal vocabulary and by representing the customer
requirements and the feasibility criteria as a logic sentence to be satisfied.
A structure satisfying the sentence, i.e., a model of the sentence, represents
an acceptable configuration.

Methods to solve configuration problems do not scale well, and various
heuristics have been used to improve performance (Schenner and Taupe 2017).
Configurations often have components that are interchangeable. They are the
source of many redundancies in the search space that negatively impact
performance. The standard approach is to add symmetry breaking rules
(DBLP:conf/kr/CrawfordGLR96).

We observed that solutions to configuration problems can be compressed in what
we call a “lifted model”, and that the solution of the original problem can be
obtained by expanding the lifted model. This suggested that configuration
problems, and, more generally, satisfiability problems, could be solved in the
compressed domain: if the compressed domain is significantly smaller, it could
lead to better performance.

As a toy example, consider the following pigeonhole problem: “given 10 pigeons
and 5 pigeonholes, assign each pigeon to a pigeonhole such that each hole has
(at most) 2 pigeons.” With the appropriate vocabulary, a solution for this
problem is:

$\displaystyle\mathit{Pigeon}=\\{$ $\displaystyle p_{1},\ldots,p_{10}\\}$ (1)
$\displaystyle\mathit{Hole}=\\{$ $\displaystyle h_{1},\ldots,h_{5}\\}$ (2)
$\displaystyle\mathit{isIn}=\\{$
$\displaystyle(p_{1},h_{1}),(p_{2},h_{2}),\ldots,(p_{5},h_{5}),$ (3)
$\displaystyle(p_{6},h_{1}),(p_{7},h_{2}),\ldots,(p_{10},h_{5})\\}$

Note the symmetries in the solution: another solution is obtained by
exchanging 2 pigeons or 2 holes in the interpretation of $\mathit{isIn}$.

This solution can be compressed to:

$\displaystyle\mathit{Pigeon}$ $\displaystyle=\\{\mathbf{p}_{1}\\}$ (4)
$\displaystyle\mathit{Hole}$ $\displaystyle=\\{\mathbf{h}_{1}\\}$ (5)
$\displaystyle\mathit{mul}$ $\displaystyle=\\{\mathbf{p}_{1}\mapsto
10,\mathbf{h}_{1}\mapsto 5\\}$ (6) $\displaystyle\mathit{isIn}$
$\displaystyle=\\{(\mathbf{p}_{1},\mathbf{h}_{1})\\}$ (7)

where the $\mathit{mul}$ function indicates how many concrete domain elements
each “lifted” domain element represents, and thus allows the domain
compression. The lifted pigeon represents 10 concrete pigeons, and the lifted
hole represents 5 concrete holes.

Even though the compressed structure only has 2 domain elements
($\mathbf{p}_{1},\mathbf{h}_{1}$, excluding the naturals), it contains enough
information to allow us to _expand_ it into a model isomorphic to the original
model. Following the theory we develop in Section 3, the expansion is as
follows:

$\displaystyle\mathbf{p}_{1}$ $\displaystyle\leadsto p_{1},\ldots,p_{10}$
$\displaystyle\mathbf{h}_{1}$ $\displaystyle\leadsto h_{1},\ldots,h_{5}$
$\displaystyle(\mathbf{p}_{1},\mathbf{h}_{1})$
$\displaystyle\leadsto\\{(p_{1},h_{1}),\ldots,(p_{5},h_{5}),(p_{6},h_{1}),\ldots,(p_{10},h_{5})\\}$

Furthermore, in Section 4, we present a translation of sentences in typed
first-order logic extended with aggregates into sentences that allow domain
compression. We show that a sentence in that language is equisatisfiable with
its translation, given the number of concrete elements in each type: if either
one is satisfiable, the other one is too. This analysis allows us to solve
satisfiability problems in the compressed domain. The novel method operates in
two steps: (i) the sentence to be satisfied is automatically translated into a
“lifted” sentence over the “lifted” vocabulary; (ii) satisfiability of the
lifted sentence is checked by step-wise growing the compressed domain111An
iterative method is required because the size of the compressed domain is not
known in advance. until a satisfying structure is found. Crucially, this
satisfying structure can always be expanded into a model of the original
sentence.

Notice that the lifted model for a variation of the pigeonhole problem above
with 100 times more pigeons and holes has the same number of lifted domain
elements as the base case: the multiplicity of each lifted domain element is
simply multiplied by 100. As a result, and unlike traditional methods, our
method solves that pigeonhole problem in constant time with respect to the
domain size (excluding the naturals).

We evaluate this method by comparing the time needed to find solutions for
generative configuration problems discussed in the literature. Our evaluation
shows that our method has significantly better performance than the
traditional one for problems whose solution can be substantially compressed.

Our paper is structured as follows: after introducing our notation, we analyze
how symmetries can be used to compress structures onto a smaller domain
without loss of information (Section 3), and describe how to lift a concrete
sentence so that it is equisatisfiable with the lifted sentence (Section 4);
we describe the method, evaluate it on generative configuration problems
(Section 5), and discuss applications in Boolean Algebra of sets with
Presburger Arithmetic (BAPA) (Section 6) before concluding with a discussion.

##  2 Preliminaries

This section introduces the logic language supported by our method, and the
concept of permutation of a structure.

### Typed first order logic with aggregates

We call FO(Type, Aggregate) the language we support. We assume familiarity
with first order logic (Enderton 1972). A _vocabulary_ $\mathit{\Sigma}$ is a
set of type, predicate, and function symbols. Predicates and functions have a
type signature (e.g. ${f:\bar{T}\rightarrow T}$, where $\bar{T}$ denotes a
tuple of types). Some symbols are pre-defined: type $\mathbb{B}$ (booleans),
$\mathbb{Q}$ (rationals), equality, arithmetic operators and arithmetic
comparisons. _Terms_ and _formulae_ are constructed from symbols according to
the usual FO syntactic rules. We also allow sum aggregates (written as
${\sum_{\begin{subarray}{c}\bar{x}\in\bar{T}:\phi\end{subarray}}t}$ or as
${\sum_{\bar{x}\in\bar{T}}(t\mathit{~{}if~{}}\phi)}$). A cardinality aggregate
$\\#\\{\bar{x}\in\bar{T}\mid\phi\\}$ is a shorthand for a sum aggregate whose
term $t$ is $1$. Quantification and aggregation can only be over finite types.
Terms and formulas must be well-typed. A formula without free-variable is
called a _sentence_.

A _$\mathit{\Sigma}$ -structure_ $\mathit{I}$, consists of a domain and an
_interpretation_ of each symbol of vocabulary $\mathit{\Sigma}$. The
interpretations of types are disjoint and finite (except $\mathbb{Q}^{I}$
which is infinite). The interpretation $p^{I}$ of a predicate $p$ is a set of
tuples $\bar{d}$ of domain elements of appropriate types. The interpretation
$f^{I}$ of a function $f$ is a set of pairs $(\bar{d},d)$, also denoted by
$\bar{d}\mapsto d$.

An _extended structure_ is a structure with a variable assignment, i.e., with
a mapping from variable $\bar{x}$ to values $\bar{d}$, denoted
$[\bar{x}:\bar{d}]$. The value of a formula or term in an extended structure
is computed according to the usual FO semantic rules, which require that the
interpretation of function symbols be total functions over their domain. A
$\mathit{\Sigma}$-structure is a _model_ of a sentence if the value of the
sentence is true in the structure, i.e., if it _satisfies_ it. The problem of
_satisfiability checking_ in typed FO logic is the problem of deciding whether
a sentence has a model, given the interpretation of the types.

### Permutations and orbits

A _permutation_ of a set is a bijection from that set to itself. We denote a
permutation by $\pi$, and its inverse by $\pi^{-1}$. The _identity_
permutation, $\pi^{0}$, maps every element of the set to itself. The _order_
of a permutation is the smallest positive number $n$ such that $\pi^{n}$ is
the identity permutation. Hence, the $n$th permutation of an element is equal
to its “$n$th modulo the order” permutation.

_Cycles_ are permutations that map elements in a cyclic fashion. A cycle is
denoted by $(d^{1}d^{2}\cdots d^{n})$. A permutation over a finite set has a
unique decomposition into _disjoint cycles_. Its order is the least common
multiple ($\mathit{lcm}$) of the length of its cycles.

The permutation of a tuple of elements $\bar{d}$ is denoted by $\pi(\bar{d})$
and is equal to
$(\pi(d_{1}),\makebox[10.00002pt][c]{.\hfil.\hfil.},\pi(d_{n}))$. The _$\pi$
-orbit_ of an element $d$ (resp. of a tuple of elements $\bar{d}$) is the set
of its repeated permutations $o_{\pi}(d)=\\{\pi^{i}(d)\mid i\in\mathbb{N}\\}$
(resp. $o_{\pi}(\bar{d})=\\{\pi^{i}(\bar{d})\mid i\in\mathbb{N}\\}$).

##  3 Lossless compression of structures

In this section, we discuss how, and when, a concrete structure with
symmetries can be compressed into a lifted structure over a smaller domain
without loss of information, and how a lifted structure can be expanded into a
concrete one.

Symmetries in a structure $I$ are described by a domain permutation $\pi$
(DBLP:journals/tplp/DevriendtBBD16): it is a permutation of the domain of $I$
that maps numbers to themselves, and other domain elements in $T^{I}$ to
domain elements in $T^{I}$. Since numbers are mapped to themselves by the
permutation, and since types besides $\mathbb{Q}$ are finite, the permutation
is composed of cycles.

A domain permutation _induces a structure transformation_. The interpretation
in the transformed structure, denoted $\pi(I)$, is defined as follows:

  * •

the type of domain element $d$ in $\pi(I)$ is its type in $I$;

  * •

a tuple $\bar{d}^{\prime}$ is in the transformed interpretation of predicate
symbol $p$ if and only if $\pi^{-1}(\bar{d}^{\prime})$ is in the original
interpretation of $p$:
$p^{\pi(I)}=\\{\bar{d}^{\prime}\mid\pi^{-1}(\bar{d}^{\prime})\in
p^{I}\\}=\\{\pi(\bar{d})\mid\bar{d}\in p^{I}\\}$;

  * •

a tuple $(\bar{d}^{\prime}\mapsto d^{\prime})$ is in the transformed
interpretation of function symbol $f$ if and only if
$\pi^{-1}(\bar{d}^{\prime})\mapsto\pi^{-1}(d^{\prime})$ is in the original
interpretation of $f$:

$\displaystyle f^{\pi(I)}$ $\displaystyle=\\{(\bar{d}^{\prime}\mapsto
d^{\prime})\mid(\pi^{-1}(\bar{d}^{\prime})\mapsto\pi^{-1}(d^{\prime}))\in
f^{I}\\}$ $\displaystyle=\\{(\pi(\bar{d})\mapsto\pi(d))\mid(\bar{d}\mapsto
d)\in f^{I}\\}$

######  Definition 1 (Automorphism)

A permutation $\pi$ that transforms a structure into itself, i.e., such that
$I=\pi(I)$, is an _automorphism_ of the structure.

Every structure has at least one automorphism: the identity domain
permutation. Note that an automorphism maps the interpretation of any constant
to itself, i.e., $c^{I}()=\pi(c^{I}())$. Thus, the length of the cycle
containing $c^{I}()$ is 1.

We introduce the new concept of _backbone_ , which plays a critical role in
the compression that we propose. Essentially, a _backbone_ for an automorphism
of $I$ is a set of domain elements obtained by picking one element in each
cycle, such that the interpretation of any symbol can be reconstructed from
its interpretation restricted to the backbone, by applying the automorphism
repeatedly. Formally:

######  Definition 2 (Backbone)

A _backbone_ for an automorphism $\pi$ of $I$ is a subset $S$ of the domain of
$I$ such that:

  * •

each cycle $C$ of $\pi$ has exactly one element in $S$;

  * •

for each predicate $p/n\in\Sigma$, $p^{I}$ is the union of the $\pi$-orbits of
the tuples in $p^{\mathit{I}}\cap S^{n}$, i.e.,

$\displaystyle p^{I}=\bigcup_{\bar{d}\in p^{\mathit{I}}\cap
S^{n}}o_{\pi}(\bar{d})=\\{\pi^{i}(\bar{d})\mid\bar{d}\in p^{\mathit{I}}\cap
S^{n},i\in\mathbb{N}\\}$ (8)

  * •

for each function $f/n\in\Sigma$, $f^{I}$ is the union of the $\pi$-orbits of
the tuples in $f^{I}\cap(S^{n}\times S)$, i.e,

$\displaystyle f^{I}=\bigcup_{(\bar{d}\mapsto d)\in
f^{\mathit{I}}\cap(S^{n}\times S)}o_{\pi}(\bar{d}\mapsto d)$ (9)
$\displaystyle=\\{\pi^{i}(\bar{d}\mapsto d)\mid(\bar{d}\mapsto d)\in
f^{\mathit{I}}\cap(S^{n}\times S),i\in\mathbb{N}\\}$

###### Example 1

For the pigeonhole example in the introduction of the paper, a backbone of
automorphism $(p_{1}\cdots p_{10})(h_{1}\cdots h_{5})$ is
$S=\\{p_{1},h_{1}\\}$. Another is $S=\\{p_{2},h_{2}\\}$.

In all structures, the set of domain elements is a _trivial_ backbone for the
identity automorphism. However, not all automorphisms have a backbone, as the
following example shows.

###### Example 2

Let $\\{a,b\\}$ be a (concrete) domain with one type $T$. In structure $I_{1}$
(resp. $I_{2}$), function symbol $f:T\rightarrow T$ is interpreted as
$\\{a\mapsto a,b\mapsto b\\}$ (resp. $\\{a\mapsto b,b\mapsto a\\}$).
Permutation $(ab)$ is an automorphism of both structures. The only two subsets
$S$ satisfying the first condition of backbone for $(ab)$ are $\\{a\\}$ and
$\\{b\\}$. Since $f^{I_{1}}$ can be reconstructed from $f^{I_{1}}\cap(S\times
S)$ for both subsets $S$, both subsets are backbones of $I_{1}$. However, none
is a backbone of $I_{2}$ (because $f^{I_{2}}\cap(S\times S)=\emptyset$ for
both candidate sets $S$).

A backbone enables us to lift a structure into a structure with a smaller
domain, as we now describe.

######  Definition 3 (Lifted vocabulary)

For a vocabulary $\Sigma$, its lifted vocabulary $\Sigma_{l}$ consists of the
symbols of $\Sigma$ and, for any type $T$ of $\Sigma$, a symbol
$\mathit{mul}_{T}:T\to\mathbb{N}$, called the _multiplicity_ function for $T$.

We will drop the subscript $T$ in the function symbol $\mathit{mul}_{T}$ when
this is unambiguous.

######  Definition 4 (Lifted structure)

Let $I$ be a $\Sigma$-structure with an automorphism $\pi$ having backbone
$S$. A lifted structure $L$ derived from $I$ is a $\Sigma_{l}$-structure such
that:

  * •

its domain is $S$, called the lifted domain;

  * •

for each type predicate $T$, $T^{L}=T^{I}\cap S$;

  * •

for each predicate symbol $p/n$, $p^{L}=p^{\mathit{I}}\cap S^{n}$;

  * •

for each function symbol $f/n$, $f^{L}=f^{I}\cap(S^{n}\times S)$;

  * •

for each $l\in S$, $mul^{L}(l)=|o_{\pi}(l)|$, the size of the $\pi$-orbit of
$l$ in $I$.

###### Example 3

Continuing the pigeonhole problem, the lifted structure is described by
Equations 4-7.

Given the lifted structure $L$ derived from $I$ and the automorphism $\pi$ on
the concrete domain $I$, one can reconstruct $I$, i.e., one can _expand_ the
lifted interpretations of the type, predicate and function symbols,
essentially by closing them under repeated application of $\pi$. Formally,

$\displaystyle\mathit{exp}(T^{L})$ $\displaystyle=\bigcup_{l\in
T^{L}}o_{\pi}(l)=\\{\pi^{i}(l)\mid l\in T^{L},i\in\mathbb{N}\\}$ (10)
$\displaystyle\mathit{exp}(p^{L})$ $\displaystyle=\bigcup_{\bar{l}\in
p^{L}}o_{\pi}(\bar{l})=\\{\pi^{i}(\bar{l})\mid\bar{l}\in
p^{L},i\in\mathbb{N}\\}$ (11) $\displaystyle\mathit{exp}(f^{L})$
$\displaystyle=\bigcup_{(\bar{l}\mapsto l)\in f^{L}}o_{\pi}(\bar{l}\mapsto l)$
$\displaystyle=\\{\pi^{i}(\bar{l}\mapsto l)\mid(\bar{l}\mapsto l)\in
f^{L},i\in\mathbb{N}\\}.$ (12)

###### Example 4

Continuing the pigeonhole problem, the expansion of the lifted structure
described by Equations 4-7 for automorphism $(p_{1}\cdots p_{10})(h_{1}\cdots
h_{5})$ is the structure described by Equations 1-3.

In our approach, we need to find lifted structures that can be expanded into
concrete ones. We observe that there is a simple construction to expand _any_
lifted $\Sigma_{l}$-structure $L$ with lifted domain $S$ that results
sometimes (but not always) in a concrete structure $I$ with an automorphism
$\pi$ having backbone $S$. This construction is as follows. Any lifted element
$l\in S$ is expanded to concrete elements $d^{1},\dots,d^{n}$ where $l$ is
identified with $d^{1}$ and $n$ is equal to $mul^{L}(l)$. If the multiplicity
of $l$ is zero,222Null multiplicities will prove useful for iterative methods
in Section 5 its expansion is the empty set. The expansion of any two distinct
lifted elements must be disjoint. We call $d^{1}$ a _base_ element, and define
$\pi(d^{i})=d^{i+1}$ for $1\leq i<n-1$, and $\pi(d^{n})=d^{1}$. Thus,
$(d^{1}\dots d^{n})$ is a cycle of $\pi$. This way, we obtain the concrete
domain $D$ and permutation $\pi$. Notice that lifted domain elements with
multiplicity zero have no image in D, and $\pi$ is not defined on them. The
expansion of a lifted tuple $\bar{l}$ in a lifted structure is its
$\pi$-orbit:

$\mathit{exp}(\bar{l})=o_{\pi}(\bar{l})=\\{\pi^{i}(\bar{l})|i\in\mathbb{N}\\}$
(13)

if none of the expansion of its elements is empty, and is empty otherwise. The
concrete interpretation of symbols is obtained by expanding the tuples in
their lifted interpretations, as in Equations (10-12).

It follows from the correspondence between Definition 2 and Equations (10-12)
that, if $\pi$ and $I$ are constructed from $L$ in this way, and if $I$ is
actually a structure, then $S$ is a backbone of $\pi$ in $I$. When $L$ only
has strictly positive multiplicities, a lifted structure derived from the
expansion of $L$ will be isomorphic to $L$: in some sense, the compression is
lossless. However, $I$ may not be a structure because the interpretation of a
function symbol in $I$ might not be a total function on its domain, as the
following example shows.

###### Example 5

Consider the lifted structure $L$ with domain $S=\\{a,b\\}$, with types
$A^{L}=\\{a\\}$, $B^{L}=\\{b\\}$, and for $f:A\times A\mapsto B$,
$f^{L}=\\{(a,a)\mapsto b\\}$. Finally, let
$\mathit{mul}(a)=\mathit{mul}(b)=2$, The expanded domain is
$\\{a^{1},a^{2},b^{1},b^{2}\\}$ with permutation $(a^{1}a^{2})(b^{1}b^{2})$.
The expansion of $f^{L}$ is $\\{(a^{1},a^{1})\mapsto
b^{1},(a^{2},a^{2})\mapsto b^{2}\\}$. There is no entry for $(a^{1},a^{2})$,
so the expansion is not a total function.

Consider now the lifted structure $L$ with domain $S=\\{a,b\\}$, with type
$A^{L}=\\{a\\},B^{L}=\\{b\\}$, for $f:A\mapsto B$, $f^{L}=\\{a\mapsto b\\}$.
Finally, $\mathit{mul}(a)=1,\mathit{mul}(b)=2$. The expanded domain is
$\\{a^{1},b^{1},b^{2}\\}$ with permutation $(a^{1})(b^{1}b^{2})$. The
expansion of $f^{L}$ is $\\{a^{1}\mapsto b^{1},a^{1}\mapsto b^{2}\\}$. This
expansion gives two different values for $a^{1}$, so it is not a function.

To distinguish lifted structures that can be expanded into concrete ones from
those that cannot, we introduce the notion of _regularity_.

######  Definition 5 (Regular function, regular lifted structure)

The lifted interpretation of a function symbol is regular if its expansion
defines a total function in the concrete domain, i.e., if it specifies exactly
one image for every tuple in the concrete domain. A _regular lifted structure_
is a lifted structure in which the interpretation of each function symbol is
regular.

We can now define the expansion of a regular lifted structure:

######  Definition 6 (Expansion of a regular lifted structure)

Let $L$ be a regular lifted structure over a lifted vocabulary. Then, $I$, the
expansion of $L$, is the structure over the concrete vocabulary defined as
follows:

  * •

its domain is the union of each type expansion, i.e.,
$\bigcup_{T_{i}}\mathit{exp}(T_{i}^{L})$;

  * •

for each type symbol $T$, $T^{I}=\mathit{exp}(T^{L})$;

  * •

for each predicate symbol $p$, $p^{I}=\mathit{exp}(p^{L})$;

  * •

for each function symbol $f$, $f^{I}=\mathit{exp}(f^{L})$.

The expansion of a regular lifted structure does not involve any search. The
time needed for this expansion is generally negligible (e.g., less than 0.1
sec for 10,000 concrete domain elements).

To further characterize regular functions, we introduce the concept of regular
tuples. We use $\mathit{Mul}(l_{1},\ldots,l_{n})$ (resp.
$\mathit{Lcm}(l_{1},\ldots,l_{n})$) as a shorthand for the product of the
multiplicities of $l_{i}$ (resp. their least common multiple $\mathit{lcm}$).
First, we observe that the size of the expansion (Equation 13) of a tuple
$\bar{l}$ is finite: it is the order of the permutation defined by the cycles
of its elements, i.e., $\mathit{Lcm}(l_{1},\ldots,l_{n})$.333Taking the
convention that the $\mathit{lcm}$ of a tuple of numbers containing 0 is 0.
Also, the expansion has at most $\mathit{Mul}(l_{1},\ldots,l_{n})$ tuples; it
is then the cross-product of the expansions of its elements. When those two
numbers are identical, we say that the tuple is regular.

######  Definition 7 (Regular lifted tuple)

A lifted tuple is regular if and only if its expansion is the cross-product of
the expansion of its elements.

###### Example 6

Let $(a,b)$ be a tuple of two lifted domain elements with $\mathit{mul}(a)=2$
and $\mathit{mul}(b)=4$. Its expansion is
$\\{(a^{1},b^{1}),(a^{2},b^{2}),(a^{1},b^{3}),(a^{2},b^{4})\\}$, of size
$\mathit{Lcm}(2,4)=4$. Note that, e.g., the tuple $(a^{1},b^{2})$ does not
belong to the expansion: thus, $(a,b)$ is not regular. It is regular when
$\mathit{mul}(b)=0$ (the expansion of $b$ and of $(a,b)$ are empty), or when,
e.g., $\mathit{mul}(b)=3$ (the expansion is
$\\{(a^{1},b^{1}),(a^{2},b^{2}),(a^{1},b^{3}),(a^{2},b^{1}),(a^{1},b^{2}),(a^{2},b^{3})\\}$),
of size $\mathit{Lcm}(2,3)=6$.

Nullary and unary tuples are always regular. An $n$-ary tuple is regular when
one of its elements has multiplicity zero, or every pair of its elements have
multiplicities that are coprime.

######  Proposition 1 (Regular function)

A function $f^{L}$ is regular if, for all tuples $\bar{l}$ in the domain of
$f^{L}$, it holds that (i) $\bar{l}$ is regular, and (ii) the multiplicity of
$\bar{l}$ is a multiple of the multiplicity of its image.

###### Proof 1

First, we show that the expansion of $f^{L}$ gives at least one value for
every tuple $\bar{d}$ in the concrete domain of $f$. Each element $d_{i}$ of
$\bar{d}$ is in the expansion of a lifted domain element $l_{i}\in T_{i}^{L}$.
Tuple $\bar{l}=(l_{1},\cdots,l_{n})\in\bar{T}^{L}$ is in the lifted domain of
$f^{L}$ as $f^{L}$ is total; it is regular by (i), hence $\bar{d}$ is in its
expansion and $f^{I}(\bar{d})$ is in $\mathit{exp}(f^{L}(\bar{l}))$.

Next, we show that the expansion gives at most one value for every tuple
$\bar{d}$ in the concrete domain of $f$. Let $\bar{d}$ be in the expansion of
$\bar{l}$, with $\mathit{Lcm}(\bar{l})=m=\mathit{Mul}(\bar{l})$ by (i). We
thus have $0<m$. The expansion of $f^{L}$ contains the pairs
$\pi^{i}(\bar{l}\mapsto f^{L}(\bar{l}))$ and $\pi^{i+n\times m}(\bar{l}\mapsto
f^{L}(\bar{l}))$, for any $\bar{l}$ in the domain of $f^{L}$, and for any $i$
and $n$. The first element of these two pairs are identical by definition of
$m$; the second elements are identical by (ii).

##  4 Translation into a lifted sentence

We now present a translation of a sentence in FO(Type, Aggregate) into a
sentence that allows domain compression, such that the translation is
equisatisfiable with the original for a given size of the concrete types. The
translation $\overline{\chi(\phi)}$ of a sentence $\phi$ is the conjunction of
(i) the transformed sentence $\chi(\phi)$, (ii) sentences expressing
regularity conditions, and (iii) sentences stating the size of the concrete
types (i.e., stating the value of the sum of values of $\mathit{mul}_{T}$).

The transformation $\chi(e)$ of an expression $e$ is defined recursively in
Table 1. The left column shows the possible syntactical forms in the concrete
sentence; the middle column shows the transformation; the third column shows
the regularity constraints added to the translation. The bottom part of the
table shows the regularity constraints added for each function symbol in the
vocabulary to ensure that the function interpretations are regular
(Proposition 1).

Table 1: Terms, formulas, and their translation

Expression $e$ |  Transformation $\chi(e)$ |  Regularity condition |
---|---|---|---
Term |  |  |
$\displaystyle x$ |  $\displaystyle x$ |  |  (14)q:Xx
$\displaystyle c()$ |  $\displaystyle c()$ |  |  (15)q:Xc
$\displaystyle f(\bar{t})$ |  $\displaystyle f(\chi(\bar{t}))$ |  |  (16)q:Xf
$\displaystyle t_{1}\oplus t_{2},\oplus\in\\{+,-,\times,\div\\}$ |  $\displaystyle\chi(t_{1})\oplus\chi(t_{2})$ |  |  (17)q:Xop
$\displaystyle\sum_{\begin{subarray}{c}\bar{x}\in\bar{T}:p(\bar{t},s)\land\phi\end{subarray}}t\textsuperscript{(*)}$ | $\sum_{\bar{x}\in\bar{T}}(\frac{\mathit{Mul}(\bar{x})\mathit{Lcm}(\chi(\bar{t}),\chi(s))}{\mathit{Lcm}(\chi(\bar{t}))\mathit{mul}(\chi(s))}\times\chi(t)\mathit{~{}if~{}}0<\mathit{Mul}(\bar{x})\land p(\chi({\bar{t}}),\chi(s))\land\chi(\phi))$ |  (18)q:Xsumf2
$\displaystyle\sum_{\begin{subarray}{c}\bar{x}\in\bar{T}:\phi\end{subarray}}t$ | $\sum_{\bar{x}\in\bar{T}}(\mathit{Mul}(\bar{x})\times\chi(t)\mathit{~{}if~{}}0<\mathit{Mul}(\bar{x})\land\chi(\phi))$ |  (19)q:Xsum
Formula |  |  |
$\displaystyle p()$ |  $\displaystyle p()$ |  |  (20)q:Xprop
$\displaystyle p(\bar{t})$ |  $\displaystyle p(\chi(\bar{t}))$ |  $\displaystyle\mathit{RC}(p(\chi(\bar{t})))\textsuperscript{(**)}$ |  (21)q:Xp
$\displaystyle t_{1}\sim t_{2},{\sim}\in\\{<,>,\leq,\geq\\}$ |  $\displaystyle\chi(t_{1})\sim\chi(t_{2})$ |  |  (22)q:Xeqa
$\displaystyle\phi_{1}\bigotimes\phi_{2},\bigotimes\in\\{\land,\lor,\Rightarrow,\Leftrightarrow\\}$ |  $\displaystyle\chi(\phi_{1})\bigotimes\chi(\phi_{2})$ |  |  (23)q:Xand
$\displaystyle\lnot\phi$ |  $\displaystyle\lnot\chi(\phi)$ |  |  (24)q:XNot
$\displaystyle\forall\bar{x}\in\bar{T}:p(\bar{t},s)\Rightarrow\phi\textsuperscript{(*)}$ | $\forall\bar{x}\in\bar{T}:0<\mathit{Mul}(\bar{x})\land p(\chi({\bar{t}}),\chi(s))\Rightarrow\chi(\phi)$ |  (25)q:Xforall2
$\displaystyle\exists\bar{x}\in\bar{T}:p(\bar{t},s)\land\phi\textsuperscript{(*)}$ | $\exists\bar{x}\in\bar{T}:0<\mathit{Mul}(\bar{x})\land p(\chi({\bar{t}}),\chi(s))\land\chi(\phi)$ |  (26)q:Xexists2
$\displaystyle\forall\bar{x}\in\bar{T}:\phi$ | $\forall\bar{x}\in\bar{T}:0<\mathit{Mul}(\bar{x})\Rightarrow\chi(\phi)$ |  (27)q:Xforall
$\displaystyle\exists\bar{x}\in\bar{T}:\phi$ | $\exists\bar{x}\in\bar{T}:0<\mathit{Mul}(\bar{x})\land\chi(\phi)$ |  (28)q:Xexists
for each function $f:\bar{T}\rightarrow T$ |  |  |
| $\forall\bar{x}\in\bar{T}:\mathit{Mul}(\bar{x})=\mathit{Lcm}(\bar{x})$ |  (29)q:f1
| $\forall\bar{x}\in\bar{T}:\exists n\in\mathbb{N}:\mathit{Mul}(\bar{x})=n\times\mathit{mul}(f(\bar{x}))$ |  (30)q:f2

  * (*)

Rules (LABEL:eq:Xsumf2, LABEL:eq:Xforall2, LABEL:eq:Xexists2) are applied only
when $\mathit{vars}(\bar{t})\subseteq\\{\bar{x}\\}$ and
$\mathit{vars}(s)\cap\\{\bar{x}\\}=\emptyset$; Rules (LABEL:eq:Xsum,
LABEL:eq:Xforall, LABEL:eq:Xexists) are applied otherwise.

  * (**)

$\mathit{RC}(p(\chi(\bar{t})))$ is defined as
$\forall\bar{x}\in\bar{T}_{\bar{x}}:p(\chi(\bar{t}))\Rightarrow\mathit{Mul}(\bar{x})=\mathit{Lcm}(\bar{x})\lor\mathit{Mul}(\chi(\bar{t}))=\mathit{Lcm}(\chi(\bar{t}))$,
where $\bar{x}=\mathit{vars}(p(\chi(\bar{t})))$.

Note that sum aggregates and quantified formulas are transformed by
specialized rules (Rules LABEL:eq:Xsumf2, LABEL:eq:Xforall2-LABEL:eq:Xexists2)
when possible (see table footnote), and by general rules (Rules LABEL:eq:Xsum,
LABEL:eq:Xforall-LABEL:eq:Xexists) otherwise. Generally, it is beneficial to
do equivalence-preserving transformations of sentences to obtain sentences of
the form allowing application of specialized rules (LABEL:eq:Xsumf2,
LABEL:eq:Xforall2, LABEL:eq:Xexists2).

The transformation of a sentence consists of adding $0<\mathit{Mul}(\bar{x})$
filters (to cope with lifted domains elements with an empty expansion) and of
multiplying the term $t$ in an aggregate term with some decompression factor:
in Rule LABEL:eq:Xsum, it is the number $\mathit{Mul}(\bar{x})$ of possible
concrete variable assignments; in Rule LABEL:eq:Xsumf2, it is that number
multiplied by the fraction of concrete assignments that make $p(\bar{t},s)$
true. The regularity condition added for an atom (Rule LABEL:eq:Xp) ensures
the translated atom is equisatisfiable with the original atom.

###### Example 7

The sentence ”at most 2 pigeons in each hole”:
$\forall
h\in\mathit{Hole}:\\#\\{p\in\mathit{Pigeon}\mid\mathit{isIn}(p,h)\\}\leq 2$.
Its transformation by Rule LABEL:eq:Xsumf2 (with $\phi=\textbf{true}$) and
LABEL:eq:Xforall is:444Recall that a cardinality aggregate is a shorthand for
a sum aggregate whose term is $1$.
$\forall h\in\mathit{Hole}:0<\mathit{mul}(h)\Rightarrow\\\
\indent\indent\sum_{p\in\mathit{Pigeon}}(\frac{\mathit{Lcm}(p,h)}{\mathit{mul}(h)}\mathit{~{}if~{}}0<\mathit{mul}(p)\land\mathit{isIn}(p,h))\leq
2.$

######  Theorem 1 (Equisatisfiability)

An FO(Type, Aggregate) sentence is equisatisfiable with its translation, given
the number of concrete elements in each type.

If $I$ is a model of the sentence, then $L$ constructed by extending $I$ by
setting all multiplicities to one is a model of the translated sentence:
indeed, the added constraints are trivially satisfied, and the translated
sentence is equivalent to the original one. Proving the converse is long and
complex. It is proved by structural induction of two invariants over the
syntactic tree of the sentence to be satisfied: (i) a transformed formula
$\chi(\phi)$ is true in $L$ under some variable assignment
$[\bar{x}:\bar{l}_{x}]$ if and only if $\phi$ is true in $I$ under any
variable assignments $[\bar{x}:\bar{d}_{x}]$ such that each $d_{x_{i}}$ is in
the expansion of $l_{x_{i}}$ (ii) similarly, if a transformed term $\chi(t)$
has value $l$ in the lifted structure $L$ under some variable assignment
$[\bar{x}:\bar{l}_{x}]$, then, the expansion of the value $l$ contains the
value of the term $t$ in $I$ (the expansion of $L$), for any variable
assignment $[\bar{x}:\bar{d}_{x}]$ such that each $d_{x_{i}}$ is in the
expansion of $l_{x_{i}}$. This property holds only when the regularity
constraints given in Table 1 hold in the lifted structure. This explains why
these constraints are added to the transformed sentence. The proof is in the
Appendix.

##  5 Evaluation of the method

#### Implementation

The goal of the evaluation is to show that there are satisfiability problems
where substantial compression of the domain is possible, and that the lifted
models can indeed be expanded into concrete ones. A problem is solved
iteratively, starting with empty lifted domains. Given a domain, the lifted
sentence is reduced to a propositional sentence and its satisfiability is
determined with a standard satisfiability solver capable of arithmetic
reasoning. If the sentence is unsatisfiable with this domain, the sentence is
reduced to a minimal unsatisfiable formula (DBLP:conf/sat/LynceM04), and the
domains of the types used in that formula are extended with one element. This
process is repeated until a model of the sentence is found (it does not
terminate if the original sentence is unsatisfiable for any domain size,
unless one imposes an ad-hoc upper limit on the size of lifted domains).

In many experiments, it was sufficient to support the special Rules
LABEL:eq:Xsumf2, LABEL:eq:Xforall2-LABEL:eq:Xexists2 for the case where the
atom $p$ is of the form $t_{1}=s$ (e.g., $\mathit{holeOf}(p)=h)$. Then, the
transformation of a sum aggregate per Rule LABEL:eq:Xsumf2 simplifies to:

$\displaystyle\frac{1}{\mathit{mul}(\chi(s))}\sum_{\bar{x}\in\bar{T}}($
$\displaystyle\mathit{Mul}(\bar{x})\times\chi(t)$ (31)
$\displaystyle\mathit{~{}if~{}}0<\mathit{Mul}(\bar{x})\land\chi({t_{1}}){=}\chi(s)\land\chi(\phi))$

This formula does not use the $\mathit{lcm}$ function, which is not supported
natively by solvers. In other experiments, we used an interpretation table for
$\mathit{lcm}$.

Problems are expressed in $\mathrm{FO}(\cdot)$555https://fo-
dot.readthedocs.io/, a Knowledge Representation language with support for
types, subtypes, and aggregates.666Subtypes are subsets of types, and are
declared as unary predicates in $\mathrm{FO}(\cdot)$. Subtypes can be used
where types are used: in the type signature of a symbol and in quantification.
A $\mathrm{FO}(\cdot)$ (lifted) sentence is translated by IDP-Z3 (Carbonnelle
et al. 2022) for use with the Z3 SMT solver (de Moura and Bjørner 2008). The
overhead of this translation is negligible.

The source code of our examples is available in the supplementary material.
Tests were run using Z3 v4.12.1 on an Intel Core i7-8850H CPU at 2.60GHz with
12 cores, running Ubuntu 22.04 with 16 GB RAM. We run a modified version of
IDP-Z3 v0.10.8 on Python 3.10.

#### Pigeonhole problem

To validate the approach, we first consider the satisfiability problem of
assigning each pigeon to one pigeonhole, such that each pigeonhole holds (at
most) 2 pigeons. Function
$\mathit{holeOf}:\mathit{Pigeon}\mapsto\mathit{Hole}$ is used to represent
this relation.

When there are twice as many pigeons as holes, the lifted solution has 1
lifted pigeon and 1 lifted hole, as shown in the introduction of the paper. As
expected, the time needed to solve the lifted problem is almost constant when
it is satisfiable. The correct multiplicities are found quickly by Z3 using a
sub-solver specialized for arithmetic. For example, with 10,000 pigeons, the
lifted sentence is solved in only 0.05 sec and the expansion of the lifted
model into a concrete one in 0.1 sec. With the same solver and the original
sentence, the solution time increases exponentially (4 sec to solve the
problem for 30 pigeons). We are aware that symmetry breaking can reduce the
complexity, but to the best of our knowledge, solving time is at least linear
in the number of pigeons for the best symmetry breaking solvers that are
available.

We also validated our method on pigeonhole problems where the relation between
pigeon and holes is represented by a binary predicate. The translated sentence
uses an interpretation table for $\mathit{lcm}$. Experiments confirm
equisatisfiability, but the complexity is quadratic because of the
$\mathit{lcm}$ table. Finding a more efficient implementation has been left
for future work.

#### Generative configuration problems

Generative configuration problems (GCP) are configuration problems in which
the number of some components has to be found: the number of elements in some
types is not known in advance. An iterative method is thus always required to
find them. When the compressed domain is smaller than the concrete domain, the
number of iterations needed to solve the lifted sentence is smaller than the
number of iterations for the original sentence, leading to better performance.
Hence, GCP is a good application domain for our method.

We evaluate our solving method on three representative GCP discussed in the
literature:

  * •

the House Configuration and Reconfiguration problem (Friedrich et al. 2011),

  * •

the Organized Monkey Village (Reger, Suda, and Voronkov 2016)

  * •

the Rack problem (Feinerer, Salzer, and Sisel 2011; Comploi-Taupe,
Francescutto, and Schenner 2022),

These problems are expressed using only an equality predicate and unary
symbols, and most regularity constraints introduced by our method are
trivially satisfied.

Table 2: Wall clock time in seconds to solve configuration problems, and number (#) of used domain elements in models. Yes: lifted sentence, No: original sentence, T: timeout after 200 sec. | Time | #
---|---|---
Lifted? | Yes | No | Yes | No
HCP 1 | 0.2 | 0.2 | 6 | 10
HCP 3 | 0.22 | 1.5 | 6 | 27
HRP 1 | 0.27 | 0.23 | 7 | 10
HRP 3 | 0.30 | 6.41 | 8 | 25
Monkey 1 | 0.28 | 184.66 | 6 | 20
Monkey 4 | 0.27 | T | 6 | 52
Rack 2011 | 0.24 | 8.82 | 5 | 23
Rack A5 | 0.46 | 0.86 | 5 | 19
Rack A10 | 0.41 | 37.52 | 5 | 38
Rack A1000 | 0.54 | T | 4 | 2250
Rack ABCD4 | 1.55 | 4.37 | 13 | 20
Rack ABCD8 | 2.69 | T | 13 | 40
Rack ABCD20 | 3.31 | T | 13 | 100
Rack A1 | 0.61 | 0.75 | 5 | 7
Rack A2 | 0.64 | 1.54 | 5 | 9
Rack A3 | 0.62 | 3.69 | 5 | 11
Rack A4 | 0.65 | 36.9 | 5 | 13
Rack A5 | 0.65 | T | 5 | 19

The top half of Table 2 shows results with Z3 (with automatic translation of
the sentence), the bottom half with the OR-tools
solver777https://google.github.io/or-tools/, used via CPMpy (Guns 2019). (with
manual translation). A more detailed table is provided in Appendix.

Solutions to problems with higher suffixes have more components than similar
problems with lower ones. The table shows near constant time performance on
the Rack ABCD problems. The lifted methods solve each of the 20 occurrences of
the ABCD Racks problem in (Comploi-Taupe, Francescutto, and Schenner 2022) in
less than 5 seconds (instead of 6 minutes on average in that paper, using an
ASP solver).

These results show that our method has significant merits for solving certain
classes of problems.

##  6 Boolean Algebra of sets with Presburger Arithmetic

Lifted domain elements represent disjoint sets of concrete domain elements. A
model search in the lifted domain can be seen as a model search involving
sets. Hence, our work is highly related to Boolean Algebra of sets with
Presburger Arithmetic (BAPA), a logic that can express constraints on the
cardinality of sets, of their unions and of their intersections (Kuncak and
Rinard 2007; Suter, Steiger, and Kuncak 2011; Bansal et al. 2016). Some
problems from verification of properties of software operating on complex data
structures contain fragments that belong to BAPA.

A sample BAPA statement is $|A|>1\land A\subseteq B\land|B\cap C|\leq 2$,
where $A,B,C$ are sets, and $|A|$ is the cardinality of $A$. The equivalent
expression in FO(Type, Aggregate) is $(\\#\\{d:A(d)\\}>1)\land(\forall
d:A(d)\Rightarrow B(d))\land(\\#\\{d:B(d)\land C(d)\\}\leq 2)$, where $A,B,C$
are now unary predicates over a (unique) type whose interpretation is to be
found. This expression can be lifted and solved using our approach (see
example in Supplementary material).

In general, any BAPA sentence can be converted to a concrete FO(Type,
Aggregate) sentence that only uses unary predicates, and that can be lifted
without regularity constraints. Hence, our approach offers a simple way to
solve BAPA problems using any solver capable of reasoning over the rationals.
The performance advantage should be evaluated in future work.

On the other hand, the conversion of a concrete FO(Type, Aggregate) sentence
to BAPA logic is challenging because FO(Type, Aggregate) is more expressive:
it allows n-ary relations, functions, sum aggregates, and product of
cardinalities. Thus, a BAPA solver could not be used to solve, e.g.,
generative configuration problems. Still, extensions of BAPA solvers to handle
finite n-ary relations have been implemented in CVC4 (Meng et al. 2017).

A simple approach to represent structures in BAPA is to use disjoint subsets
of the concrete domain, called _Venn regions_ , so that the cardinalities of
any set of interest is the sum of the cardinalities of its Venn regions.
Unfortunately, the number of Venn regions grows exponentially with the number
of sets of interest. Hence, various methods have been developed to reduce this
growth, e.g., by creating new Venn regions lazily when required (Bansal et al.
2016). Venn regions are similar to our lifted domain elements, and the
iterative method that creates new Venn region is similar, to some extent, to
our iterative method that creates new lifted elements when required.

Our method cannot prove the unsatisfiability of a sentence. By contrast,
efficient methods have been proposed to prove the unsatisfiability of BAPA
sentences (Suter, Steiger, and Kuncak 2011).

##  7 Discussion

To the best of our understanding, our method is very different from current
symmetry breaking methods in SAT solving, from methods for model counting and
from methods for lifted inference in probabilistic logic (although we borrowed
the term ”lifted” from that domain).

Much work remains to be done in evaluating the method and determining problem
areas where it is useful. Also the relationship with BAPA logic is worth
further exploration, because, unlike our method, BAPA can identify
unsatisfiable sentences and our method does not terminate for such problems.
Efficient implementation of the $lcm$ function is another area of research.

Ideally, any compression of a model of a sentence (Section 3) should be a
model of the lifted sentence. It is unlikely that this is achievable, as it
requires a translation that avoids all regularity constraints apart from those
for functions. This requires being able to predict the fraction of concrete
variable assignments (in the expansion of a lifted assignment) that make a
concrete formula true, given that the translated formula is true with the
lifted assignment. In particular, filter formulas (in an aggregate) having
both free and quantified variables are problematic.

Still, many refinements of the translation in Table 1 are feasible. We have
already worked out some refinements, but they cannot be presented within the
current space constraints. Here we provide a glimpse (some understanding of
the proof in the appendix might be required to follow).

One refinement concerns $\exists\bar{x}:p(t[\bar{x}],s[\bar{y}])\land\phi$ .
When $s$ is a tuple instead of a single term, the atom cannot be handled by
the special Rule LABEL:eq:Xexists2 and a regularity constraint over all
variables of the atom is added when using Rule LABEL:eq:Xexists. One can show
that either $\mathit{Mul}(\bar{y})=\mathit{Lcm}(\bar{y})$ or
$\mathit{Mul}(\bar{s})=\mathit{Lcm}(\bar{s})$ is sufficient to ensure that the
tuple $\bar{s}$ evaluates under an assignment $[\bar{y}:\bar{d}_{y}]$ to a
value $\pi^{i}(\bar{l}_{s})$ for some $i$ (with $\bar{l}_{s}$ the value of
$\bar{s}$ in the lifted structure). This is a much weaker constraint, and it
is sufficient to show that the rule remains correct. Also, not all atoms in
$\phi$ need a regularity constraint as in Table 1. For an atom in a positive
context, the constraint can be dropped (if the only occurrences of variables
from $\bar{y}$ are in arguments also occurring in $\bar{s}$), or weakened.
Similar refinements are possible in aggregates. In universally quantified
formulae, the above weakening of constraints is valid for atoms in a negative
context.

Another unexplored question is the complexity of problems with models that can
be compressed. Apparently, a pigeon hole problem is an easy problem (although
hard for SAT solvers).

## References

  * Aloul, Sakallah, and Markov (2006) Aloul, F. A.; Sakallah, K. A.; and Markov, I. L. 2006.  Efficient symmetry breaking for boolean satisfiability.  _IEEE Transactions on Computers_ , 55(5): 549–558.
  * Aschinger et al. (2014) Aschinger, M.; Drescher, C.; Gottlob, G.; and Vollmer, H. 2014.  LoCo - A Logic for Configuration Problems.  _ACM Trans. Comput. Log._ , 15(3): 20:1–20:25.
  * Bansal et al. (2016) Bansal, K.; Reynolds, A.; Barrett, C.; and Tinelli, C. 2016.  A new decision procedure for finite sets and cardinality constraints in SMT.  In _International Joint Conference on Automated Reasoning_ , 82–98. Springer.
  * Barbosa et al. (2022) 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.; and Zohar, Y. 2022.  cvc5: A Versatile and Industrial-Strength SMT Solver.  In Fisman, D.; and Rosu, G., eds., _Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I_ , volume 13243 of _Lecture Notes in Computer Science_ , 415–442. Springer.
  * Carbonnelle et al. (2022) Carbonnelle, P.; Vandevelde, S.; Vennekens, J.; and Denecker, M. 2022.  IDP-Z3: a reasoning engine for FO(.).  _CoRR_ , abs/2202.00343.
  * Comploi-Taupe, Francescutto, and Schenner (2022) Comploi-Taupe, R.; Francescutto, G.; and Schenner, G. 2022.  Applying incremental answer set solving to product configuration.  In et al., A. F., ed., _SPLC ’22: 26th ACM Int’l Systems and Software Product Line Conference_ , 150–155. ACM.
  * de Moura and Bjørner (2008) de Moura, L.; and Bjørner, N. 2008.  Z3: An Efficient SMT Solver.  In et al., C. R. R., ed., _Tools and Algorithms for the Construction and Analysis of Systems, 14th Int’l Conference_ , volume 4963 of _Lecture Notes in Computer Science_ , 337–340. Springer.
  * de Salvo Braz, Amir, and Roth (2005) de Salvo Braz, R.; Amir, E.; and Roth, D. 2005.  Lifted First-Order Probabilistic Inference.  In et al., L. P. K., ed., _IJCAI-05, Proceedings of the Nineteenth Int’al Joint Conference on Artificial Intelligence, 2005_ , 1319–1325. Professional Book Center.
  * Déharbe et al. (2011) Déharbe, D.; Fontaine, P.; Merz, S.; and Paleo, B. W. 2011.  Exploiting Symmetry in SMT Problems.  In et al., N. S. B., ed., _CADE-23 2011._ , volume 6803 of _Lecture Notes in Computer Science_ , 222–236. Springer.
  * Devriendt, Bogaerts, and Bruynooghe (2014) Devriendt, J.; Bogaerts, B.; and Bruynooghe, M. 2014.  BreakIDGlucose: On the importance of row symmetry in SAT.  In _Proceedings 4th International Workshop on the Cross-Fertilization Between CSP and SAT_ , 1–17.
  * Devriendt et al. (2016) Devriendt, J.; Bogaerts, B.; Bruynooghe, M.; and Denecker, M. 2016.  Improved Static Symmetry Breaking for SAT.  In Creignou, N.; and Le Berre, D., eds., _Theory and Applications of Satisfiability Testing – SAT 2016_ , 104–122. Cham: Springer International Publishing.  ISBN 978-3-319-40970-2.
  * Enderton (1972) Enderton, H. B. 1972.  _A mathematical introduction to logic_.  Academic Press.  ISBN 978-0-12-238450-9.
  * Falkner et al. (2011) Falkner, A. A.; Haselböck, A.; Schenner, G.; and Schreiner, H. 2011.  Modeling and solving technical product configuration problems.  _Artif. Intell. Eng. Des. Anal. Manuf._ , 25(2): 115–129.
  * Feinerer, Salzer, and Sisel (2011) Feinerer, I.; Salzer, G.; and Sisel, T. 2011.  Reducing Multiplicities in Class Diagrams.  In et al., J. W., ed., _MODELS 2011._ , volume 6981 of _Lecture Notes in Computer Science_ , 379–393. Springer.
  * Felfernig et al. (2014) Felfernig, A.; Hotz, L.; Bagley, C.; and Tiihonen, J. 2014.  _Knowledge-based configuration: From research to business cases_.  Newnes.
  * Friedrich et al. (2011) Friedrich, G.; Ryabokon, A.; Falkner, A. A.; Haselböck, A.; Schenner, G.; and Schreiner, H. 2011.  (Re)configuration using Answer Set Programming.  In et al., K. M. S., ed., _Proceedings of the IJCAI 2011 Workshop on Configuration_ , volume 755 of _CEUR Workshop Proceedings_. CEUR-WS.org.
  * Gebser, Ryabokon, and Schenner (2015) Gebser, M.; Ryabokon, A.; and Schenner, G. 2015.  Combining heuristics for configuration problems using answer set programming.  In _International Conference on Logic Programming and Nonmonotonic Reasoning_ , 384–397. Springer.
  * Gent and Smith (1999) Gent, I. P.; and Smith, B. 1999.  _Symmetry breaking during search in constraint programming_.  Citeseer.
  * Guns (2019) Guns, T. 2019.  Increasing modeling language convenience with a universal n-dimensional array, CPpy as python-embedded example.  In _Proceedings of the 18th workshop on Constraint Modelling and Reformulation at CP (Modref 2019)_ , volume 19.
  * Kuncak and Rinard (2007) Kuncak, V.; and Rinard, M. C. 2007.  Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic.  In Pfenning, F., ed., _CADE-21, 2007_ , volume 4603 of _Lecture Notes in Computer Science_ , 215–230. Springer.
  * Lenzerini and Nobili (1990) Lenzerini, M.; and Nobili, P. 1990.  On the satisfiability of dependency constraints in entity-relationship schemata.  _Information Systems_ , 15(4): 453–461.
  * Mariën et al. (2008) Mariën, M.; Wittocx, J.; Denecker, M.; and Bruynooghe, M. 2008.  SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions.  In Büning, H. K.; and Zhao, X., eds., _Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings_ , volume 4996 of _Lecture Notes in Computer Science_ , 211–224. Springer.
  * McCune (1994) McCune, W. 1994.  A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems.  Technical report, Argonne National Laboratory.
  * Meng et al. (2017) Meng, B.; Reynolds, A.; Tinelli, C.; and Barrett, C. W. 2017.  Relational Constraint Solving in SMT.  In de Moura, L., ed., _CADE 26, 2017_ , volume 10395 of _Lecture Notes in Computer Science_ , 148–165. Springer.
  * Nethercote et al. (2007) Nethercote, N.; Stuckey, P. J.; Becket, R.; Brand, S.; Duck, G. J.; and Tack, G. 2007.  MiniZinc: Towards a standard CP modelling language.  In _Principles and Practice of Constraint Programming–CP 2007: 13th Int’l Conference_ , 529–543. Springer.
  * Reger, Suda, and Voronkov (2016) Reger, G.; Suda, M.; and Voronkov, A. 2016.  Finding Finite Models in Multi-sorted First-Order Logic.  In et al., N. C., ed., _Theory and Applications of Satisfiability Testing - SAT 2016_ , volume 9710 of _Lecture Notes in Computer Science_ , 323–341. Springer.
  * Schenner and Taupe (2017) Schenner, G.; and Taupe, R. 2017.  Techniques for solving large-scale product configuration problems with ASP.  In _Proceedings of the 19th International Configuration Workshop_ , 12–19.
  * Suter, Steiger, and Kuncak (2011) Suter, P.; Steiger, R.; and Kuncak, V. 2011.  Sets with Cardinality Constraints in Satisfiability Modulo Theories.  In et al., R. J., ed., _VMCAI 2011_ , volume 6538 of _Lecture Notes in Computer Science_ , 403–418. Springer.
  * Tack (2009) Tack, G. 2009.  _Constraint propagation: models, techniques, implementation_.  Ph.D. thesis, Saarland University, Germany.
  * Taupe, Falkner, and Schenner (2016) Taupe, R.; Falkner, A.; and Schenner, G. 2016.  Deriving tighter component cardinality bounds for product configuration.  In _18 th International Configuration Workshop_ , 47.
  * Taupe et al. (2021) Taupe, R.; Friedrich, G.; Schekotihin, K.; and Weinzierl, A. 2021.  Solving Configuration Problems with ASP and Declarative Domain Specific Heuristics.  In et al., M. A., ed., _Proceedings of the 23rd International Configuration Workshop ( 2021)_ , volume 2945 of _CEUR Workshop Proceedings_ , 13–20. CEUR-WS.org.

##  8 Appendix

See AAAI.tex file


# Measuring the tau polarization at ILC

Keita Yumino  The Graduate University for Advanced Studies, SOKENDAI  Daniel
Jeans  KEK, Tsukuba, Japan  The Graduate University for Advanced Studies,
SOKENDAI

###### Abstract

Measurement of the tau lepton polarization in $e^{-}e^{+}\to\tau^{-}\tau^{+}$
is an important electro-weak measurement at ILC and other future electron-
positron colliders. In this paper we discuss several methods to extract
polarimeter information for $e^{-}e^{+}\to\tau^{-}\tau^{+}$ events at the
nominal centre-of-mass energy, and develop a new method, based on charged
particle impact parameter measurement, which can accurately reconstruct tau
momenta even in events with significant Initial State Radiation.

In future work we will extend the study to estimate the precision with which
the tau polarization can be measured at ILC-250, both for high-mass tau pairs
and for those which radiatively return to the $Z^{0}$ peak. This will
complement our past study which showed that the tau polarization can be
measured to better than 1% at the ILC-500.

Submitted to the Proceedings of the US Community Study

on the Future of Particle Physics (Snowmass 2021)

##  I Introduction

The polarized beams foreseen for the ILC allow sensitive probes of Left and
Right-handed electrons’ neutral current couplings, both at the nominal
collision energies (250, 350, 500, 1000 GeV) and in the “radiative return” to
the $Z$ boson. At a collider with unpolarized beams, for example at LEP,
measurement of the tau lepton polarisation in tau-pair events provides a
similar measurement of the chirality of the neutral current interactions. At
the ILC, it will be possible to simultaneously use both of these methods. The
relation between these two measurements will be affected both by the true beam
polarization – providing a powerful check for systematic effects – and the
universality of the chiral interactions between lepton generations – a
particularly interesting topic in these days of flavor anomalies.

We discuss studies of the extraction of tau polarisation information at an
electron positron collider such as the ILC. Several different methods to
extract polarisation observables are studied.

##  II Polarimeters

The distribution of a tau lepton’s decay products depends on the orientation
of its spin. Polarization-sensitive observables, known as polarimeters, make
use of this dependence to reconstruct the spin orientation. We study hadronic
decays of the tau, which offer greater sensitivity to the tau’s polarisation.
Optimal tau polarimeter vectors can be rather simply defined in the case of
$\tau^{\pm}\to\pi^{\pm}\nu$ (which we sometimes abbreviate as
“$\tau\rightarrow\pi$”) and $\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$
(“$\tau\rightarrow\rho$”) decays, see e.g. Tauola . The polarimeter vectors
are defined in the tau rest frames as follows: for
$\tau^{\pm}\to\pi^{\pm}\nu$, it is the direction of the neutrino momentum,
while for $\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$ it is the direction of the vector
$\mathbf{P}=2(\mathbf{q}\cdot\mathbf{p_{\nu}})\mathbf{q}-m_{q}^{2}\mathbf{p_{\nu}}$,
where $\mathbf{q}=\mathbf{p}_{\pi^{\pm}}-\mathbf{p}_{\pi^{0}}$, and
$\mathbf{p_{\nu}},\mathbf{p}_{\pi^{\pm}},\mathbf{p}_{\pi^{0}}$ are
respectively the 3-momenta of the neutrino, charged and neutral pions. To
distinguish taus of different helicity, we consider the cosine of the angle
this polarimeter vector makes to the tau flight direction: we call this the
“polarimeter”. We refer to this form of the polarimeters as “optimal”; example
distributions are shown in Fig. 1. Extracting this optimal form of the
polarimeter requires knowledge of the tau neutrino momentum, which is
obviously not directly measurable, or equivalently of the parent tau momentum.
It also requires the reconstruction of every visible particle produced in the
tau decay, and the correct identification of the tau decay mode.

Figure 1:  “Optimal” polarimeter distributions for $\tau^{\pm}\to\pi^{\pm}\nu$
(left) and $\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$ (right) decays of $\pm$ helicity
tau leptons, reconstructed using MC truth information.

“Approximate” polarimeters can be defined, reconstructed based only on the
momenta of visible tau decay products. In the 2-body decay
$\tau^{\pm}\to\pi^{\pm}\nu$, the energy of the pion is an optimal polarimeter
for taus of known energy, however due to the spread in beam energies at a real
collider and the resulting spread in tau energies, its sensitivity is slightly
decreased. In the case of $\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$, one can arrive
at an approximate polarimeter by integrating over possible neutrino momenta,
as described in duflot . In the case of $\tau^{\pm}\to\pi^{\pm}\nu$ decays,
the approximate method retains almost all the sensitivity of the “optimal”
analysis, while for $\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$ decays the sensitivity
of the “approximate” method is significantly smaller than the “optimal” one.

##  III Approximate polarimeters at ILC-500

High-mass tau pairs at ILC-500 provide an experimental challenge due to the
large boost, leading to very highly collimated tau jets whose constituents can
be challenging to resolve. We here summarize results presented in
Jeans:2019brt .

Tau-pair event samples were generated using WHIZARD version 1.95 whizard ;
omega , taking into account the ILC beam energy spread, beamstrahlung and
initial state radiation. After decaying the taus using TAUOLA Tauola , events
were fully simulated and reconstructed using standard ILD tools based on
ddsim/DD4hep dd4hep  and MarlinReco marlinreco . The principal output of the
reconstruction is a collection of Particle Flow Objects (PFO), corresponding
to reconstructed final state particles.

An event selection was developed to select high-mass pairs of taus, and to
reject other processes. A selection efficiency of around 60% was achieved for
high-mass tau pairs with at least one hadronic tau decay, with around 1.5–4%
contamination from non-tau backgrounds, depending on the assumed beam
polarisation. The separation of the single-prong hadronic decay modes to one,
two, or three pion modes achieved an efficiency of between 90% and 60%,
depending on the decay mode. One– and two–pion decays were used to calculate
“approximate” polarimeters from reconstructed information. Pseudo-experiments
carried out on simulated polarimeter distributions were used to estimate the
statistical precision achievable at ILC-500: better than 1% for the 1.6/ab of
data in each of the $\mathrm{e^{-}_{L80}e^{+}_{R30}}$ and
$\mathrm{e^{-}_{R80}e^{+}_{L30}}$ polarisations, and around 2% in the like-
sign polarisations for which 0.4/ab was assumed.

The influence of various experimental effects was also investigated: use of
the “approximate” form of the polarimeters; signal inefficiency and background
contamination; and ECAL energy resolution, shown in Fig. 2. Each of these
factors gives rise to a similar level of degradation in experimental
precision, which is degraded by a factor of around two compared to the ideal
result.

Figure 2: Statistical precision on the tau polarisation at ILC-500, in the
$\mathrm{e^{-}_{L80}e^{+}_{R30}}$ and $\mathrm{e^{-}_{R80}e^{+}_{L30}}$
polarizations, at various levels of “cheating”, from optimal MC information
(“MC-optimal”) to full simulation and realistic reconstruction (“no cheat
(Sel/Bg)”). Triangles (open circles) correspond to the
$\tau^{\pm}\to\pi^{\pm}\nu$ ($\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$) decays, and
IDR-L/S refer to two ILD models Jeans:2019brt .

##  IV Reconstruction of the tau momentum in di-tau events

To go beyond the approximate polarimeters described above, explicit
reconstruction of the tau momentum is required. We discuss several ways in
which the tau momenta can be directly reconstructed in the
$e^{-}e^{+}\to\tau^{-}\tau^{+}$ process. We study these methods using the MC
truth information of di-tau events generated by WHIZARD, taking into account
the effects of ISR and the beam energy spread and beamstrahlung expected at
ILC-250. Tau leptons are decayed by TAUOLA. No detector simulation or
realistic reconstruction algorithms were applied.

###  IV.1 Cone method

In the case of a di-tau event both of whose taus decay hadronically, if the
two tau leptons are back-to-back and each carry the nominal beam energy, the
tau momenta can be calculated to within a 2-fold ambiguity. These assumptions
are applicable to tau pairs produced at the nominal centre-of-mass energy,
with no energy loss via ISR or beamstrahlung. The assumed energy and invariant
mass of the tau define both the energy of the neutrino and the angle which it
makes to the visible tau momentum. Equivalently, one can calculate the angle
which the tau momentum makes to the visible momentum, defining a cone around
the visible momentum on which the tau momentum lies.

The two taus in an event are assumed to be back-to-back in the collision
frame. The intersections of the two cones in an event then represent tau
momentum directions which are consistent with all assumptions and constraints.
The number of possible solutions is either 2 (in the case of intersecting
cones, as illustrated in Fig. 3) or 0 (if the cones do not intersect). The
assumptions made above are not valid in the case of significant initial state
radiation, or non-nominal beam energy, for example due to beamstrahlung. Under
such conditions, the cones often do not intersect, leading to an inefficiency
of the method, or, if they do intersect, to inaccurate reconstruction.

Figure 3:  Illustration of the cone method, showing the cone intersections
corresponding to the tau momentum solutions.

Figure 4: Distribution of $e^{-}e^{+}\to\tau^{-}\tau^{+}$ events in their
invariant mass $m_{\tau\tau}$, for all events and for those in which the cone
method identifies a solution. The right plot shows the cone method’s
efficiency as a function of $m_{\tau\tau}$.

Fig. 4 shows the original distribution of events in the tau invariant mass
$m_{\tau\tau}$ and the distribution of events for which the cone method found
a solution. The ratio of the two is also shown, demonstrating that while the
cone method has a reasonable efficiency of $\sim 70\%$ for events at
$m_{\tau\tau}\sim 250~{}$GeV, the efficiency drops to around $20\%$ by
$m_{\tau\tau}=240~{}$GeV and $<5\%$ by $m_{\tau\tau}=200~{}$GeV. Even a rather
modest deviation from the method’s assumptions can have a strong effect on the
ability to identify a solution.

For events for which the cone method does not find a solution, one possible
option is to take the midpoint of cone surfaces as a solution for the tau
momentum direction. We call this “Midpoint method”. This can always find a
solution, however it may be far from the true one, particularly for events
whose taus are in reality not back-to-back, such as those preceded by ISR.

Figure 5 compares the polarimeters calculated using the cone and midpoint
methods with the MC truth values. In the case of $\tau^{\pm}\to\pi^{\pm}\nu$
decays, the polarimeter reconstructed using the cone method is in good
agreement with the optimal one, while for $\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$
decays the reconstruction is noticeably worse. Events in which the cone method
fails – predominantly those with $m_{\tau\tau}$ far from the nominal centre-
of-mass energy – are then passed to the midpoint method. Comparisons of the
extracted polarimeter with the MC truth for these events are shown in the same
figure. The accuracy of polarimeter reconstruction is markedly worse, since
the assumptions are, in general, broken more severely for such events.

Figure 5:  Correlation between reconstructed and true polarimeters for
$\tau^{\pm}\to\pi^{\pm}\nu$ (left) and $\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$
(right) decays, for events reconstructed using the cone (upper), and midpoint
(lower) methods.

###  IV.2 Impact parameter method

We here describe a new tau reconstruction method which is much less sensitive
to ISR, which allows reconstruction of tau momenta and optimal polarimeters
for events at different effective centre-of-mass energies. This is achieved by
including information of tau decay daughters’ trajectories close to the
interaction point: in other words, their impact parameters. The vertex
detectors being designed for ILC have superb single hit resolution, low mass
to minimize multiple scattering, and will be placed within $\sim 15$ mm of the
interaction point. This provides an excellent measurement of the impact
parameter. Use of the impact parameter to reconstruct tau leptons from Higgs
boson decay has already been demonstrated in Jeans:2015vaa . The event
topology in $e^{-}e^{+}\to\tau^{-}\tau^{+}$ is significantly different, so the
methods therein developed are not directly applicable.

The ILC and other electron-positron Higgs factories typically have an
interaction region that has a very small transverse size (significantly
smaller than the impact parameter resolution), and somewhat long in the $z$
direction along the beams. In the case of the ILC, the beam size at 250 GeV
will be $7~{}nm\times 700~{}nm\times 0.3~{}mm$. We therefore assume that the
primary interaction occurs along the beam line $x=y=0$, and that $z$ component
of the interaction point is unknown.

We additionally assume that ISR has negligible transverse momentum (or in
other words that the taus are back-to-back in the x-y projection of the
nominal CM frame), and that any energy loss due to ISR can be modelled as a
single photon collinear with one of the incoming beams.

Figure 6: Schematic image of calculating tau direction.

We then consider a plane which contains the $z$ axis (ie the beam axis), at
some angle $\phi$ to the $x$ axis, as illustrated in Fig. 6. The interaction
point lies somewhere along the $z$ axis, and therefore within the plane. Since
the taus are back-to-back, their momenta also lie in the plane at a particular
value of $\phi$. The intersection of the trajectories of charged tau daughters
with this plane can be calculated (in this study we assume these trajectories
can be approximated as straight lines near the IP); these intersections
correspond to the decay points of the tau leptons.

If we take some general interaction position along the $z$-axis, defined by
its coordinate $z_{\rm{IP}}$, then the flight direction of the taus is
defined, being between the intersection point and the decay points.

For each choice of $\phi$ and $z_{\rm{IP}}$ the two tau 4-momenta can be
calculated by applying 4-momentum conservation and assuming a single ISR
photon. By comparing this calculated 4-momentum to the visible tau 4-momentum,
the invariant mass of each tau’s missing momentum (i.e. the mass of the
invisible tau decay products) can be calculated. Since we are concerned mostly
with hadronic tau decays, we choose the values of $\phi$ and $z_{\rm{IP}}$
which result in neutrino masses closest to zero. The equations are difficult
(even impossible?) to solve analytically, so we use a graphical method to find
solutions. Figure 7 shows the extracted invisible invariant masses for the two
taus depending on the choice of $\phi$ and $z_{\rm{IP}}$, and the positions of
the identified local minima which are taken as potential solutions.

Figure 7: Dependence of the invisible masses on $\phi$ and $z_{\rm{IP}}$. The
color scale represents the invisible invariant mass of the two taus (left,
center) and their sum (right). Red triangles correspond to the identified
solutions, local minima in the right-hand plot.

The number of identified solutions in $e^{-}e^{+}\to\tau^{-}\tau^{+}$ events
is shown in Fig. 8, for all events, and for those in which ISR carries less
than 5 GeV of transverse momentum. Half of the method’s inefficiency is due to
cases in which there is large missing transverse momentum; once these events
are removed, the average efficiency to identify at least one solution is
around 75%. The angle between the reconstructed and true tau directions is
shown in the same figure: the reconstructed direction is typically within a
few mrad of the true direction.

Figure 8: Top: The number of solutions, in all $e^{-}e^{+}\to\tau^{-}\tau^{+}$
events (left) and those with small ($<5$ GeV) ISR transverse momentum (right).
Bottom: The angle between the true and reconstructed tau directions.

Figure 9 shows the distribution in $m_{\tau\tau}$ of all events and of those
in which at least one solution is found. It also shows their ratio – the
method’s efficiency – for the entire sample, and when considering only events
whose ISR has small transverse momentum $<5~{}$GeV: such events can probably
be experimentally identified by a search for visible photons far from the tau
jets. The efficiency in this subsample is around 80% at high $m_{\tau\tau}$,
and remains in the range 60-70% down to very small $m_{\tau\tau}$$\sim
10~{}$GeV. There is an interesting structure around the $Z$ peak which is not
yet fully understood.

Figure 9: Upper: distribution of $e^{-}e^{+}\to\tau^{-}\tau^{+}$ events in
$m_{\tau\tau}$, and distribution of events in which at least one “impact
parameter method” solution was found. Lower: $m_{\tau\tau}$ dependence of the
efficiency of the method in all events (left), and in events with small ISR
transverse momentum (right).

Once the tau momenta have been reconstructed, polarimeter information can be
calculated using the “optimal” forms with maximal sensitivity. Figure 10 shows
the distributions of polarimeters for taus of positive and negative helicity,
calculated using the solutions found by the impact parameter method. A clear
difference between taus of positive and negative helicity is seen. The figure
also shows the correlation between the true and reconstructed polarimeters,
which shows the rather good reconstruction quality for the majority of events,
with only a rather small probability of mis-reconstruction by a large amount.

Figure 10:  Top: Polarimeters for $\tau^{\pm}\to\pi^{\pm}\nu$ and
$\tau^{\pm}\to\pi^{\pm}\pi^{0}\nu$ calculated using solutions found using the
impact parameter method. Bottom: comparison between the reconstructed and true
polarimeters.

These studies will be continued in the remaining period of the Snowmass study.
We will estimate the precision with which the tau polarisation can be measured
at ILC-250, comparing the different reconstruction techniques. At present, we
ignore the effects of detector resolution: these will also be included in a
future update of this work.

##  V Conclusion

We first reported on our previous full-simulation study which showed that the
tau polarization can be measured to better than 1% at ILC-500.

We further studied the reconstruction of tau polarisation at ILC-250, using
particle momenta at MC level. Several techniques to fully reconstruct
$e^{-}e^{+}\to\tau^{-}\tau^{+}$ events were investigated, however they fail to
accurately reconstruct events with large energy loss through ISR. We developed
a new reconstruction method which makes use of charged particle impact
parameter information, as provided by the precise vertex detectors planned for
ILC experiments. In a study at the MC level, this method seems to provide
efficient and accurate reconstruction of tau leptons, allowing polarization
information to be efficiently extracted.

In future work, we will investigate the effect of full detector simulation and
reconstruction, quantify the precision with which the tau polarisation can be
measured at ILC-250 at $m_{\tau\tau}\sim 250$ and $\sim m_{Z}$, and compare
the proposed reconstruction methods.

## References

  * [1] S. Jadach, J. H. Kuhn and Z. Was, “TAUOLA: A Library of Monte Carlo programs to simulate decays of polarized tau leptons”, Comput. Phys. Commun. 64 (1990) 275.
  * [2] L. Duflot, “Nouvelle méthode de mesure de la polarisation du $\tau$. Application au canal $\tau\to{a_{1}}\nu_{\tau}$ dans l’expérience ALEPH”, LAL-93-09.
  * [3] D. Jeans and K. Yumino, “ILD benchmark: a study of $e^{-}e^{+}\to\tau^{-}\tau^{+}$ at 500 GeV,” [arXiv:1912.08403 [hep-ex]].
  * [4] W. Kilian, T. Ohl, J. Reuter, “WHIZARD: Simulating Multi-Particle Processes at LHC and ILC”, Eur.Phys.J.C71 (2011) 1742, arXiv: 0708.4233
  * [5] M. Moretti, T. Ohl, J. Reuter, “O’Mega: An Optimizing matrix element generator”, LC-TOOL-2001-040-rev, arXiv: hep-ph/0102195-rev.
  * [6] https://dd4hep.web.cern.ch/dd4hep/
  * [7] https://github.com/iLCSoft/MarlinReco/
  * [8] D. Jeans, “Tau lepton reconstruction at collider experiments using impact parameters,” Nucl. Instrum. Meth. A 810, 51-58 (2016) [arXiv:1507.01700 [hep-ex]].