# Interactive Model Expansion
in an Observable Environment11footnotemark: 1

CARBONNELLE PIERRE  VENNEKENS JOOST  BOGAERTS BART  DENECKER MARC

###### Abstract

Many practical problems can be understood as the search for a state of affairs
that extends a fixed partial state of affairs, the _environment_ , while
satisfying certain conditions that are formally specified. Such problems are
found in, e.g., engineering, law or economics.

We study this class of problems in a context where some of the relevant
information about the environment is not known by the user at the start of the
search. During the search, the user may consider tentative solutions that make
implicit hypotheses about these unknowns. To ensure that the solution is
appropriate, these hypotheses must be verified by observing the environment.
Furthermore, we assume that, in addition to knowledge of what constitutes a
solution, knowledge of general laws of the environment is also present. We
formally define partial solutions with enough verified facts to guarantee the
existence of complete and appropriate solutions.

Additionally, we propose an interactive system to assist the user in their
search by determining 1) which hypotheses implicit in a tentative solution
must be verified in the environment, and 2) which observations can bring
useful information for the search. We present an efficient method to over-
approximate the set of relevant information, and evaluate our implementation.

###### keywords:

Knowledge Representation, Man-Machine Interface, Configuration Problem.

##  1 Introduction

> Some things are in our control
> and others not.
>
> Epictetus

Many practical problems can be understood as the search for a state of affairs
that extends a fixed partial state of affairs, the _environment_ , while
satisfying certain conditions that are formally specified. Such problems are
found in, e.g., engineering, law or economics. Consider, for instance, the
buyer of a house who has to declare the purchase for tax purposes. The
environment consists of the properties of the house, of the seller and of the
sales contract: they are not under the control of the purchaser. This
environment has to be extended with a registration containing decisions on,
e.g., which tax rebate to claim. Such rebates are subject to conditions, and
have consequences, stated by law.

The Knowledge Representation (KR) methodology to solve such problems is to
design a vocabulary to represent the relevant objects and concepts in the
states of affairs, and to express the conditions as a theory in a declarative
KR language. The theory is the set of laws to be satisfied. When the
environment is fully known, it can be expressed as a structure, and the search
for a solution can be performed automatically by Model Expansion inference on
the theory and the structure (Mitchell et al., 2006).

However, the information about the environment is rarely fully known at the
start of the search. In our example, the buyer of the house does not know all
the attributes of the house when they start their registration. In such cases,
two approaches have been implicitly used: (i) all _relevant_ information about
the environment is assumed to be known at the start of the search so that a
solution can be determined without making any hypothesis about the environment
(Felfernig et al., 2014a ), or, (ii) when this assumption is dropped, the
model expansion mechanism will choose values for the unknown environmental
symbols, and the user has the implicit responsibility to verify that these
values are indeed correct in the environment. We are not aware of any method
to assist the user in the verification task that this second approach
requires. Thus, there is a danger that the verification is incomplete, and
that the user accepts a solution making incorrect assumptions in their
environment.

The primary goal of this work is to study the problem of model expansion in an
unknown, but observable, environment in a precise and formal way. To achieve
this goal, it is crucial that we make an _explicit distinction_ between
environmental and decision symbols in the system. In this setting, an
important difference arises between an _unknown_ environmental symbol, and an
_undecided_ decision symbol. In both cases, the value of the symbol is not
available to the system, but in the first case, it exists but is unknown,
while in the second case, it does not exist yet. Values assigned to symbols by
the system must be handled accordingly. When the system assigns a value to an
environmental symbol, the user must go observe if the assigned value is
correct.

Notice that the value of some environmental symbols may not be known at the
start of the search. For example, the buyer may not know whether a rebate has
already been claimed for a renovation. If this information becomes relevant,
the buyer will have to “observe it” in the environment, e.g., by asking the
seller. Distinguishing environmental from decision symbols is unique to our
system. When the system is aware of this distinction, it can assist the user
by highlighting which observations still need to be made to be sure that the
proposed solution conforms to reality, as well as inform them that the final
configuration is indeed appropriate (i.e., that all the hypotheses have been
verified by observing the environment).

Next to making a distinction between two types of symbols, we also make a
distinction between the laws of possible environments and the laws of
acceptable solutions. The laws of possible environments are guaranteed to hold
independently of the decisions of the user; by contrast, the satisfaction of
the laws of acceptable solutions depends on the decision of the user.
Importantly, unlike consequences of the laws of possible environments,
environmental consequences derived from the laws of acceptable solutions must
be observed. To see this, assume we extend our previous examples with
assertions stating which county belongs to which states, and what decisions a
buyer must make to obtain a tax rebate in each state. The first assertions are
part of the laws of possible environments, while the second assertions are
part of the laws of acceptable solutions. If the property is known to be in a
county, it is safe to conclude from the first set of assertions that the
property is also in the state of that county: it is not necessary to observe
the state in which it is. By contrast, suppose that the buyer decides to claim
a tax rebate available in only one state. By the second set of assertions, the
system concludes that the property must be in that state, but this is not a
safe conclusion. Indeed, it is clear that this conclusion must be verified by
observing the environment, and if the property is observed to be in another
state, the user must be informed that he cannot claim that tax rebate.

To further assist the user in their task, the system can also determine which
observations can bring useful information for the search. Suppose that a lower
tax rate can be obtained only if the property is energy efficient and will be
used for housing. If the buyer does not plan to use it for housing, then the
energy efficiency does not need to be known. To capture this kind of scenario,
we introduce a notion of _relevance_ : informally, a symbol is relevant when
it is an essential part of a solution. Relevance is instrumental in reducing
the number of observations and decisions the user has to make. This is
especially valuable when such observations are costly. Past efforts to
determine relevant symbols in the context of interactive configuration have
used so-called _activation rules_ , i.e., rules that determine when symbols
become relevant. These activation rules have to be added manually by the
knowledge engineer. Our approach eliminates the need for such rules, and
automatically derives the relevance of symbols based on their occurrence in
minimal solutions instead. Furthermore, we propose an approximate, but
efficient, method to derive relevance automatically, using standard solvers.

The rest of this paper is organized as follows. In Section 2, we introduce the
logic concepts we use in this paper. Next, we formalize model expansion in a
two-theory setting: one describing valid solutions and another describing
possible environments, with a clear distinction between environmental and
decision symbols (Section 3). In Section 4 and 5, we formalize the concept and
operation of an assistant for interactive model expansion in that setting.
Then, we define partial solutions with enough observations and decisions to
guarantee that complete and appropriate solutions exist (Section 6). We define
relevant symbols (Sections 7), and present an efficient method to over-
approximate the set of relevant symbols. Finally, we evaluate our
implementation (Section 8) and compare it to related work (Section 9)

##  2 Preliminaries

We assume familiarity with syntax and semantics of propositional logic and
first-order logic (FO). To keep the presentation light, we develop our theory
for propositional logic, but, in fact, the concepts we define apply to all
logics with a model semantics. Our examples use a fragment of first-order
logic.

A vocabulary $\Sigma$ is a set of symbols. A theory is a set of formulae
constructed from these symbols using the logic connectives
$\lnot,\land,\lor,\Rightarrow,\Leftrightarrow$ (negation, conjunction,
disjunction, material implication, equivalence). A partial (resp. total)
structure of $\Sigma$ is a partial (resp. total) function from $\Sigma$ to
$\\{\mathbf{t},\mathbf{f}\\}$, giving a Boolean value (a.k.a. interpretation)
to each symbol. The value of a symbol $\sigma\in\Sigma$ in a structure $S$ is
denoted by $\sigma^{S}$ if it exists. In this case, we say that $\sigma$ is
interpreted by $S$, and that the _fact_ “$\sigma$ has the value denoted by
$\sigma^{S}$” is true in $S$. The set of interpreted symbols of $S$ is denoted
by $\Sigma_{S}$. If $S$ is a total structure of $\Sigma$, we can determine the
truth-value of all well-formed expressions and theories $e$ over $\Sigma$; the
resulting truth-value is denoted by $\llbracket e\rrbracket^{S}$. A total
structure $S$ that makes every formula in $T$ true is a _model_ of $T$; then,
$T$ is _satisfied_ by $S$.

We call a partial structure $S$ _less precise than_ $S^{\prime}$ (and write
$S\leq_{p}S^{\prime}$) if $\Sigma_{S}\subseteq\Sigma_{S^{\prime}}$ and all
facts true in $S$ are also true in $S^{\prime}$, i.e., if $S^{\prime}$ assigns
the same values as $S$ to the interpreted symbols of $S$ (it may interpret
more symbols). In this case, we call $S^{\prime}$ an _expansion of $S$_. The
set of total expansions of $S$ is denoted $\overline{S}$. A partial structure
$S$ is _consistent with $T$_ if it has a _model expansion_ for $T$, i.e., a
total expansion that satisfies $T$. It _entails $T$_ if all its total
expansions satisfy $T$. We say that $S$ and $S^{\prime}$ are _disjoint_ if
$\Sigma_{S}\cap\Sigma_{S^{\prime}}=\emptyset$. For two disjoint structures $S$
and $S^{\prime}$, we define $S+S^{\prime}$ to be the structure that maps
symbols $\sigma$ interpreted by $S$ to $\sigma^{S}$ and symbols interpreted by
$S^{\prime}$ to $\sigma^{S^{\prime}}$.

##  3 Split model expansion

We first consider the generic problem of (non-interactive) model expansion in
a two-theory setting, using two vocabularies, when the environment is fully
known. The first vocabulary, $\Sigma_{\mathit{env}}$, contains the _env
ironmental symbols_. The particular environment faced by the user is described
by a total structure $S_{\mathit{env}}$ for $\Sigma_{\mathit{env}}$. The
second vocabulary, $\Sigma_{\mathit{sol}}$, is disjoint from the first and
contains the decision symbols. A solution is fully described by a total
structure $S_{\mathit{sol}}$ for $\Sigma_{\mathit{sol}}$. The union of the 2
vocabularies is denoted by $\Sigma_{\mathit{all}}$.

We assume to have a theory $T_{\mathit{env}}$ over vocabulary
$\Sigma_{\mathit{env}}$ that contains the laws satisfied by any environment
that could be faced by the user. Any structure $S_{\mathit{env}}$ that
describes a particular environment is a model of $T_{\mathit{env}}$. We also
assume that the constraints on the solution to the problem faced by the user
are formalized by a logic theory $T_{\mathit{sol}}$ in the vocabulary
$\Sigma_{\mathit{all}}$. This theory fully captures all knowledge about when a
solution is valid in a given environment.

###### Definition 1

The _split model expansion problem_ $\mathcal{SMX}$ is a problem that takes as
input a tuple
$(\Sigma_{\mathit{env}},\Sigma_{\mathit{sol}},S_{\mathit{env}},T_{\mathit{env}},T_{\mathit{sol}})$
where $S_{\mathit{env}}$ is a total structure over $\Sigma_{\mathit{env}}$,
$T_{\mathit{env}}$ is a theory over $\Sigma_{\mathit{env}}$ satisfied by
$S_{\mathit{env}}$, and $T_{\mathit{sol}}$ is a theory over
$\Sigma_{\mathit{env}}\cup\Sigma_{\mathit{sol}}$.
A _total solution_ for such a problem is a total structure $S_{\mathit{sol}}$
over $\Sigma_{\mathit{sol}}$ such that

$\llbracket
T_{\mathit{sol}}\rrbracket^{S_{\mathit{env}}+S_{\mathit{sol}}}=\mathbf{t}.$

Note that $T_{\mathit{env}}$ is not used in the definition of the total
solution because we assume that the environment satisfies $T_{\mathit{env}}$
already. Having $T_{\mathit{env}}$ as an additional input is useful in the
process of finding a solution when the environment $S_{\mathit{env}}$ is not
fully known, but observable, as discussed in the next sections.

###### Example 1

We consider a simplified tax legislation for the sale of real estate, defined
as follows. The tax amount is 10 $\%$ of the sales price for standard
registration with the authorities, but a lower tax rate can be obtained when
the house is bought to be leased to tenants for a low rent, or when the seller
is licensed to sell social housing.

The environmental symbols we use to describe the seller and the house are
propositions; the decision symbols are nullary function symbols: the type of
registration (whose value is either $\mathit{Social},\mathit{Modest}$ or
$\mathit{Other}$) and the tax rate (an integer). The states of affairs are
described by structures over these vocabularies:

$\displaystyle\Sigma_{\mathit{env}}$
$\displaystyle=\\{\mathit{SocialHousing},\mathit{LicensedSeller},\mathit{LowRent}\\}.$
$\displaystyle\Sigma_{\mathit{sol}}$
$\displaystyle=\\{\mathit{RegistrationType},\mathit{TaxRate}\\}.$

The theory $T_{\mathit{env}}$ about the possible environments states that a
social housing is necessarily leased at a low rent.

$\mathit{SocialHousing}\Rightarrow\mathit{LowRent}.$

The legislation is described by $T_{\mathit{sol}}$, stating the prerequisites
for the types of registration, and the corresponding tax rate (where equality
is interpreted as in first order logic):

$\displaystyle\mathit{RegistrationType}{=}\mathit{Modest}\Rightarrow\mathit{LowRent}.$
$\displaystyle\mathit{RegistrationType}{=}\mathit{Social}\Rightarrow\mathit{LicensedSeller}\land\mathit{SocialHousing}.$
$\displaystyle\mathit{TaxRate}{=}1~{}\Leftrightarrow\mathit{RegistrationType}{=}\mathit{Social}.$
$\displaystyle\mathit{TaxRate}{=}7~{}\Leftrightarrow\mathit{RegistrationType}{=}\mathit{Modest}.~{}$
$\displaystyle\mathit{TaxRate}{=}10\Leftrightarrow\mathit{RegistrationType}{=}\mathit{Other}.~{}~{}$

A possible sale is described by $S_{\mathit{env}}$=
$\\{\mathit{SocialHousing}{=}\mathbf{t},LicencedSeller{=}\mathbf{t},\mathit{LowRent}{=}\mathbf{t}\\}$.
The split model expansion problem has 3 total solutions:

$\displaystyle\\{\mathit{TaxRate}{=}1,\mathit{RegistrationType}{=}\mathit{Social}\\},$
$\displaystyle\\{\mathit{TaxRate}{=}7,\mathit{RegistrationType}{=}\mathit{Modest}.\\},\text{
and}$
$\displaystyle\\{\mathit{TaxRate}{=}10,\mathit{RegistrationType}{=}\mathit{Other}.\\}.$

An interactive assistant for this theory is available
online.222https://tinyurl.com/simpleRegistration

##  4 Interactive model expansion

Often, a problem has many acceptable solutions in a given environment. Instead
of choosing a particular solution by automated model expansion (Mitchell et
al., 2006), it is preferable that the automated system allow the user to
explore the set of acceptable solutions. For example, a property tax
legislation may allow the buyer to register the sales in different ways, as in
Example 1, and the system should allow them to see the various prerequisites
and consequences of each valid options, e.g., on the tax rate.

We call the two interacting agents System and User. System offers User the
freedom to choose values for environmental and decision symbols while
verifying the validity of the solution that User constructs with respect to
the 2 theories, $T_{\mathit{env}}$ and $T_{\mathit{sol}}$. Since a system is
often designed for many users, and each user wants a solution for their own
environment, we assume it is the task of User to communicate information about
their environment to System. User may have additional knowledge that is
unknown to System. Indeed, it is often the case that some tacit knowledge is
not formalized in the theories, but well known by the user. Obviously, System
cannot use this tacit knowledge; instead, User must use it in the appropriate
way.

At each step of an interactive process, User has constructed two partial
structures, $S_{\mathit{obs}}$ and $S_{\mathit{dec}}$, assigning values to
environmental and decision symbols respectively. Those values correspond to
observations and to (tentative) decisions respectively.

###### Definition 2

A _state of the interactive process_ is a pair of partial structures
$(S_{\mathit{obs}},S_{\mathit{dec}})$ such that $S_{\mathit{obs}}$ (resp.
$S_{\mathit{dec}}$) is a partial structure over $\Sigma_{\mathit{env}}$ (resp.
$\Sigma_{\mathit{sol}}$).

By contrast, in prior work where there is no distinction between environmental
and decision symbols, the state is described by only one partial structure.

Although System only has the information that User has provided to it, it also
knows $T_{\mathit{env}}$ and $T_{\mathit{sol}}$; hence, it can verify that the
state is consistent with $T_{\mathit{env}}$ and $T_{\mathit{sol}}$:

###### Definition 3

A state $(S_{\mathit{obs}},S_{\mathit{dec}})$ is _consistent_ (with
$T_{\mathit{env}}$ and $T_{\mathit{sol}}$) iff there is an expansion of the
state that satisfies both theories:

$\exists S\in\overline{S_{\mathit{obs}}+S_{\mathit{dec}}}:\llbracket
T_{\mathit{env}}\cup T_{\mathit{sol}}\rrbracket^{S}=\mathbf{t}$

During the interactive process, decisions can be added and retracted. This
leads to the following definition:

###### Definition 4

An _interactive process_ for a problem $\mathcal{SMX}$ with input
$(\Sigma_{\mathit{env}},\Sigma_{\mathit{sol}},S_{\mathit{env}},T_{\mathit{env}},T_{\mathit{sol}})$
is a sequence
$(S_{\mathit{obs}}^{\mathit{i}},S_{\mathit{dec}}^{\mathit{i}})_{0<i\leq n}$ of
$n$ consistent states, such that, at each step, either the set of observations
or the set of decisions is made either more precise or less precise, i.e., for
any $0<i<n$:

  * •

$(S_{\mathit{obs}}^{\mathit{i}}<_{p}S_{\mathit{obs}}^{\mathit{i+1}}\lor
S_{\mathit{obs}}^{\mathit{i+1}}<_{p}S_{\mathit{obs}}^{\mathit{i}})\land
S_{\mathit{dec}}^{\mathit{i}}=S_{\mathit{dec}}^{\mathit{i+1}}$

  * •

or,
$S_{\mathit{obs}}^{\mathit{i}}=S_{\mathit{obs}}^{\mathit{i+1}}\land(S_{\mathit{dec}}^{\mathit{i}}<_{p}S_{\mathit{dec}}^{\mathit{i+1}}\lor
S_{\mathit{dec}}^{\mathit{i+1}}<_{p}S_{\mathit{dec}}^{\mathit{i}})$.

In the interactive process, User and System work together towards a solution
as follows:

  * •

The interaction starts with a pair of empty structures,
$(S_{\mathit{obs}},S_{\mathit{dec}})$. If this state is inconsistent with
$T_{\mathit{env}}$ and $T_{\mathit{sol}}$, System tells User that there is no
solution to the split model expansion problem.

  * •

User can make $S_{\mathit{obs}}$ or $S_{\mathit{dec}}$ more precise as long as
the new state is consistent. System prevents User from changing their
decisions $S_{\mathit{dec}}$ to an inconsistent state because it would not
bring them closer to a solution. If User needs to make $S_{\mathit{obs}}$ more
precise following an observation, and if this change makes the state
inconsistent, System asks User to retract a decision first so that the new
observation can then be added without making the state inconsistent. To
facilitate this task, System shows the list of decisions that, if retracted,
would allow the entry. This list is the list of interpretations in the
$\leq_{p}$-minimal structure $S$ less precise than $S_{\mathit{dec}}$ that,
together with $S_{\mathit{obs}}$, is inconsistent with
$T_{\mathit{env}}\bigcup T_{\mathit{sol}}\bigcup O$, where $O$ is the
observation to be added. It can be obtained using unsat_core methods (Cimatti
et al., 2007). By repeatedly making the state more precise while keeping it
consistent, User eventually obtains a total solution.

  * •

User can make $S_{\mathit{obs}}$ or $S_{\mathit{dec}}$ less precise, i.e.,
retract past observations and decisions. The resulting state is necessarily
consistent. This allows User to explore the complete space of solutions in
their environment.

###### Example 2

Returning to Example 1, assume that User first decides that
$\mathit{RegistrationType}{=}\mathit{Social}$. The corresponding state
$(\\{\\},\\{\mathit{RegistrationType}{=}\mathit{Social}\\})$ is consistent.
They proceed by observing $\lnot\mathit{SocialHousing}$. This cannot be added
to the state because $\mathit{SocialHousing}$ is a prerequisite for a
$\mathit{Social}$ registration, per $T_{\mathit{sol}}$. User thus needs to
retract their only decision ($\mathit{RegistrationType}{=}\mathit{Social}$)
before entering their observation.

Suppose instead that User selects
$\mathit{RegistrationType}{=}\mathit{Social}$ followed by
$\mathit{LowRent}{=}\mathbf{f}$. The resulting state is consistent with
$T_{\mathit{sol}}$ in the absence of $T_{\mathit{env}}$. However, the state is
inconsistent with $T_{\mathit{env}}$ because a $\mathit{Social}$ registration
can only be done for a social housing, which is necessarily leased at a low
rent. User must backtrack on their decision
$\mathit{RegistrationType}{=}\mathit{Social}$ before entering the observation
that the housing is not leased at a low rent.

Note that the presence of $T_{\mathit{env}}$ reduces the number of consistent
states, and thus shortens the search for a solution.

##  5 Propagation

System further assists User by informing them of the logical consequences of
what is known in the current state. Such knowledge is of great value to User,
and is used in most interactive assistant tools (Van Hertum et al., 2017;
Falkner et al., 2019). It reduces the number of decisions that User has to
make, and shortens the interaction in a way analogous to how unit propagation
accelerates the naive backtracking algorithm in propositional satisfiability
checking. The consequences of what is known are determined by a computation
called _propagation_ (or _backbone_ computation).

###### Definition 5

A partial structure $S^{\prime}$ is a _$T$ -propagation_ of a partial model
$S$ of $T$ iff it is an expansion of $S$ with the same set of model expansions
for $T$ as $S$, i.e.,

  * •

$S\leq_{p}S^{\prime}$

  * •

$\forall M\in\overline{S}:(\llbracket T\rrbracket^{M}=\mathbf{t}\Rightarrow
M\in\overline{S^{\prime}})$

Structure $S^{\prime}$ expands $S$ by selecting some of the uninterpreted
symbols whose value is the same in all models of $T$ that expand $S$, and
assigning them that value. We call $S^{\prime}$ the _optimal propagation_ of
$S$ with respect to $T$ if it is the most precise $T$-propagation. Algorithms
to compute propagation are discussed in the literature (e.g., Zhang et al.,
(2019)).

In our interactive assistant framework, a complication arises when propagation
derives facts for environmental symbols using the theory of solutions. In
general, there is no guarantee that these facts are true in the environment
faced by the user. To address this issue, we first propagate using
$T_{\mathit{env}}$ only, and then using both $T_{\mathit{env}}$ and
$T_{\mathit{sol}}$. This will further demonstrate the benefits of the split
theory setting.

Because $T_{\mathit{env}}$ only concerns environmental symbols, the
propagation of $S_{\mathit{obs}}$ by $T_{\mathit{env}}$ can assign new values
only to environmental symbols. We denote the structure containing these new
values by $S_{\mathit{obs}}^{e}$. The propagation of the state by both
$T_{\mathit{env}}$ and $T_{\mathit{sol}}$, i.e., by $T_{\mathit{all}}$, can
assign new values to both environmental and decision symbols. We denote the
structures containing these new values by $S_{\mathit{obs}}^{a}$ and
$S_{\mathit{dec}}^{a}$. The structures $S_{\mathit{obs}}^{e}$,
$S_{\mathit{obs}}^{a}$ and $S_{\mathit{dec}}^{a}$ are disjoint. System
displays these structures differently:

  * •

$S_{\mathit{obs}}^{e}$: The new environmental facts obtained by propagation of
$S_{\mathit{obs}}$ using $T_{\mathit{env}}$ are shown as consequences to User:
they do not need to be verified by observing the environment. This is safe
because the propagated facts are true in the environment of User, by the
definition of $T_{\mathit{env}}$.

  * •

$S_{\mathit{obs}}^{a}$: The new environmental facts obtained by propagation of
the state using $T_{\mathit{all}}$ are shown as prerequisites of his
decisions, to be verified by observing the environment. Indeed, there is no
guarantee that they are true in the environment faced by User. The observation
of the environment may occur at a later stage of the interactive process. If
the observation does match the value obtained by propagation, User adds it to
the state $S_{\mathit{obs}}$; the state will remain consistent. If the
observation does not match, adding it would make the state inconsistent: User
must first retract a decision to allow the entry, as explained in Section 4.

  * •

$S_{\mathit{dec}}^{a}$: The new decision facts obtained by propagation of the
state using $T_{\mathit{all}}$ are shown as consequences to User. User cannot
just change such a value, since that would cause inconsistency. If User wants
to update the propagated value, they first need to retract decisions that led
to the propagation.

###### Example 3

Returning to Ex. 1, the optimal propagation of the state
$(\\{\mathit{LowRent}{=}\mathbf{f},$ $\mathit{SocialHousing}{=}\mathbf{f}\\},$
$\\{\\})$ is $S_{\mathit{env}}^{e}=\\{\\},S_{\mathit{env}}^{a}=\\{\\}$ and
$S_{\mathit{dec}}^{a}=\\{\mathit{RegistrationType}{=}\mathit{Other},$
$\mathit{TaxRate}{=}10\\}$: no observation needs to be verified. On the other
hand, the optimal propagation of $(\\{\\},\\{\mathit{TaxRate}=7\\})$ is
$S_{\mathit{env}}^{e}=\\{\\},S_{\mathit{env}}^{a}=\\{\mathit{LowRent}{=}\mathbf{t}\\}$
and $S_{\mathit{dec}}^{a}=\\{\mathit{RegistrationType}{=}\mathit{Modest}\\}$
where $\\{\mathit{LowRent}{=}\mathbf{t}\\}$ needs to be verified.

##  6 Partial solutions

We now consider other forms of acceptable solutions. For example, it may not
be necessary to observe the environment fully. In addition, some decisions may
be unnecessary, in the sense that they can be made arbitrarily without
impacting the result. Finally, the user may postpone some decisions when they
have the guarantee that a solution exists.

We define definite and contingent solutions. A _definite_ solution entails the
satisfaction of $T_{\mathit{sol}}$, assuming $T_{\mathit{env}}$:

###### Definition 6

A _definite solution_ of the split model expansion problem $\mathcal{SMX}$ is
a state $(S_{\mathit{obs}},S_{\mathit{dec}})$ such that (i) all facts in
$S_{\mathit{obs}}$ are true in $S_{\mathit{env}}$ and (ii) $T_{\mathit{sol}}$
is satisfied by every expansion $S_{o}$ of $S_{\mathit{obs}}$ that satisfies
$T_{\mathit{env}}$ and by every expansion $S_{d}$ of $S_{\mathit{dec}}$,

$\forall S_{o}\in\overline{S_{\mathit{obs}}}:\llbracket
T_{\mathit{env}}\rrbracket^{S_{o}}=\mathbf{t}\Rightarrow\forall
S_{d}\in\overline{S_{\mathit{dec}}}:\llbracket
T_{\mathit{sol}}\rrbracket^{S_{d}+S_{o}}=\mathbf{t}$

Notice that Definition 6 treats $T_{\mathit{env}}$ and $T_{\mathit{sol}}$ very
differently. This is because even though we do not know the full structure
$S_{\mathit{env}}$, we do know that it exists, that it is more precise than
$S_{\mathit{obs}}$, and that it satisfies $T_{\mathit{env}}$. For this reason,
we only need to consider expansions of $S_{\mathit{obs}}$ that satisfy
$T_{\mathit{env}}$. For such expansions, it should be the case that no matter
how we make our choices, we obtain a solution to the problem at hand.

###### Example 4

A definite solution for the simplified real estate problem without any prior
observation is $(\\{\\},$
$\\{\mathit{RegistrationType}{=}\mathit{Other},\mathit{TaxRate}{=}10\\})$.
Indeed, any sale can be registered with type $\mathit{Other}$ and a tax rate
of 10.

Any consistent state can be expanded into a definite solution. Indeed, by
definition, every consistent state can be expanded into a total solution,
which is a definite solution. In practice, definite solutions are often
partial, not total, structures. As soon as User has found a definite solution,
they can stop making observations and decisions. Indeed, such a solution can
always be expanded to construct total solutions of the problem, by further
observing the environmental and making any decision for the remaining decision
symbols.

In some cases, User only needs the guarantee that a solution is reachable in
their environment, by making the appropriate remaining decisions in a later
stage. Since they do not know their environment fully, establishing this
guarantee requires considering every environment more precise than what is
known:

###### Definition 7

A _contingent solution_ of the split model expansion problem $\mathcal{SMX}$
is a state $(S_{\mathit{obs}},S_{\mathit{dec}})$ such that (i) all facts in
$S_{\mathit{obs}}$ are true in $S_{\mathit{env}}$ and (ii) $T_{\mathit{sol}}$
is satisfied by at least one expansion $S_{d}$ of $S_{\mathit{dec}}$ for every
expansion $S_{o}$ of $S_{\mathit{obs}}$ that satisfies $T_{\mathit{env}}$,
i.e.,

$\forall S_{o}\in\overline{S_{\mathit{obs}}}:(\llbracket
T_{\mathit{env}}\rrbracket^{S_{o}}=\mathbf{t}\Rightarrow\exists
S_{d}\in\overline{S_{\mathit{dec}}}:\llbracket
T_{\mathit{sol}}\rrbracket^{S_{d}+S_{o}}=\mathbf{t})$

###### Example 5

A contingent solution for the simplified real estate problem without any prior
observation is $(\\{\\},$ $\\{\mathit{RegistrationType}=\mathit{Other}\\})$.
Indeed, any sale can be registered with type $\mathit{Other}$. The tax rate
can be computed later (in this case easily).

### Complexity

The complexity of deciding whether a state is a contingent or definite
solution is much higher than checking whether it is consistent and total. In
the context of propositional logic, checking for definite solution is
$\Pi^{p}_{1}$-complete (coNP-complete) while checking for contingent solution
is $\Pi^{p}_{2}$-complete. In Section “Implementation”, we propose a cheap
approximate method to solve this problem.

##  7 Relevance

We now turn to the question of determining which observations are relevant for
the search. We have shown that uninterpreted symbols in a definite solution
$(S_{\mathit{obs}},S_{\mathit{dec}})$ are _irrelevant_ (or “do-not-care”) in
the following sense: $S_{\mathit{dec}}$ extended with _any_ interpretation for
these symbols will satisfy $T_{\mathit{sol}}$ in _any_ possible environment
that expands $S_{\mathit{obs}}$ while satisfying $T_{\mathit{env}}$. In this
section, we extend the notion of relevance to any state.

###### Definition 8

A _$\leq_{p}$ -minimal definite solution_ is a definite solution that is not
more precise than another definite solution. We denote the set of minimal
definite solutions more precise than a state by
$MinDef(S_{\mathit{obs}},S_{\mathit{dec}})$.

A minimal contingent solution is similarly defined; the set is denoted by
$MinCont(S_{\mathit{obs}},S_{\mathit{dec}})$.

###### Definition 9

The symbol $\sigma$ in $\Sigma_{\mathit{all}}$ is _relevant_ in the consistent
state $(S_{\mathit{obs}},S_{\mathit{dec}})$ if, and only if, it is interpreted
in at least one $\leq_{p}$-minimal definite solution more precise than the
state, i.e.,

$\exists S\in MinDef(S_{\mathit{obs}},S_{\mathit{dec}}):\sigma\in\Sigma_{S}$

By our definition, all symbols interpreted in the state are relevant. As soon
as User enters a value for a relevant symbol, the state is updated and the
list of relevant symbols can be re-computed.

###### Proposition 1

If there are no uninterpreted relevant symbols in a consistent state, the
state is a definite solution.

######  Proof 7.1.

Suppose $(S_{\mathit{obs}},S_{\mathit{dec}})$ is a consistent state without
uninterpreted relevant symbols. By the definition of consistency, there is a
total solution (and hence, a definite) solution that is more precise than
$(S_{\mathit{obs}},S_{\mathit{dec}})$, meaning that the set of definite
solutions that expand $(S_{\mathit{obs}},S_{\mathit{dec}})$ is non-empty. As a
consequence (using the fact that $\leq_{p}$ is a well-founded order on the set
of states of a fixed and finite vocabulary), this set has at least one
$\leq_{p}$-minimal element. Let
$(S_{\mathit{obs}}^{\prime},S_{\mathit{dec}}^{\prime})$ be such a
$\leq_{p}$-minimal definite solution that expands
$(S_{\mathit{obs}},S_{\mathit{dec}})$. By Def. 9, all symbols on which
$(S_{\mathit{obs}}^{\prime},S_{\mathit{dec}}^{\prime})$ and
$(S_{\mathit{obs}},S_{\mathit{dec}})$ differ are relevant. Since, by our
assumption, all relevant symbols are interpreted in
$(S_{\mathit{obs}},S_{\mathit{dec}})$ (and thus also in
$(S_{\mathit{obs}}^{\prime},S_{\mathit{dec}}^{\prime})$), the state and the
definite solution are actually equal.

######  Proposition 7.2.

If there are no uninterpreted relevant environmental symbols in a consistent
state, the state is a contingent solution.

######  Proof 7.3.

Similarly to the previous proof, suppose $(S_{\mathit{obs}},S_{\mathit{dec}})$
is a consistent state without uninterpreted relevant environmental symbols.
Let $(S_{\mathit{obs}}^{\prime},S_{\mathit{dec}}^{\prime})$ be a
$\leq_{p}$-minimal contingent solution that expands
$(S_{\mathit{obs}},S_{\mathit{dec}})$. By the definition, all symbols on which
$(S_{\mathit{obs}}^{\prime},S_{\mathit{dec}}^{\prime})$ and
$(S_{\mathit{obs}},S_{\mathit{dec}})$ differ are relevant. Since, by our
assumption, all relevant environmental symbols are interpreted in
$(S_{\mathit{obs}},S_{\mathit{dec}})$ (and thus also in
$(S_{\mathit{obs}}^{\prime},S_{\mathit{dec}}^{\prime})$), $S_{\mathit{obs}}$
and $S_{\mathit{obs}}^{\prime}$ are equal. Since the state differs from the
contingent solution only by the decisions and is consistent, it is a
contingent solution too.

These properties allow System to alert User when a definite (resp. contingent)
solution has been found. In propositional logic, the problem of computing
whether a symbol $\sigma$ is relevant in some state is
$\Sigma^{p}_{3}$-complete. While computing the set of relevant symbols is
computationally expensive, it can be approximated cheaply, as discussed in the
next section.

######  Example 7.4.

When $\\{\mathit{LowRent}{=}\mathbf{f}\\}$, $\mathit{LicensedSeller}$ is
irrelevant. Indeed, $\mathit{RegistrationType}$ cannot be $\mathit{Social}$
nor $\mathit{Modest}$, and the only $\leq_{p}$-minimal definite solution is
$\\{\mathit{LowRent}{=}\mathbf{f},$
$\mathit{TaxRate}{=}10,\mathit{RegistrationType}{=}\mathit{Other}\\}$, in
which $\mathit{LicensedSeller}$ is uninterpreted.

##  8 Implementation and validation

We developed a decision support tool that embodies our proposal, called the
Interactive Consultant. Given two vocabularies
$(\Sigma_{\mathit{env}},\Sigma_{\mathit{sol}})$ and two theories
($T_{\mathit{env}}$ and $T_{\mathit{sol}}$), the tool generates a user
interface that allows the user to follow the proposed interactive process,
with the benefit of computer-generated guidance. The tool supports theories in
$\mathrm{FO}(\cdot)$, i.e., in first-order logic extended with types,
aggregates, linear arithmetic over infinite domains, and (possibly inductive)
definitions.333https://fo-dot.readthedocs.io/ It uses the IDP-Z3 reasoning
engine for $\mathrm{FO}(\cdot)$ (Carbonnelle et al., 2022)444www.idp-z3.be,
which is based on the Z3 SMT solver (de Moura and Bjørner, 2008). The tool and
its source code are available online.555https://interactive-
consultant.idp-z3.be/ and https://gitlab.com/krr/IDP-Z3

The user enters an observation or a decision by clicking on buttons or
entering values in fields. The interactive advisor 1) updates the state, 2)
propagates the state using $T_{\mathit{env}}$, 2) propagates again using
$T_{\mathit{env}}\land T_{\mathit{sol}}$, and 3) determines the relevant
symbols. The user interface is then updated to reflect the attributes and
state of symbols: environmental vs. decision symbol, relevant, propagated.
When there are no _environmental_ symbols that are both relevant and
uninterpreted, the solution is known to be a contingent solution for the
environment. When there is no symbol that is both relevant and uninterpreted,
the solution is known to be a definite solution for the environment, and the
user can stop observing and making decisions.

Because relevance, as defined in Section 7, is expensive to compute, we
approximate it using a 2-step process: 1) we compute propagation in state
$(S_{\mathit{obs}},S_{\mathit{dec}})$ as discussed in Section 5 and create
theory $C$ consisting of the propagated literals;666I.e., if the
$T_{\mathit{all}}$-propagation contains $\\{p=\mathbf{t},q=\mathbf{f}\\}$,
theory $C$ contains $\\{p.\lnot q.\\}$. 2) we replace atoms occurring in the
grounded777The grounded version is obtained by expanding quantifications and
aggregates over their (finite) domain. version of $T_{\mathit{all}}$ by their
value in the state (including propagated values), if any, and we simplify the
formula using the laws of logic and arithmetic, to obtain
$T_{\mathit{all}}^{*}$. Then, the set of definite solutions that extend state
$(S_{\mathit{obs}},S_{\mathit{dec}})$ for theory $C\cup T_{\mathit{all}}^{*}$
is the set of such solutions for theory $T_{\mathit{all}}$, i.e., $C\cup
T_{\mathit{all}}^{*}$ and $T_{\mathit{all}}$ are equivalent in that state. The
symbols that do not occur in theory $C\cup T_{\mathit{all}}^{*}$ cannot be
relevant: indeed, changing their value cannot change the truth-value of
$T_{\mathit{all}}$ in the state. Thus, theory $C\cup T_{\mathit{all}}^{*}$
contains all the symbols that are relevant in the state; it may also contain
some irrelevant symbols, depending on how thoroughly the propagation and
simplification is performed, but this is acceptable in practice. Since Step 1
is computed for the reasons given in Section 5, the additional cost of
computing relevance is only determined by Step 2, and can be very low and
still be useful to the user.

Definitions stated in the theory require special care when determining
relevance. _Definitions_ specify a unique interpretation of a defined symbol,
given the interpretation of its parameters. They take the form of an
equivalence between the defined atom and a _definiens_ , i.e., a logic formula
that defines it. A defined atom can be made irrelevant by replacing it by its
definiens in the theory: the transformed theory will be equivalent (except for
the defined symbol), and the defined atom will not occur in it anymore. Yet,
defined atoms are often relevant for the user as it abstracts complexity in a
useful way. Thus, we distinguish definitions from the other logical sentences
in the theory. We consider a ground atom relevant if, and only if, it is
important for the user to know its value, or it occurs in a simplified logical
sentence, or it occurs in the simplified definition of a ground atom
previously considered relevant.

To validate our approach, we have configured the decision support tool for
Example 1 (available online888https://tinyurl.com/simpleRegistration). Our
tests showed that the system effectively assists the user by correctly
determining which hypotheses must be verified, and which observations are
relevant.

We then performed experiments on the real estate legislation adapted from
Deryck et al., (2019) (available
online999https://tinyurl.com/BelgianRegistration). We simulate the user by a
robot entering values in the user interface in a random order. We measured how
many decisions and observations the robot has to make, using two approaches:

  * •

using the traditional approach where the problem instance is fully known
before model expansion; the user enters the observations before his decisions,
and stops when he finds a total solution;

  * •

using our approach; the user only enters relevant observations and decisions,
until he finds a definite solution.

In the traditional approach, the user has to make an average of 26.4 entries
to obtain a model;101010Depending on the order of data entry, the value of
some environmental symbols may be derived by propagation of
$T_{\mathit{env}}$: in that case, the user does not have to enter a value for
them. with the approach we propose, the user only needs to make 11.6 entries
to obtain a definite solution, a 56% reduction (see details in Appendix). This
reduction in the user’s workload is also observed in other realistic use cases
(Aerts et al., 2022).

##  9 Related work

The configuration problem, i.e., the problem of configuring a complex system
out of simpler components to satisfy customer requirements, is a special case
of model expansion that has been studied, e.g., by Felfernig et al., 2014b .
Several authors have discussed interactive tools to solve configuration
problems (Hotz et al., 2014; Madsen, 2003; Van Hertum et al., 2017; Falkner et
al., 2019). Our work is orthogonal to these studies. Indeed, the explicit
distinction we make between environmental and decision symbols, and between
the theory of the environment and the theory of acceptable solutions, can be
combined with the ideas from earlier work. To illustrate this, our interactive
tool supports the 8 reasoning tasks identified as useful by Van Hertum et al.,
(2017).

Several approaches for controlling the relevance of symbols in configuration
problems have been proposed. In these approaches, the modeler has the
responsibility to write so-called _activation rules_ that explicitly specify
when a symbol becomes active (as done by Mittal and Falkenhainer, (1990);
Bowen and Bahler, (1991) in Dynamic CSPs), or even when an entire component
becomes active (as done by Stumptner and Haselböck, (1993) in Generative
CSPs). Our approach does not need activation rules to derive relevance of
symbols. Jansen et al., (2016) also propose an approach without activation
rules, based on justification theory. Its implementation requires a custom
solver (Deryck et al., 2019). By contrast, our implementation uses a standard
SMT solver.

To facilitate decision-making in companies, the Object Management Group has
published a widely accepted standard in the business process communities,
called the Decision Model and Notation standard (DMN) (OMG, 2021). One
extension of DMN, called cDMN (Vandevelde et al., 2021), further increases the
expressivity of the notation. Decision models in those two notations can be
translated automatically into $\mathrm{FO}(\cdot)$ (Vandevelde et al., 2021),
allowing our Interactive Consultant to support decision-making in companies.
These DMN representations would be enhanced by using two vocabularies and two
theories, as we propose, further highlighting the relevance of our work.

Our two-theory setting has some similarity with distributed constraint
satisfaction problems, i.e., problems where several agents, each with their
own constraints, search for a solution that satisfies their constraints
(Yokoo, 2012). Here, the environment, System and User may be viewed as agents,
each with their own set of constraints. In our case, however, the theory of
the environment is used by another agent, the interactive assistant.

The concept of relevance has been discussed in a special issue of Artificial
Intelligence in 1997 (Subramanian et al., 1997), focusing on autonomous
systems with limited computational resources. Relevance has been applied to
improve the performance of propositional satisfiability solvers (Jansen et
al., 2016). Instead, we apply it to reduce the workload of the user, by
showing them the observations and decisions that make them progress in their
search of a solution.

##  10 Conclusion

In this paper, we have studied the problem of model expansion in an unknown,
but observable, environment in a precise and formal way. It was crucial to
make an _explicit_ distinction between environmental and decision symbols, as
well as between the laws of possible environments and the laws of acceptable
solutions. Additionally, we have shown how to reduce, safely, the number of
observations and decisions to be made by the user of an interactive assistant
in such a setting.

Relevance is an interesting topic for future work. The partial solutions we
describe entail the satisfaction of the whole theory of acceptable solutions,
given the environment. Sometimes, the user is interested in ensuring that a
more limited goal is entailed by their decisions. By determining relevance
relative to a goal, the number of observations can be further reduced.
Furthermore, one could investigate whether some observations and decisions are
more relevant than others.

Our approach could be generalized to problems with multiple agents
participating in a model expansion, each with their own goals and constraints,
e.g., in Community-based Configuration problems (Felfernig et al., 2014a ) and
Distributed Constraint Satisfaction (Yokoo, 2012).

##  11 Competing interests

The authors declare none.

## References

  * Aerts et al., (2022) Aerts, B., Deryck, M., and Vennekens, J. 2022\.  Knowledge-based decision support for machine component design: A case study.  Expert Syst. Appl., 187, 115869.
  * Bowen and Bahler, (1991) Bowen, J. and Bahler, D. Conditional existence of variables in generalised constraint networks.  In Dean, T. L. and McKeown, K. R., editors, Proceedings of the 9th National Conference on Artificial Intelligence 1991, pp. 215–220. AAAI Press.
  * 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.
  * Cimatti et al., (2007) Cimatti, A., Griggio, A., and Sebastiani, R. A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories.  In Marques-Silva, J. and Sakallah, K. A., editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings 2007, volume 4501 of Lecture Notes in Computer Science, pp. 334–339. Springer.
  * de Moura and Bjørner, (2008) de Moura, L. M. and Bjørner, N. Z3: An efficient SMT solver.  In Ramakrishnan, C. R. and Rehof, J., editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008 2008, volume 4963 of Lecture Notes in Computer Science, pp. 337–340. Springer.
  * Deryck et al., (2019) Deryck, M., Vennekens, J., Devriendt, J., and Marynissen, S. Legislation in the knowledge base paradigm: Interactive decision enactment for registration duties.  In 13th IEEE International Conference on Semantic Computing, ICSC 2019, Newport Beach, CA, USA, January 30 - February 1, 2019 2019, pp. 174–177. IEEE.
  * Falkner et al., (2019) Falkner, A. A., Haselböck, A., Krames, G., Schenner, G., and Taupe, R. Constraint solver requirements for interactive configuration.  In Hotz, L., Aldanondo, M., and Krebs, T., editors, Proceedings of the 21st Configuration Workshop 2019, volume 2467 of CEUR Workshop Proceedings, pp. 65–72.
  * (8) Felfernig, A., Hotz, L., Bagley, C., and Tiihonen, J. Configuration-related research challenges.  In Felfernig, A., Hotz, L., Bagley, C., and Tiihonen, J., editors, Knowledge-based configuration: From research to business cases 2014a, chapter 15, pp. 191–7*192. Newnes.
  * (9) Felfernig, A., Hotz, L., Bagley, C., and Tiihonen, J. 2014b.  Knowledge-based configuration: From research to business cases.  Newnes.
  * Hotz et al., (2014) Hotz, L., Felfernig, A., Stumptner, M., Ryabokon, A., Bagley, C., and Wolter, K. Configuration knowledge representation and reasoning.  In Felfernig, A., Hotz, L., Bagley, C., and Tiihonen, J., editors, Knowledge-based configuration: From research to business cases 2014, chapter 6, pp. 41–72. Newnes.
  * Jansen et al., (2016) Jansen, J., Bogaerts, B., Devriendt, J., Janssens, G., and Denecker, M. Relevance for SAT(ID).  In Kambhampati, S., editor, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016 2016, pp. 596–602. IJCAI/AAAI Press.
  * Madsen, (2003) Madsen, J. N. 2003\.  Methods for interactive constraint satisfaction.  Master’s thesis, Department of Computer Science, University of Copenhagen.
  * Mitchell et al., (2006) Mitchell, D. G., Ternovska, E., Hach, F., and Mohebali, R. 2006\.  Model expansion as a framework for modelling and solving search problems.  Technical Report TR 2006-24, Simon Fraser University, Canada.
  * Mittal and Falkenhainer, (1990) Mittal, S. and Falkenhainer, B. Dynamic constraint satisfaction problems.  In Shrobe, H. E., Dietterich, T. G., and Swartout, W. R., editors, Proceedings of the 8th National Conference on Artificial Intelligence 1990, pp. 25–32. AAAI Press / The MIT Press.
  * OMG, (2021) OMG 2021\.  Decision Model and Notation (DMN).  https://www.omg.org/dmn/.  Accessed: 2021-02-22.
  * Stumptner and Haselböck, (1993) Stumptner, M. and Haselböck, A. A generative constraint formalism for configuration problems.  In Torasso, P., editor, Proceedings of Advances in Artificial Intelligence 1993, volume 728 of Lecture Notes in Computer Science, pp. 302–313. Springer.
  * Subramanian et al., (1997) Subramanian, D., Greiner, R., and Pearl, J. 1997\.  The relevance of relevance (editorial).  Artif. Intell., 97, 1-2, 1–5.
  * Van Hertum et al., (2017) Van Hertum, P., Dasseville, I., Janssens, G., and Denecker, M. 2017\.  The KB paradigm and its application to interactive configuration.  Theory Pract. Log. Program., 17, 1, 91–117.
  * Vandevelde et al., (2021) Vandevelde, S., Aerts, B., and Vennekens, J. 2021\.  Tackling the DM challenges with cDMN: A tight integration of DMN and constraint reasoning.  Theory and Practice of Logic Programming,, 1–24.
  * Yokoo, (2012) Yokoo, M. 2012\.  Distributed constraint satisfaction: Foundations of cooperation in multi-agent systems.  Springer Science & Business Media.
  * Zhang et al., (2019) Zhang, Y., Pu, G., and Zhang, M. SMTBCF: efficient backbone computing for SMT formulas.  In Ameur, Y. A. and Qin, S., editors, Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings 2019, volume 11852 of Lecture Notes in Computer Science, pp. 36–51. Springer.

##  Appendix A Detailed Validation Report

The theory to represent the real estate tax legislation has 27 environmental
symbols and two decision symbols. We created 5 problem instances by randomly
choosing $\Sigma_{\mathit{env}}$ structures that satisfy $T_{\mathit{env}}$.

To simulate the traditional approach, the robot enters the environmental data
in a random order, and at each step, propagation by $T_{\mathit{env}}$ is
performed. If the value of an environmental symbol is derived by this
$T_{\mathit{env}}$-propagation, the robot does not have to enter it. After all
environmental data is entered, the robot chooses decision values randomly
among those that remain possible, until he obtains a total solution.

To simulate the approach we propose, at each step, the robot fills in one
uninterpreted symbol, chosen randomly among the relevant ones, until he
obtains a definite solution. If the symbol is environmental, it enters the
value given by the problem instance; if it is a decision symbol, it chooses a
valid value at random. When the state becomes inconsistent, User retracts a
conflicting decision at random.

Table A 1 shows that the workload is significantly reduced when the system
determines which observations are relevant, and which observations must be
made in the environment to ensure the solution is definite, as we propose.

Table 1: The number of observations and decisions is greatly reduced with our proposal. |  |
---|---|---
| Count of Observations and Decisions
| Traditional | Our proposal
Sale 1 | 26 | 10
Sale 2 | 26 | 14
Sale 3 | 26 | 10
Sale 4 | 27 | 10
Sale 5 | 27 | 14
Average | 26.4 | 11.6
Gain |  | -14.8 (- 56 %)
|  |
|  |


that when $s=-1$, the lower-frequency losses are much smaller than the higher
ones after $5000$ iterations, while when $s=3$ the higher frequencies are
learned faster than the lower ones.

\begin{overpic}[width=433.62pt]{figures-1D/Fig5sm1}
\put(0.0,30.0){\rotatebox{90.0}{loss}} \put(40.0,-2.0){epochs} \end{overpic}

\begin{overpic}[width=433.62pt]{figures-1D/Fig5s0}
\put(0.0,30.0){\rotatebox{90.0}{loss}} \put(40.0,-2.0){epochs} \end{overpic}

\begin{overpic}[width=433.62pt]{figures-1D/Fig5s1}
\put(0.0,30.0){\rotatebox{90.0}{loss}} \put(40.0,-2.0){epochs} \end{overpic}

Figure 5: Frequency loss for $\ell=3$ (blue), $\ell=5$ (red), and $\ell=9$
(yellow) based on the squared $H^{s}$ norm as the loss function. Left: $s=-1$;
Middle: $s=0$; Right: $s=1$. The error bars are generated using the results
obtained by executions with thirty different random seeds. In the left figure,
the result of one of the thirty executions is omitted because the NN is
trapped by a local minimizer that is not a global one, making the NN not
converge to the target function.

###  F.2 Learning spherical harmonics on the unit sphere

In section 6.2, we train a NN with data derived from sampling function defined
on $\mathbb{S}^{2}$ at nonuniform points. The training data is a maximum
determinant set of 2500 points that comes from the so-called “spherepts”
dataset [Wright and Michaels, 2015]. In this experiment, the target function
is

$g(\mathbf{x})=\sum_{\ell=1}^{15}Y_{2\ell,0}(\mathbf{x}),$

where $Y_{2\ell,0}$ is the normalized zonal spherical harmonic function of
degree $2\ell$. Therefore, the spherical harmonic coefficients of $g$ defined
in eq. 4 satisfy $\hat{g}_{\ell,p}=1$ if $p=0$ and $\ell=2,4,\ldots,30$, and
$\hat{g}_{\ell,p}=0$ otherwise. We then train an NN with the squared $H^{s}$
norm as the loss function (see eq. 18) for $s=-1,0,2.5$. By 4, we need
$\ell_{\text{max}}\geq L=30$. We set $\ell_{\text{max}}=40$ in eq. 18,
assuming that the bandwidth $L$ is not known a priori. We observe frequency
biasing in this experiment by considering
$|\widehat{{\mathcal{N}}}_{\ell,p}-\hat{g}_{\ell,p}|$ after each epoch for
$\ell=4,10,20$. We confirm that low frequencies of $g$ are captured earlier in
training than high frequencies when $s=-1$ and $s=0$ (see Figure 3, left and
middle), and that this frequency biasing phenomena can be counterbalanced by
taking $s=2.5$ (see Figure 3, right).

###  F.3 Test on Autoencoder

Autoencoders can be used as a generative models to randomly generate new data
that is similar to the training data. In this experiment, we use Sobolev-based
norms to improve NN training for producing new images of digits that match the
MNIST dataset. In our final experiment, we use the same autoencoder
architecture as in Chollet [2016], except we train the autoencoder with a
different loss function (see section 6.3).

Here, for training images $\\{\mathbf{x}_{i}\\}$, a standard loss function can
be

$\Phi(\mathbf{W})=\frac{1}{2}\int\text{dist}(\mathcal{N}(\mathbf{x}),\mathbf{x})d\mu(\mathbf{x})\approx\frac{1}{2n}\sum_{i=1}^{n}\text{dist}(\mathcal{N}(\mathbf{x}_{i}),\mathbf{x}_{i}),$

where $\mu$ is the distribution of the training images and
$\text{dist}(\mathcal{N}(\mathbf{x}_{i}),\mathbf{x}_{i})$ is a distance
between the output of the NN given by $\mathcal{N}(\mathbf{x})$ and the image
$\mathbf{x}$. We select the distance metric to measure the difference between
$\mathcal{N}(\mathbf{x})$ and $\mathbf{x}$ as

$\Phi(\mathbf{W})=\frac{1}{2n}\sum_{i=1}^{n}\|\mathcal{N}(\mathbf{x}_{i})-\mathbf{x}_{i}\|_{F}^{2},$
(63)

where $\|\cdot\|_{F}$ denotes the matrix Frobenius norm. The distance metric
in eq. 63 can be viewed as a discretization of the continuous $L^{2}$ norm.
That is, if one imagines generating a continuous function
$x:[0,1]^{2}\rightarrow[0,\infty)$ that interpolates an image as well as a
function that interpolates the NN, then

$\frac{1}{N_{\text{pixel}}}\|\mathcal{N}(\mathbf{x})-\mathbf{x}\|_{F}^{2}\approx\iint|\mathcal{N}(x)(y_{1},y_{2})-x(y_{1},y_{2})|^{2}dy_{1}dy_{2}=\|\mathcal{N}(x)-x\|_{L^{2}}^{2},$

where $N_{\text{pixel}}$ is the total number of pixels of the image
$\mathbf{x}$. In this continuous viewpoint, the $H^{s}$ norm is given by
(assuming that the continuous interpolating functions $x$ and $\mathcal{N}(x)$
are constructed with periodic boundary conditions)

$\|\mathcal{N}(x)-x\|^{2}_{H^{s}}=\int(1+|\xi|^{2})^{s}|\widehat{\mathcal{N}(x)}(\xi)-\widehat{x}(\xi)|^{2}d\xi\approx\|\mathbf{S}_{s}\circ\left(\mathbf{F}_{l}\left(\mathcal{N}(\mathbf{x})-\mathbf{x}\right)\mathbf{F}_{r}^{\top}\right)\|_{F}^{2},$
(64)

where $\mathbf{F}_{l},\mathbf{F}_{r}$ are the left and right 2D-DFT matrices,
respectively, $(S_{s})_{j\ell}=(1+j^{2}+\ell^{2})^{s/2}$, and ‘$\circ$’ is the
Hadamard product. Hence, if we define $\text{vec}(\mathbf{A})$ to be the
vector obtained by reshaping a matrix $\mathbf{A}$ using the column major
order, then we have

$\|\mathbf{S}_{s}\circ\left(\mathbf{F}_{l}\left(\mathcal{N}(\mathbf{x})-\mathbf{x}\right)\mathbf{F}_{r}^{\top}\right)\|_{F}^{2}=\left\lVert\text{diag}(\text{vec}(\mathbf{S}_{s}))(\mathbf{F}_{r}\otimes\mathbf{F}_{l})\text{vec}(\mathcal{N}(\mathbf{x})-\mathbf{x})\right\rVert^{2}_{2},$

where $\otimes$ is the Kronecker product of two matrices. Setting
$\mathbf{J}_{s}=\text{diag}(\text{vec}(\mathbf{S}_{s}))(\mathbf{F}_{r}\otimes\mathbf{F}_{l})$,
the loss function in our NN training can be written as

$\Phi_{s}(\mathbf{W})=\frac{1}{2n}\sum_{i=1}^{n}\|\mathbf{J}_{s}\text{vec}\left(\mathcal{N}(\mathbf{x}_{i})-\mathbf{x}_{i}\right)\|_{2}^{2}=\frac{1}{2n}(\mathbf{u}-\mathbf{y})^{\top}(\mathbf{I}\otimes\mathbf{J}_{s}^{\top}\mathbf{J}_{s})(\mathbf{u}-\mathbf{y}),$
(65)

where $\mathbf{I}$ is the $n$-by-$n$ identity matrix and
$\mathbf{u},\mathbf{y}$ are the vectors of length $n\times N_{\text{pixel}}$
given by
$\mathbf{u}=(\text{vec}(\mathcal{N}(\mathbf{x}_{1}))^{\top},\ldots,\text{vec}(\mathcal{N}(\mathbf{x}_{n}))^{\top})^{\top}$
and
$\mathbf{y}=(\text{vec}(\mathbf{x}_{1})^{\top},\ldots,\text{vec}(\mathbf{x}_{n})^{\top})^{\top}$.
Hence, the discrete NTK matrix is given by
$n^{-1}\mathbf{H}^{\infty}(\mathbf{I}\otimes\mathbf{J}_{s}^{\top}\mathbf{J}_{s})$,
where the $(i,j)$th sub-block is
$\mathbf{H}^{\infty}_{ij}=\big{\langle}\frac{\partial\text{vec}(\mathcal{N}(\mathbf{x}_{i};\mathbf{W}))}{\partial\mathbf{W}},\frac{\partial\text{vec}(\mathcal{N}(\mathbf{x}_{j};\mathbf{W}))}{\partial\mathbf{W}}\big{\rangle}$
for $i,j=1,\ldots,n$. Here,
$\big{\langle}\frac{\partial\text{vec}(\mathcal{N}(\mathbf{x}_{i};\mathbf{W}))}{\partial\mathbf{W}},\frac{\partial\text{vec}(\mathcal{N}(\mathbf{x}_{j};\mathbf{W}))}{\partial\mathbf{W}}\big{\rangle}$
is interpreted as the $N_{\text{pixel}}$-by-$N_{\text{pixel}}$ matrix whose
$(i^{\prime},j^{\prime})$th entry is
$\big{\langle}\frac{\partial[\text{vec}(\mathcal{N}(\mathbf{x}_{i};\mathbf{W}))_{i^{\prime}}]}{\partial\mathbf{W}},\frac{\partial[\text{vec}(\mathcal{N}(\mathbf{x}_{j};\mathbf{W}))_{j^{\prime}}]}{\partial\mathbf{W}}\big{\rangle}$.
This means that the frequency biasing behavior during NN training is directly
affected by the choice of $s$. We remark that while eq. 65 is a mathematically
equivalent expression for the loss function that allows us to easily express
the NTK, in practice, we implement the loss function based on eq. 64 using a
2D FFT protocol.

We use the same autoencoder architecture as in Chollet [2016], except with the
loss function in eq. 65 for $s=-1,0,1$. We first pollute the training images
with low-frequency noise and train the NN, hoping that the trained NN will act
as filter for the noise. We see that training the NN with eq. 65 for $s=1$
gives us the best results due to the high-frequency biasing induced by the
choice of the loss function. Although $\mathbf{H}^{\infty}$ is low frequency
biasing, the high-frequency biasing of $\mathbf{J}_{s}^{\top}\mathbf{J}_{s}$
dominates for sufficiently large $s$. In that case, the low-frequency noise
barely changes the training in the earlier epochs as the low-frequency
components of the residual correspond to small eigenvalues of
$\mathbf{H}^{\infty}(\mathbf{I}\otimes\mathbf{J}_{s}^{\top}\mathbf{J}_{s})$.
Similar results are discussed in Engquist et al. [2020] and Zhu et al. [2021]
in the inverse problem and image processing contexts, respectively.

The opposite phenomenon occurs when we add high-frequency noise (see Figure 4,
bottom row). Since $\mathbf{H}^{\infty}$ by itself makes the NN training
procedure bias towards low-frequencies, the output for $s=0$ does already
filter high-frequency noise. Since $\mathbf{J}_{s}^{\top}\mathbf{J}_{s}$ for
$s<0$ further biases towards low-frequencies, one can obtain better high-
frequency filters. We observe that the best denoising results for the
autoencoder comes from selecting $s=-1$ (see Figure 4, bottom row).