#  An Abstract View on Optimizations in Propositional Frameworks

YULIYA LIERLER

###### Abstract

Search-optimization problems are plentiful in scientific and engineering
domains. Artificial intelligence has long contributed to the development of
search algorithms and declarative programming languages geared toward solving
and modeling search-optimization problems. Automated reasoning and knowledge
representation are the subfields of AI that are particularly vested in these
developments. Many popular automated reasoning paradigms provide users with
languages supporting optimization statements: answer set programming or MaxSAT
on min-one, to name a few. These paradigms vary significantly in their
languages and in the ways they express quality conditions on computed
solutions. Here we propose a unifying framework of so-called weight systems
that eliminates syntactic distinctions between paradigms and allows us to see
essential similarities and differences between optimization statements
provided by paradigms. This unifying outlook has significant simplifying and
explanatory potential in the studies of optimization and modularity in
automated reasoning and knowledge representation. It also supplies researchers
with a convenient tool for proving the formal properties of distinct
frameworks; bridging these frameworks; and facilitating the development of
translational solvers.

##  1 Introduction

Artificial intelligence is a powerhouse for delivering algorithmic frameworks
to support solutions to search-optimization problems that are plentiful in
scientific and engineering domains. Automated reasoning and knowledge
representation are the subfields of AI that are particularly vested in
developing general-purpose search algorithms and declarative programming
languages specifically geared towards formulating constraints of search-
optimization problems. Various automated reasoning paradigms provide users
with languages supporting optimization statements. Indeed, consider such
popular AI paradigms as answer set programming with weak constraints (ASP-WC)
(Alviano,,2018) and propositional satisfiability with optimizations (MaxSAT
family) (Robinson et al.,,2010). In practice, when search problems are
formulated there is often an interest not only in identifying a solution, but
also in pointing at the one that is optimal with respect to some criteria.
Another way to perceive this setting is by having interplay of “hard” and
“soft” modules (drawing a parallel to terminology used in formulating partial
weighted MaxSAT). Hard modules formulate immutable constraints of a problem,
i.e., requirements that solutions to a problem must satisfy in order to
deserve being called a solution. Soft modules express conditions that are
closer to preferences. Consider the well known travelling salesman problem
(TSP) that asks the following: “Given a list of cities and the information on
how the cities are connected by roads with associated lengths, what are the
possible routes that visit each city and return to the origin city? What are
the shortest routes?” Here, the first question of TSP formulates “hard”
requirements. In order for a sequence of cities to form a solution it has to
form a special kind of path. The second question of TSP formulates a
preference. Out of all possible solutions we are interested in these that
satisfy some numeric criterion. In ASP-WC, for example, a traditional logic
program composed of rules is used to express a hard fragment of a given
problem, while weak constraints are used to formulate a soft fragment.

Supporting various kinds of optimizations on an encoding and solving level is
a holy grail of ASP-WC as in practical applications it is common that there
are criteria which can make one solution to be preferred over the other. Yet,
some approaches to answer set solving that rely on translations to related
automated reasoning (AR) paradigms – “translational” solvers such as cmodels
(Giunchiglia et al.,,2006) and lp2sat (Janhunen,,2006), which translate logic
programs into the propositional satisfiability (SAT) problem (Mitchell,,2005)
– do not provide any support for weak constraints. One reason is that SAT
itself has no support for formulating soft requirements. MaxSAT and its
variants are extensions to SAT supporting optimizations. The formulations of
these extensions significantly differ syntactically and semantically from
those used in ASP-WC so that the exact link, between ASP-WC and MaxSAT
formalisms, required in implementing translational approaches is not obvious.
In general, optimizations in different areas of AR (see, for instance,
(Nieuwenhuis and Oliveras,; Li et al.,; Andres et al.,; Di Rosa and
Giunchiglia,; Brewka et al.,; Alviano,,2006; 2011; 2012; 2013; 2015; 2018))
are studied in separation with no clear articulation of the exact links
between the languages expressing optimization criteria and their
implementations. Yet, it is due to note that their relation is often obvious
to researchers developing solving procedures within AR. The algorithmic
techniques have been borrowed from solvers in one paradigm to solvers in the
other, see, for instance, the paper by Alviano et al., (2020) explaining how
algorithmic techniques behind MaxSAT can be utilized in solving problems
formulated in ASP-WC. Here, we focus on uncovering the precise semantic
relation between distinct paradigms geared to support translational
approaches.

This paper takes modularity and abstraction as key tools for building a
thorough understanding between related and, yet, disperse advances pertaining
to optimizations or soft modules within different AR communities. Lierler and
Truszczynski, (2015) proposed an abstract modular framework that allows us to
bypass the syntactic details of a particular logic and study advances in AR
from a bird’s eye view. That framework is appropriate for capturing varieties
of logics within hard modules. We extend the framework in a way that soft
modules can be formulated and studied under one roof. We illustrate how a
family of SAT based optimization formalisms such as MaxSAT, weighted MaxSAT,
and partial weighted MaxSAT (pw-MaxSAT) can be embedded into the proposed
framework. We also illustrate how ASP-WC fits into the same framework. The
predominant focus of this work are so called quantitative
optimizations/preferences. An objective function for assessing quality of
computed models is of central importance in these methods. Weighted-conditions
of introduced weighted systems are vehicles for expressing these objective
functions. Qualitative preferences is an alternative. These maybe expressed by
means of preference relations on the level of atoms (literals - atoms or their
complements) or interpretations. We illustrate how some optimization
frameworks stemming from qualitative preferences within SAT such as min-one
(Creignou et al.,,2001) and distancesat (Bailleux and Marquis,,2006) are
conveniently captured by w-system. This fact allows us an immediate extension
of these ideas to the case of answer set programming.

In addition, we carefully study the introduced abstract framework and
illustrate a number of its formal properties. These properties immediately
translate into formal claims about specific instances of this framework such
as MaxSAT or ASP-WC. The paper culminates in a result illustrating how ASP-WC
programs can be processed by means of MaxSAT/MinSAT solvers. The opposite link
also becomes apparent. To summarize, we propose to utilize abstract view on
logics and modularity as tools for constructing overarching view for distinct
criteria used for optimization within different AR communities. We would like
to point at work by Alviano et al., (2018), where the authors also realized
the importance of abstracting away the syntactic details of the formalisms to
describing hard and soft constraints of a considered problem in order to
streamline the utilization of existing efficient solving techniques in new
settings. Similarly, the work by Ensan and Ternovska, (2019) is devoted to
preferences in declarative programming solving.

Paper outline  We start the paper by reviewing the concepts of an abstract
logic and modular systems. We then introduce a notion of weighted abstract
modular systems – key artifact of this paper. In Section 4, we show how these
weighted systems naturally capture MaxSAT family and answer set programming
with weak constraints. Section 5 is devoted to the case of qualitative
preferences and we illustrate how these weighted systems capture such SAT-
based formalisms as min-one and distancesat, which also lend themselves to
newly defined frameworks of, for instance, min-one for the case of answer set
programming. Section 6 enumerates formal properties of w-systems showcasing
how these properties immediately translate into properties of MaxSAT family
and ASP-WC paradigms. In conclusion of this section we are able to provide a
precise link between pw-MaxSAT/pw-MinSAT and ASP-WC. The concluding section of
the paper lists proofs.

Parts of this paper appeared in the proceedings of the 17th Edition of the
European Conference on Logics in Artificial Intelligence (Lierler,,2021). In
particular, this paper unlike its conference predecessor provides a complete
account of proofs for the stated formal results. It also extends the use of
weighted systems to the case of qualitative preferences utilized in such
formalisms as min-one and distancesat.

##  2 Review: Abstract Logics and Modular Systems

We start with the review of an abstract logic by Brewka and Eiter, (2007). We
illustrate how this abstract concept captures SAT and logic programs under
answer set semantics. We then review model-based abstract modular systems
advocated by Lierler and Truszczynski, (2015).

A _language_ is a set $L$ of _formulas_. A _theory_ is a subset of $L$. Thus
the set of theories is closed under union and has the least and the greatest
elements: $\emptyset$ and $L$. We call a theory a singleton if it is an
element/a formula in $L$ (or a singleton subset, in other words). This
definition ignores any syntactic details behind the concepts of a formula and
a theory. A _vocabulary_ is possibly an infinite countable set of _atoms_.
Subsets of a vocabulary $\sigma$ represent (classical propositional)
_interpretations_ of $\sigma$. We write $\mathit{Int}(\sigma)$ for the family
of all interpretations of a vocabulary $\sigma$. It is customary for a given
vocabulary $\sigma$, to identify a set $X$ of atoms over $\sigma$ with an
assignment function that assigns the truth value true to every atom in $X$ and
false to every atom in $\sigma\setminus X$. In classical propositional logic,
interpretations are often defined by means of such assignment functions.

###### Definition 1

A _logic_ is a triple
$\mathcal{L}=(L_{\mathcal{L}},\sigma_{\mathcal{L}},\mathit{sem}_{\mathcal{L}})$,
where

  1. 1.

$L_{\mathcal{L}}$ is a language (_language_ of $\mathcal{L}$)

  2. 2.

$\sigma_{\mathcal{L}}$ is a vocabulary (_vocabulary_ of $\mathcal{L}$)

  3. 3.

$\mathit{sem}_{\mathcal{L}}:2^{L_{\mathcal{L}}}\rightarrow
2^{\mathit{Int}(\sigma_{\mathcal{L}})}$ is a function from theories in
$L_{\mathcal{L}}$ to collections of interpretations (_semantics_ of
$\mathcal{L}$)

If a logic $\mathcal{L}$ is clear from the context, we omit the subscript
$\mathcal{L}$ from the notation of the language, the vocabulary and the
semantics of the logic.

Brewka and Eiter, (2007) showed that this abstract notion of a logic captures
default logic, propositional logic, and logic programs under the answer set
semantics. For example, the logic $\mathcal{L}=(L,\sigma,\mathit{sem})$, where

  1. 1.

$L$ is the set of propositional formulas over $\sigma$,

  2. 2.

$\mathit{sem}(F)$, for a theory $F\subseteq L$, is the set of propositional
models of theory $F$ (where we understand an interpretation to be a model of
theory $F$ if it is a model of each element/propositional formula in $F$) over
$\sigma$,

captures propositional logic. (We assume the readers familiarity with the key
concepts of propositional logic: formulas, interpretations, models.) We call
this logic a pl-logic. A clause is a propositional formula of the form

$\neg a_{1}\vee\dotsc\vee\neg a_{\ell}\vee\ a_{\ell+1}\vee\dotsc\vee\ a_{m},$
(1)

where every $a_{i}$ is an atom. If we restrict elements of $L$ to be clauses,
then we call $\mathcal{L}$ a sat-logic. Intuitively, the finite theories in
sat-logic can be identified with CNF formulas. Say, sat-logic theory
$\\{(a\vee b),(\neg a\vee\neg b)\\}$ stands for the formula

$(a\vee b)\wedge(\neg a\vee\neg b).$ (2)

We now review logic programs. A _logic program_ over $\sigma$ is a finite set
of _rules_ of the form

$\begin{array}[]{l}a_{0}\leftarrow a_{1},\dotsc,a_{\ell},\ not\
a_{\ell+1},\dotsc,\ not\ a_{m},\end{array}$ (3)

where $a_{0}$ is an atom in $\sigma$ or $\bot$ (empty), and each $a_{i}$
$(1\leq i\leq m)$ is an atom in $\sigma$. The expression $a_{0}$ is the _head_
of the rule. The expression on the right hand side of the arrow, is the
_body_. When the body is empty we drop $\leftarrow$. Expression $not\
a_{\ell+1},\dotsc,\ not\ a_{m}$ is called negative part of the body.

We say that a set $X$ of atoms satisfies rule (3), if $X$ satisfies the
propositional formula

$a_{1}\wedge\dotsc\wedge a_{\ell}\wedge\ \neg a_{\ell+1}\wedge\dotsc\wedge\
\neg a_{m}\rightarrow a_{0}.\ $

The reduct $\Pi^{X}$ of a program $\Pi$ relative to a set $X$ of atoms is
obtained by first removing all rules (3) such that $X$ does not satisfy the
propositional formula corresponding to the negative part of the body $\neg
a_{\ell+1}\wedge\ldots\wedge\neg a_{m},$ and replacing all remaining rules
with their counterparts without negative part of the body

$a\leftarrow a_{1},\ldots,a_{\ell}.$

For example, let $\Pi_{1}$ denote a program

$\begin{array}[]{l}a\leftarrow not\ b\\\ b\leftarrow not\ a.\end{array}$ (4)

The reduct $\Pi_{1}^{\\{a\\}}$ consists of a single rule

$a.$

A set $X$ of atoms is an answer set, if it is the minimal set that satisfies
all rules of $\Pi^{X}$ (Lifschitz et al.,,1999). For instance, program (4) has
two answer sets $\\{a\\}$ and $\\{b\\}$.

Abstract logics of Brewka and Eiter subsume the formalism of logic programs
under the answer set semantics. Indeed, let us consider a logic
$\mathcal{L}=(L,\sigma,\mathit{sem})$, where

  1. 1.

$L$ is the set of logic program rules over $\sigma$,

  2. 2.

$\mathit{sem}(\Pi)$, for a program $\Pi\subseteq L$, is the set of answer sets
of $\Pi$ over $\sigma$,

We call this logic the lp-logic.

Lierler and Truszczynski, (2015) propose (model-based) abstract modular
systems that allow us to construct heterogeneous systems based of “modules”
stemming from a variety of logics. We now review their framework.

###### Definition 2

Let
$\mathcal{L}=(L_{\mathcal{L}},\sigma_{\mathcal{L}},\mathit{sem}_{\mathcal{L}})$
be a logic. A theory of $\mathcal{L}$, that is, a subset of the language
$L_{\mathcal{L}}$ is called a _(model-based) $\mathcal{L}$-module_ (or a
_module_ , if the explicit reference to its logic is not necessary). An
interpretation $I\in\mathit{Int}(\sigma_{\mathcal{L}})$ is a _model_ of an
$\mathcal{L}$-module/theory $T$ if $I\in\mathit{sem}_{\mathcal{L}}(T)$.

We use words theory and modules interchangeably at times. Furthermore, for a
theory/module in pl- or sat-logics we often refer to those as propositional or
SAT formulas (sets of clauses). For a theory/module in lp-logic we refer to it
as a logic program.

For an interpretation $I$, by $I_{|\sigma}$ we denote an interpretation over
vocabulary $\sigma$ constructed from $I$ by dropping all its members not in
$\sigma$. For example, let $\sigma_{1}$ be a vocabulary such that
$a\in\sigma_{1}$ and $b\not\in\sigma_{1}$, then
$\\{a,b\\}_{|\sigma_{1}}=\\{a\\}$. We now extend the notion of a model to
vocabularies that go beyond the one of a considered module in a
straightforward manner. For an $\mathcal{L}$-module $T$ and an interpretation
$I$ whose vocabulary is a superset of the vocabulary $\sigma_{\mathcal{L}}$ of
$T$, we say that $I$ is a model of $T$, denoted $I\models T$, if
$I_{|\sigma_{\mathcal{L}}}\in\mathit{sem}_{\mathcal{L}}(T)$. This extension is
in spirit of a convention used in classical logic (for example, given a
propositional formula $p\wedge q$ over vocabulary $\\{p,q\\}$ we can speak of
interpretation assigning true to propositional variables $\\{p,q,r\\}$ as a
model to this formula).

###### Definition 3

A set of modules, possibly in different logics and over different vocabularies
is a _(model-based) abstract modular system (AMS)_. For an abstract modular
system $\mathcal{H}$, the union of the vocabularies of the logics of the
modules in $\mathcal{H}$ forms the _vocabulary_ of $\mathcal{H}$, denoted by
$\sigma_{\mathcal{H}}$. An interpretation
$I\in\mathit{Int}(\sigma_{\mathcal{H}})$ is a _model_ of $\mathcal{H}$ when
for every module $T\in\mathcal{H}$, $I$ is a model of $T$. (It is easy to see
that we can extend the notion of a model to interpretations whose vocabulary
goes beyond $\sigma_{\mathcal{H}}$ in a straightforward manner.)

When an AMS consists of a single module $\\{F\\}$ we identify it with module
$F$ itself.

##  3 Weighted Abstract Modular Systems

In practice, we are frequently interested not only in identifying models of a
given logical formulation of a problem (hard fragment) but identifying models
that are deemed optimal according to some criteria (soft fragment).
Frequently, multi-level optimizations are of interest. An AMS framework is
geared towards capturing heterogeneous solutions for formulating hard
constraints. Here we extend it to enable the formulation of soft constraints.
We start by introducing a “w-condition” – a module accommodating notions of a
level and a weight. We then introduce w-systems – a generalization of AMS that
accommodates new kinds of modules. In conclusion, we embed multiple popular
automated reasoning optimization formalisms into this framework.

###### Definition 4

Let
$\mathcal{L}=(L_{\mathcal{L}},\sigma_{\mathcal{L}},\mathit{sem}_{\mathcal{L}})$
be a logic. A pair $(T_{\mathcal{L}},w@l)$ – consisting of a theory
$T_{\mathcal{L}}$ of logic $\mathcal{L}$ (or $\mathcal{L}$-module) and an
expression $w@l$, where $w$ is an integer and $l$ is a positive integer – is
called an _ $\mathcal{L}$-w(eighted)-condition_ (or a _w-condition_ , if the
explicit reference to its logic is not necessary). We refer to integers $l$
and $w$ as levels and weights, respectively. An interpretation
$I\in\mathit{Int}(\sigma_{\mathcal{L}})$ is a _model_ of an
$\mathcal{L}$-w-condition $B=(T_{\mathcal{L}},w@l)$, denoted $I\models B$ if
$I\in\mathit{sem}_{\mathcal{L}}(T_{\mathcal{L}})$. A mapping $[{I\models B}]$
is defined as follows

$[{I\models B}]=\begin{cases}w&\hbox{when $I\models B$, }\\\
0&\hbox{otherwise.}\end{cases}$ (5)

By ${\lambda({B})}$ and ${B}_{w}$ we denote level $l$ and weight $w$
associated with w-condition $B$, respectively.

We identify w-conditions of the form $(T,w@1)$ with expressions $(T,w)$ (i.e.,
when the level is missing it is considered to be one).

For a collection $\mathcal{Z}$ of w-conditions, the union of the vocabularies
of the logics of the w-conditions in $\mathcal{Z}$ forms the _vocabulary_ of
$\mathcal{Z}$, denoted by $\sigma_{\mathcal{Z}}$.

###### Definition 5

A pair $(\mathcal{H},\mathcal{Z})$ consisting of an AMS $\mathcal{H}$ and a
set $\mathcal{Z}$ of w-conditions (possibly in different logics and over
different vocabularies) so that
$\sigma_{\mathcal{Z}}\subseteq\sigma_{\mathcal{H}}$ is called a
_w(eighted)-abstract modular system_ (or w-system).

Let $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ be a w-system ($\mathcal{H}$ and
$\mathcal{Z}$ intuitively stand for hard and soft). The vocabulary of
$\mathcal{H}$ forms the _vocabulary_ of $\mathcal{W}$, denoted by
$\sigma_{\mathcal{W}}$. We now state the definition of a model of a system
that is solely based on the semantics of the hard part.

###### Definition 6

Let pair $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ be a w-system. An
interpretation $I\in\mathit{Int}(\sigma_{\mathcal{W}})$ is a _model_ of
$\mathcal{W}$ if it is a model of AMS $\mathcal{H}$.

For the special case when all w-conditions of a considered w-system have the
form $(T,w)$, we provide a simple definition of an optimal/min-optimal model
that takes soft part of w-system into account so that models are distinguished
based on their “w-conditions quality”. This definition is inspired by the way
the solutions to partially weighted MaxSAT problems are stated (see Section
4.1).

###### Definition 7

Let pair $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ be a w-system, where
$\mathcal{Z}$ has the form $\\{(T_{1},w_{1}),\dots,(T_{n},w_{n})\\}$. A model
$I^{*}$ of $\mathcal{W}$ is optimal if $I^{*}$ satisfies equation

$I^{*}=\displaystyle{\operatorname*{arg\,max}_{I}{\sum_{B\in\mathcal{Z}}{[{I\models
B}]}}},$

where $I$ ranges over models of $\mathcal{W}$. A model $I^{*}$ of
$\mathcal{W}$ is min-optimal if it satisfies the conditions of optimal model,
where in the equation above we replace $max$ by $min$.

Let $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ be w-system. For a level $l$, by
$\mathcal{W}_{l}$ we denote the subset of $\mathcal{Z}$ that includes all
w-conditions whose level is $l$. By ${\lambda({\mathcal{W}})}$ we denote the
set of all levels associated with w-system $\mathcal{W}$ constructed as
$\\{{\lambda({B})}\mid B\in\mathcal{Z}\\}$.

We now provide the definition of an optimal model for the general form of
w-systems. It is inspired by a definition of an optimal answer set coming from
the ASP-WC framework, where multi-level optimizations are standard (see
Section 4.2).

###### Definition 8

Let $I$ and $I^{\prime}$ be models of w-system
$\mathcal{W}=(\mathcal{H},\mathcal{Z})$. Model $I^{\prime}$ min-dominates $I$
if there exists a level $l\in{\lambda({\mathcal{W}})}$ such that following
conditions are satisfied:

  1. 1.

for any level $l^{\prime}>l$ the following equality holds

$\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I\models
B}]}}=\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I^{\prime}\models
B}]}}$

  2. 2.

the following inequality holds for level $l$

$\displaystyle{\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}}<\displaystyle{\sum_{B\in\mathcal{W}_{l}}{[{I\models B}]}}$

Model $I^{\prime}$ max-dominates $I$ if we change less-than symbol by greater-
than symbol in the inequality of Condition 2.

A model $I^{*}$ of $\mathcal{W}$ is optimal if there is no model $I^{\prime}$
of $\mathcal{W}$ that max-dominates $I^{*}$. A model $I^{*}$ of $\mathcal{W}$
is min-optimal if there is no model $I^{\prime}$ of $\mathcal{W}$ that min-
dominates $I^{*}$.

We now attempt to reconcile terminology used in Definitions 7 and 8. We state
an alternative definition to optimal and min-optimal models of Definition 8
and then provide a formal result on their equivalence. Let
$\mathcal{W}=(\mathcal{H},\mathcal{Z})$ be w-system. For a level
$l\in{\lambda({\mathcal{W}})}$ by ${l}^{\uparrow}$ we denote the least level
in ${\lambda({\mathcal{W}})}$ that is greater than $l$ (it is obvious that for
the greatest level in ${\lambda({\mathcal{W}})}$, ${l}^{\uparrow}$ is
undefined). For example, for levels in $\\{2,6,8,9\\}$, ${2}^{\uparrow}=6$,
${6}^{\uparrow}=8$, and ${8}^{\uparrow}=9$.

###### Definition 9

Let pair $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ be a w-system. For level
$l\in{\lambda({\mathcal{W}})}$, a model $I^{*}$ of $\mathcal{W}$ is
$l$-optimal if $I^{*}$ satisfies equation

$I^{*}=\displaystyle{\operatorname*{arg\,max}_{I}{\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}}},$ (6)

where

  * •

$I$ ranges over models of $\mathcal{W}$ if $l$ is the greatest level in
${\lambda({\mathcal{W}})}$,

  * •

$I$ ranges over ${l}^{\uparrow}$-optimal models of $\mathcal{W}$, otherwise.

We call a model $l$-min-optimal if $max$ is replaced by $min$ in (6).

A model $I^{*}$ of $\mathcal{W}$ is optimal if $I^{*}$ is $l$-optimal model
for every level $l\in{\lambda({\mathcal{W}})}$. A model $I^{*}$ of
$\mathcal{W}$ is min-optimal if $I^{*}$ is $l$-min-optimal model for every
level $l\in{\lambda({\mathcal{W}})}$.

###### Proposition 1

Definitions 8 and 9 are equivalent.

The proofs of the formal results of this paper are presented in its final
section. The proof of the claim of Proposition 1 relies on the following
lemmas that we list here as they refer to interesting properties of
$l$-optimal models.

###### Lemma 1

For a w-system $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ and levels
$l,l^{\prime}\in{\lambda({\mathcal{W}})}$ so that $l<l^{\prime}$, any
$l$-optimal/$l$-min-optimal model of $\mathcal{W}$ is also an
$l^{\prime}$-optimal/$l^{\prime}$-min-optimal model of $\mathcal{W}$ as well
as model of $\mathcal{W}$. For the least level $l$ in
${\lambda({\mathcal{W}})}$, $l$-optimal/$l$-min-optimal model of $\mathcal{W}$
is an optimal/min-optimal model of $\mathcal{W}$.

###### Lemma 2

For a w-system $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ and levels
$l,l^{\prime}\in{\lambda({\mathcal{W}})}$ so that $l\leq l^{\prime}$, and any
$l$-optimal/$l$-min-optimal models $I$ and $I^{\prime}$ of $\mathcal{W}$,

$\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I\models
B}]}=\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I^{\prime}\models B}]}.$

Section 6 presents many interesting formal properties of w-systems. Yet,
before proceeding towards that presentation in the following section we
illustrate several AI formalisms that can be viewed as instances of w-systems.
With that our later discussion of formal properties of w-systems immediately
applies to these AI formalisms.

##  4 Instances of W-Systems

###  4.1 MaxSAT/MinSAT Family as W-systems

We now restate the definitions of MaxSAT, weighted MaxSAT and pw-MaxSAT
(Robinson et al.,,2010). We then show how these formalisms are captured in
terms of w-systems. In the sections that follow we use w-systems to model
logic programs with weak constraints. The uniform language of w-systems allows
us to prove properties of theories in these different logics by eliminating
the reference to their syntactic form. Later in the paper we provide
translation from logic programs with weak constraints to pw-MaxSAT problems.

To begin we introduce a notion of so called $\sigma$-theory. For a vocabulary
$\sigma$ and a logic $\mathcal{L}$ over this vocabulary
($\sigma_{\mathcal{L}}=\sigma$), we call theory $T_{\mathcal{L}}$ a
$\sigma$-theory/$\sigma$-module when it satisfies property
$sem(T_{\mathcal{L}})=Int(\sigma)$. For example, in case of pl-logic or sat-
logic a conjunction of clauses of the form $a\vee\neg a$ for every atom
$a\in\sigma$ forms a $\sigma$-theory. For a $\sigma$-theory a logic of the
theory becomes immaterial so we allow ourselves to denote an arbitrary
$\sigma$-theory by $T_{\sigma}$ disregarding the reference to its logic.

As customary in propositional logic given an interpretation $I$ and a
propositional formula $F$, we write $I\models F$ when $I$ satisfies $F$ (i.e.,
$I$ is a model of $F$). A mapping $[{I\models F}]$ is defined as

$[{I\models F}]=\begin{cases}1&\hbox{when $I\models F$, }\\\
0&\hbox{otherwise.}\end{cases}$ (7)

###### Definition 10

An interpretation $I^{*}$ over vocabulary $\sigma$ is a solution to MaxSAT
problem $F$, where $F$ is a CNF formula over $\sigma$, when it satisfies the
equation

$I^{*}=arg\max_{I}{\sum_{C\in F}{[{I\models C}]}},$

where $I$ ranges over all interpretations over $\sigma$.

The following result illustrates how w-systems can be used to capture MaxSAT
problem.

###### Proposition 2

Let $F$ be a MaxSAT problem over $\sigma$. The optimal models of w-system
$(T_{\sigma},\\{(C,{1})\mid C\in F\\})$ – where pairs of the form $(C,{1})$
are sat-logic w-conditions – form the set of solutions for $F$.

Proposition 2 allows us to identify w-systems of particular form with MaxSAT
problems. For example, any w-system of the form
$\big{(}T_{\sigma},\\{(C_{1},1),\dots(C_{n},1)\\}\big{)}$ – where $C_{i}$
$(1\leq i\leq n)$ is a singleton sat-logic theory – can be seen as a MaxSAT
problem composed of clauses $\\{C_{1},\dots,C_{n}\\}$.

###### Definition 11

A weighted MaxSAT problem (Argelich et al.,,2008)/weighted MinSAT problem (Li
et al.,,2011) is defined as a set $(C,w)$ of pairs, where $C$ is a clause and
$w$ is a positive integer. An interpretation $I^{*}$ over vocabulary $\sigma$
is a solution to weighted MaxSAT problem $P$ over $\sigma$, when it satisfies
the equation

$I^{*}=arg\max_{I}{\sum_{(C,w)\in P}{w\cdot[{I\models C}]}},$ (8)

where $I$ ranges over all interpretations over $\sigma$. An interpretation
$I^{*}$ over vocabulary $\sigma$ is a solution to weighted MinSAT problem $P$
over $\sigma$, when it satisfies the equation (8), where we replace $max$ with
$min$.

The following proposition allows us to identify w-systems of particular form
with weighted MaxSAT/MinSAT problems.

###### Proposition 3

Let $P$ be a weighted MaxSAT problem over $\sigma$. The optimal models of
w-system $(T_{\sigma},P)$ – where each element in $P$ is understood as a sat-
logic w-condition – form the set of solutions for $P$.

Let $P$ be a weighted MinSAT problem over $\sigma$. The min-optimal models of
w-system $(T_{\sigma},P)$ – where each element in $P$ is understood as a sat-
logic w-condition – form the set of solutions for $P$.

###### Definition 12

A partially-weighted MaxSAT problem or pw-MaxSAT problem (Fu and Malik,,2006)
(pw-MinSAT problem (Li et al.,,2011)) is defined as a pair $(F,P)$ over
vocabulary $\sigma$, where $F$ is a CNF formula over $\sigma$ and $P$ is a
weighted MaxSAT problem (a weighted MinSAT problem) over $\sigma$. Formula $F$
is referred to as hard problem fragment, whereas clauses in $P$ form soft
problem fragment. An interpretation $I$ over $\sigma$ is a model of pw-MaxSAT
problem/pw-MinSAT problem $(F,P)$, when $I$ is a model of $F$.

Let $(F,P)$ be a pw-MaxSAT problem over vocabulary $\sigma$. A model $I^{*}$
of $(F,P)$ is optimal when it satisfies equation (8), where $I$ ranges over
models of $F$.

Let $(F,P)$ be a pw-MinSAT problem over vocabulary $\sigma$. A model $I^{*}$
of $(F,P)$ is optimal when it satisfies equation (8), where $I$ ranges over
models of $F$ and $max$ is replaced by $min$.

The following proposition allows us to identify w-systems of particular form
with pw-MaxSAT/pw-MinSAT problems.

###### Proposition 4

Let $(F,P)$ be a pw-MaxSAT problem over vocabulary $\sigma$. The models and
optimal models of w-system $(F,P)$ – where $F$ is a sat-logic module and each
element in $P$ is understood as a sat-logic w-condition – coincide with the
models and optimal models of pw-MaxSAT problem $(F,P)$, respectively.

Let $(F,P)$ be a pw-MinSAT problem over vocabulary $\sigma$. The models and
min-optimal models of w-system $(F,P)$ – where $F$ is a sat-logic module and
each element in $P$ is understood as a sat-logic w-condition – coincide with
the models and optimal models of pw-MinSAT problem $(F,P)$, respectively.

We now present sample pw-MaxSAT problem to illustrate some definitions at
work. Take $F_{1}$ to denote sat-theory module (2). Consider a pw-MaxSAT
problem

$(F_{1},\\{(a,1),(b,1),(a\vee\neg b,2),(\neg a\vee b,0)\\}).$ (9)

The models of this problem are $\\{a\\}$ and $\\{b\\}$; and its optimal model
is $\\{a\\}$. If we consider this pair as pw-MinSAT problem then $\\{b\\}$ is
an optimal model of this problem. Consider a pw-MinSAT problem

$(F_{1},\\{(\neg a\vee b,2)\\}).$ (10)

The models of this problem are $\\{a\\}$ and $\\{b\\}$; and its optimal model
is $\\{a\\}$.

Embedding family of MaxSAT/MinSAT problems into w-systems realm provides us
with immediate means to generalize their definitions to accommodate

  * •

negative weights;

  * •

distinct levels accompanying weight requirement on its clauses;

  * •

removing restriction from its basic syntactic object being a clause and
allowing, for example, arbitrary propositional formulas, as a logic for its
module and w-conditions.

Consider the following definition of MinMaxPL Problem, meant to be a
counterpart of pw-MaxSAT/pw-MinSAT defined for arbitrary propositional
formulas and incorporating enumerated items. We call a w-system $(F,S)$ a
MinMaxPL problem, when $F$ is a pl-logic module and each w-condition in $S$ is
in pl-logic. It is easy to see that any pw-MaxSAT problem is a special case
instance of MinMaxPL problem, whose optimal models coincide. Any pw-MinSAT
problem is a special case instance of MinMaxPL problem, where optimal models
of pw-MinSAT and min-optimal models of respective MinMaxPL problem coincide.

The pair

$(F_{1},\\{(a,1),(b,1@3),(a\vee\neg b,2),(\neg a\vee b,0)\\})$ (11)

forms a sample MinMaxPL problem that differs from (9) in boosting the level of
one of its w-conditions. The optimal model of this system is $\\{b\\}$. In the
sequel we illustrate that presence of levels and negative weights in w-systems
can often be considered as syntactic sugar. Also, the concept of min-optimal
model can be expressed in terms of optimal models of a closely related
w-system. Yet, from the perspective of knowledge representation, convenience
of modeling, algorithm design for search procedures such features are
certainly of interest and deserve an attention and thorough understanding.

###  4.2 Optimizations in Logic Programming or Answer Set Programming with
Weak Constraints

We now review a definition of a logic program with weak constraints following
the lines of (Calimeri et al.,,2020). A weak constraint has the form

$:\sim a_{1},\dotsc,a_{\ell},\ not\ a_{\ell+1},\dotsc,\ not\ a_{m}[w@l],$ (12)

where $m>0$ and $a_{1},\ldots,a_{m}$ are atoms, $w$ (weight) is an integer,
and $l$ (level) is a positive integer. In the sequel, we abbreviate expression

$:\sim a_{1},\dotsc,a_{\ell},\ not\ a_{\ell+1},\dotsc,\ not\ a_{m}$ (13)

occurring in (12) as $D$ and identify it with the propositional formula

$a_{1}\wedge\dotsc\wedge a_{\ell}\wedge\ \neg a_{\ell+1}\wedge\dotsc\wedge\
\neg a_{m}.$ (14)

An optimization program (or o-program) over vocabulary $\sigma$ is a pair
$(\Pi,W)$, where $\Pi$ is a logic program over $\sigma$ and $W$ is a finite
set of weak constraints over $\sigma$.

Let $\mathcal{P}=(\Pi,W)$ be an optimization program over vocabulary $\sigma$
(intuitively, $\Pi$ and $W$ form hard and soft fragments, respectively). By
${\lambda({\mathcal{P}})}$ we denote the set of all levels associated with
optimization program $\mathcal{P}$ constructed as $\\{l\mid\,D[w@l]\in W\\}$.

###### Definition 13

Let $\mathcal{P}=(\Pi,W)$ be an optimization program over $\sigma$. Set $X$ of
atoms over $\sigma$ is an answer set of $\mathcal{P}$, when it is an answer
set of $\Pi$.

Let $X$ and $X^{\prime}$ be answer sets of $\mathcal{P}$. Answer set
$X^{\prime}$ dominates $X$ if there exists a level
$l\in{\lambda({\mathcal{P}})}$ such that following conditions are satisfied:

  1. 1.

for any level $l^{\prime}$ that is greater than $l$ the following equality
holds

$\displaystyle{\sum_{D[w@l^{\prime}]\in W}{w\cdot[{X\models
D}]}}=\displaystyle{\sum_{D[w@l^{\prime}]\in W}{w\cdot[{X^{\prime}\models
D}]}}$

  2. 2.

the following inequality holds for level $l$

$\displaystyle{\sum_{D[w@l]\in W}{w\cdot[{X^{\prime}\models
D}]}}<\displaystyle{\sum_{D[w@l]\in W}{w\cdot[{X\models D}]}}$

An answer set $X^{*}$ of $\mathcal{P}$ is optimal if there is no answer set
$X^{\prime}$ of $\mathcal{P}$ that dominates $X^{*}$.

Consider a logic whose language is a strict subset of that of propositional
logic: a language that allows only for formulas of the form (14), whereas its
semantics is that of propositional logic. We call this logic a wc-logic.

###### Proposition 5

Let $(\Pi,W)$ be an optimization logic program over vocabulary $\sigma$. The
models and min-optimal models of w-system $\big{(}\Pi,\\{(D,{w@l})\mid
D[w@l]\in W\\}\big{)}$ – where $\Pi$ is an lp-logic module and pairs of the
form $(D,{w@l})$ are wc-logic w-conditions – coincide with the answer sets and
optimal answer sets of $(tit\Pi,W)$, respectively.

Propositions 2, 3, 4, and 5 allow us to identify MaxSAT, weighted MaxSAT, pw-
MaxSAT, and o-programs with respective w-systems. In the following, we often
use the terminology stemming from w-systems, when we talk of these distinct
frameworks. For instance, we allow ourselves to identify a weak constraint
(12) with a wc-logic w-condition

$(a_{1}\wedge\dotsc\wedge a_{\ell}\wedge\ \neg a_{\ell+1}\wedge\dotsc\wedge\
\neg a_{m},w@l).$ (15)

We now exemplify the definition of an optimization program. Let $\Pi_{1}$ be
logic program (4). An optimal answer set of optimization program

$(\Pi_{1},\\{:\sim a,not\ b.[-2@1]\\})$ (16)

is $\\{a\\}$. We note that the answer sets and the optimal answer set of (16)
coincide with the models and the optimal model of pw-MinSAT problem (10). The
formal results of this paper will show that this is not by chance.

It is worth noting that an alternative syntax is frequently used by answer set
programming practitioners when they express optimization criteria:

$\\#minimize\\{w_{1}@l_{1}:lit_{1},\dots,w_{n}@l_{n}:lit_{n}\\},$

where $lit_{i}$ is either an atom $a_{i}$ or an expression $not\ a_{i}$. This
statement stands for $n$ weak constraints

$\begin{array}[]{l}:\sim<EMAIL_ADDRESS>~{}~{}\cdots{}{}\\\ :\sim
<EMAIL_ADDRESS>
Similarly, statement

$\\#maximize\\{w_{1}@l_{1}:lit_{1},\dots,w_{n}@l_{n}:lit_{n}\\},$

stands for $n$ weak constraints

$\begin{array}[]{l}:\sim<EMAIL_ADDRESS>~{}\cdots{}{}\\\ :\sim
<EMAIL_ADDRESS>
##  5 Qualitative Optimizations with W-systems

So far we paid attention to what is often called quantitative optimizations
or, another way to call these, quantitative preferences. An objective function
for assessing quality of computed models is of central importance in these
methods. Weighted-conditions of w-systems are vehicles for expressing
objective functions. The MaxSAT/MinSAT family considered earlier exemplifies
formalisms implementing quantitative preferences.

Qualitative preferences is an alternative. These may be expressed by means of
preference relations on the level of atoms (literals - atoms or their
complements) or interpretations. Alviano et al., (2018) developed an abstract
framework that elegantly captures qualitative, quantitative, and mixed
preferences. They introduce a concept of a knowledge base which parallels the
concept of a theory/module of this work and is characterized by a set of
interpretations. A knowledge base is accompanied by a preference relation over
a vocabulary $\sigma$ of a considered knowledge base which is a partial order
over $2^{\sigma}$. Alviano et al., (2018) illustrate how such an abstraction
is useful in stating, studying, and implementing various algorithms for
computing preferred models. The focus of their work is algorithmic. Here we
focus on a framework that has a “definitional” and “lining” power. We view
w-systems as a convenient tool to capture formalisms defined in different
terms and then link these. Thus, w-systems are a viable alternative to the
Alviano et al., (2018) abstraction.

In this section, we use w-systems to capture several formalisms studied in the
literature that focus on qualitative preferences. In the studied cases, the
language of w-systems focused on quantitative preference is yet convenient to
express what is considered qualitative preferences. In particular, we follow
the steps by Giunchiglia and Maratea, (2006), who review min-one (Creignou et
al.,,2001) and distancesat (Bailleux and Marquis,,2006) problems and define
their variants min-one⊆ and distancesat⊆. Recall the standard Davis-Logemann-
Loveland (dll) procedure (Davis et al.,,1962) – a decision procedure for
establishing the fact whether a given CNF formula is satisfiable. This
procedure can be easily adapted to find a model of a satisfiable formula.
Giunchiglia and Maratea, (2006) introduce a procedure opt-dll that modifies
dll by enforcing an order in which it explores interpretations. Then, opt-dll
is shown to be an appropriate tool for finding a model to such qualitative
optimizations formalisms as min-one, distancesat and their variants min-one⊆
and distancesat⊆.

Here, we illustrate that w-systems naturally lend themselves into capturing
min-one and distancesat problems. We then illustrate how the ideas behind opt-
dll translate into ways of utilizing w-systems for characterizing min-one⊆ and
distancesat⊆ problems. With that we introduce one more bridge between
qualitative and quantitative preferences, where the later are used to capture
the former. This is an alternative to an approach exemplified by Giunchiglia
and Maratea, (2006), where the authors focus on the question how qualitative
preferences may capture quantitative ones. In their work, quantitative
preferences (appearing within MaxSAT, for example) are translated into a
propositional formula with auxiliary atoms capturing numeric constraints.

###  5.1 min-one Family as W-Systems

######  Definition 14 (min-one and min-one⊆ problems)

For a vocabulary $\sigma$, let $\xi$ be a subset of $\sigma$ and $F$ be a CNF
formula over $\sigma$. By min-one${}^{\xi}_{F}$ (min-one⊆${}^{\xi}_{F}$) we
denote the set of interpretations $I$ over $\sigma$ that are models of $F$ and
$I\cap\xi$ are of minimal cardinality (subset minimal). We call members of
min-one${}^{\xi}_{F}$ (min-one⊆${}^{\xi}_{F}$) solutions to min-one (min-one⊆)
problem $F$ over $\sigma$ characterized by $\xi$.

###### Proposition 6

Let $F$ be min-one problem over $\sigma$ characterized by $\xi$. The solutions
to this problem are formed by the optimal models of w-system

$(F,\\{(\neg a,1)\mid a\in\xi\\})$ (17)

(where its theory and w-conditions are considered to be in sat-logic).

Construction of the w-system featured in Proposition 6 is intuitive: it
prefers models that contain fewest number of atoms, capturing the requirement
on minimal cardinality. The statement of Proposition 6 is in spirit of earlier
propositions, so that w-systems can be used to provide an alternative
definition for min-one problems. Indeed, w-system (17) can be identified with
respective min-one problem. The solutions to this problem are formed by the
optimal models of w-system (17).

The min-one formalism is an elaboration on a problem of satisfiability, where
models of a propositional formula are distinguished with respect to a
qualitative preference characterized by some vocabulary $\xi$. In a trivial
way we may utilize the language of w-systems to define a similar framework for
logic programs that we call min-one-asp. For a vocabulary $\sigma$, let $\xi$
be a subset of $\sigma$ and $\Pi$ be a logic program over $\sigma$; we call
program $\Pi$ a min-one-asp problem characterized by $\xi$. The solutions to
this problem are the optimal models of w-system

$(\Pi,\\{(\neg a,1)\mid a\in\xi\\}),$

where a theory of this w-system is in lp-logic and w-conditions of this
w-system are in sat-logic. Section 7 cites work that relates logic programs
under answer set semantics and SAT. With these relations in mind it is easy to
see how a tool for computing solutions to a min-one problem can be used for
computing solutions to a min-one-asp problem (for example, a variant of opt-
dll introduced in (Giunchiglia and Maratea, 2006, Theorem 5)). The following
result is immediate from the definitions of min-one and min-one-asp problems.

###### Proposition 7

For a vocabulary $\sigma$, let $\xi$ be a subset of $\sigma$; $\Pi$ be a logic
program over $\sigma$; and $F_{\Pi}$ be a CNF formula over $\sigma$ whose
models coincide with the answer sets of $\Pi$. The solutions to min-one
problem $F_{\Pi}$ characterized by $\xi$ coincide with the solutions to min-
one-asp problem $\Pi$ characterized by $\xi$.

In this section we continue to review the formalisms in light of their origins
as SAT problems enhanced by qualitative preferences. Yet, the narrative on the
min-one-asp problem sheds light on how the ideas of these formalisms can
easily be utilized within the world of answer set programming.

We now turn our attention to the min-one⊆ problem.

###### Proposition 8

Let $F$ be min-one⊆ problem over $\sigma$ characterized by $\xi$, let
$a_{1},a_{2},\dots,a_{n}$ be a permutation of $\xi$. Any optimal model of
w-system

$(F,\\{(\neg a_{i},1@i)\mid a_{i}\hbox{ is an element of
}a_{1},a_{2},\dots,a_{n}\\}),$ (18)

is a solution to this min-one⊆ problem.

Construction of the w-system featured in Proposition 8 mimics/is inspired by
the modification to the dll algorithm by opt-dll in order to obtain a behavior
of the algorithm that is suitable for computing a solution to min-one⊆
problem. Indeed, procedure opt-dll Giunchiglia and Maratea, (2006) forces an
order on assigning atoms in $\xi$ first exploring an option that a newly
considered atom is assigned false (i.e., interpretations that do not contain
this atom in them are considered first). As a result, a model found by opt-dll
is guaranteed to be subset minimal. Observe how levels in the definition of
w-system (18) are a key instrument to mimic the behavior of opt-dll and they
do that in an intuitive fashion. Future Section 6.2 illustrates how levels can
be flattened to a single one by means of adjusting the weights of the system.
Yet, in that case the natural use of levels as illustrated here would be lost
to crafting special-purpose weights.

The claims of Propositions 6 and 8 differ substantially: Proposition 8 looses
“definitional” power of Proposition 6. Rather, it illustrates how we can
construct a w-system whose optimal models capture some solutions of min-one⊆
problem. On the other hand, the next proposition allows us to see that all
solutions of min-one⊆ problem can be characterized by w-systems in style of
(18).

###### Proposition 9

Let $F$ be min-one⊆ problem over $\sigma$ characterized by $\xi$; $I$ be one
of its solution; and $a_{1},a_{2},\dots,a_{n}$ be a permutation of $\xi$ that
satisfies the following condition: for any pair of atoms $a_{i}$ and $a_{j}$
so that $i<j$ if $a_{j}$ is in $I$ then $a_{i}$ is also in $I$ (in other
words, this permutation orders atoms of $\xi$ that occur in $I$ prior to the
atoms of $\xi$ that do not occur in $I$). Then, $I$ is an optimal model of
w-system (18).

###  5.2 distancesat Family as W-Systems

######  Definition 15 (distancesat and distancesat⊆ problems)

For a vocabulary $\sigma$, let $\hat{I}$ be an interpretation of $\sigma$ and
$F$ be a CNF formula over $\sigma$. By distancesat${}^{\hat{I}}_{F}$
(distancesat⊆${}^{\hat{I}}_{F}$) we denote the set of interpretations $I$ over
$\sigma$ that are models of $F$ and set $(\hat{I}\setminus
I)\cup(I\setminus\hat{I})$ are of minimal cardinality (subset minimal). We
call members of distancesat${}^{\hat{I}}_{F}$ (distancesat⊆${}^{\hat{I}}_{F}$)
solutions to distancesat (distancesat⊆) problem $F$ over $\sigma$
characterized by $\hat{I}$.

We now claim similar formal results as in the case of the min-one family.

###### Proposition 10

Let $F$ be distancesat problem over $\sigma$ characterized by $\hat{I}$. The
solutions to this problem are formed by the optimal models of w-system

$(F,\\{(a,1)\mid a\in\hat{I}\\}\cup\\{(\neg a,1)\mid
a\in\sigma\setminus\hat{I}\\}).$ (19)

###### Proposition 11

Let $F$ be distancesat⊆ problem over $\sigma$ characterized by $\hat{I}$, let
$a_{1},a_{2},\dots,a_{n}$ be a permutation of $\sigma$. Any optimal model of
w-system

$\begin{array}[]{rll}(F,&\\{(a_{i},1@i)&\mid a_{i}\hbox{ is an element of
}a_{1},a_{2},\dots,a_{n}\hbox{ and }a_{i}\in\hat{I}\\}\cup\\\ &\\{(\neg
a_{i},1@i)&\mid a_{i}\hbox{ is an element of }a_{1},a_{2},\dots,a_{n}\hbox{
and }a_{i}\in\sigma\setminus\hat{I}\\}),\end{array}$ (20)

is a solution to this distancesat⊆ problem.

##  6 Formal Properties of w-systems

We now state some interesting formal properties about w-systems. Word Property
denotes the results that follow rather immediately from the model/optimal
model definitions. The concluding section of this paper provides proofs to the
propositions that appear in this section.

###### Property 1

Any two w-systems with the same hard theory have the same models.

Due to this property when stating the results for w-systems that share the
same hard theory, we only focus on optimal and min-optimal models.

###### Property 2

Any model of w-system of the form $(\mathcal{H},\emptyset)$ is optimal/min-
optimal.

###### Property 3

Optimal/min-optimal models of the following w-systems coincide

  * •

w-system $\mathcal{W}$ and

  * •

w-system resulting from $\mathcal{W}$ by dropping all of its w-conditions
whose weight is $0$.

Thus, the w-conditions, whose weight is $0$ are immaterial and can be removed.
For instance, we can safely simplify sample pw-MaxSAT problem (9) and MinMaxPL
problem (11) by dropping their w-conditions $(\neg a\vee b,0)$.

###### Property 4

Given a positive integer $a$, optimal/min-optimal models of the following
w-systems coincide

  * •

w-system $(\mathcal{H},\\{(T_{1},w_{1}@l_{1}),\dots,(T_{m},w_{m}@l_{m})\\})$
and

  * •

w-system $(\mathcal{H},\\{(T_{1},a\cdot w_{1}@l_{1}),\dots,(T_{m},a\cdot
w_{m}@l_{m})\\})$.

We call a w-system $\mathcal{W}$ level-normal, when we can construct the
sequence of numbers $1,2,\dots,|{\lambda({\mathcal{W}})}|$ from the elements
in ${\lambda({\mathcal{W}})}$. It is easy to see that we can always adjust
levels of w-conditions in $\mathcal{W}$ to respect such a sequence preserving
optimal models of original w-system $\mathcal{W}$.

###### Proposition 12

Optimal/min-optimal models of the following w-systems coincide

  * •

w-system $\mathcal{W}$ and

  * •

the level-normal w-system constructed from $\mathcal{W}$ by replacing each
level $l_{i}$ occurring in its w-conditions with its ascending sequence order
number $i$, where we arrange elements in ${\lambda({\mathcal{W}})}$ in a
sequence in ascending order $l_{1},l_{2},\dots
l_{|{\lambda({\mathcal{W}})}|}$.

Sample MaxPL problem (11) is not level normal. Yet, this proposition assures
us that it is safe to consider the level-normal w-system

$(F_{1},\\{(a,1),(b,1@2),(a\vee\neg b,2),(\neg a\vee b,0)\\})$ (21)

in its place. In the sequel we often assume level-normal w-systems without
loss of generality.

###### Proposition 13

For a w-system $\mathcal{W}=(\mathcal{H},\mathcal{Z})$, if every level
$l\in{\lambda({\mathcal{W}})}$ is such that for any distinct models $I$ and
$I^{\prime}$ of $\mathcal{W}$ the equality

$\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}=\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models B}]}$ (22)

holds then optimal/min-optimal models of w-systems $\mathcal{W}$ and
$(\mathcal{H},\emptyset)$ coincide. Or, in other words, any model of
$\mathcal{W}$ is also optimal and min-optimal model.

By this proposition, for instance, it follows that optimal models of pw-MaxSAT
problem $(F_{1},\\{(a,1),(b,1)\\})$ coincide with its models $\\{a\\}$ and
$\\{b\\}$ or, in other words, the problem can be simplified to
$(F_{1},\emptyset)$.

Let $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ be a w-system. For a set $S$ of
w-conditions, by ${\mathcal{W}}[{\setminus{S}}]$ we denote the w-system
$(\mathcal{H},\mathcal{Z}\setminus S)$.

###### Proposition 14

For a w-system $\mathcal{W}=(\mathcal{H},\mathcal{Z})$, if there is a set
$S\subseteq\mathcal{Z}$ of w-conditions all sharing the same level $l$ such
that for any distinct ${l}^{\uparrow}$-optimal/min-optimal models $I$ and
$I^{\prime}$ of $\mathcal{W}$ (or any distinct models $I$ and $I^{\prime}$ of
$\mathcal{W}$ in case ${l}^{\uparrow}$ is undefined) the equality (22), where
$\mathcal{W}_{l}$ is replaced by $S$, holds then $\mathcal{W}$ has the same
optimal/min-optimal models as ${\mathcal{W}}[{\setminus{S}}]$.

It is obvious that this proposition holds with more restrictive condition when
words ${l}^{\uparrow}$-optimal/min-optimal models are replaced by models. This
result provides us with the semantic condition on when it is “safe” to drop
some w-conditions from the w-system. By this proposition, for instance, it
follows that the optimal models of pw-MaxSAT problem (9) coincide with the
optimal models of w-system constructed from (9) by dropping its w-conditions
$(a,1)$ and $(b,1)$. To summarize, all listed results account to the fact that
the optimal models of pw-MaxSAT problem (9) and the following pw-MaxSAT
problem coincide

$(F_{1},\\{(a\vee\neg b,2)\\}).$ (23)

Let
${(\mathcal{H},\\{(T_{1},w_{1}@l_{1}),\dots,(T_{n},w_{n}@l_{n})\\})}^{-1\cdot}$
map a w-system into the following w-system $(\mathcal{H},\\{(T_{1},-1\cdot
w_{1}@l_{1}),\dots,(T_{n},-1\cdot w_{n}@l_{n})\\}).$ The next proposition
tells us that min-optimal models and optimal models are close relatives:

###### Proposition 15

For a w-system $\mathcal{W}$, the optimal models (min-optimal models) of
$\mathcal{W}$ coincide with the min-optimal models (optimal models) of
${\mathcal{W}}^{-1\cdot}$.

###  6.1 Eliminating Negative (or Positive) Weights

We call logics $\mathcal{L}$ and $\mathcal{L}^{\prime}$ compatible when their
vocabularies coincide, in other words, when
$\sigma_{\mathcal{L}}=\sigma_{\mathcal{L}^{\prime}}$. Let $\mathcal{L}$ and
$\mathcal{L}^{\prime}$ be compatible logics, and $T$ and $T^{\prime}$ be
theories in these logics, respectively. We call such theories compatible. For
compatible theories $T$ and $T^{\prime}$, we call $T$ and $T^{\prime}$ as well
as w-conditions $(T,w@l)$ and $(T^{\prime},w@l)$ equivalent  when
$sem(T)=sem(T^{\prime})$. For example, sat-logic theory (2) over vocabulary
$\\{a,b\\}$ is equivalent to lp-logic theory (4) over $\\{a,b\\}$.

The following proposition captures an apparent property of w-systems that
equivalent modules and w-conditions may be substituted by each other without
changing the overall semantics of the system.

###### Property 5

Models and optimal/min-optimal models of w-systems

$(\\{T_{1},\dots,T_{n}\\},\\{B_{1},\dots,B_{m}\\})\hbox{ and
}(\\{T^{\prime}_{1},\dots,T^{\prime}_{n}\\},\\{B^{\prime}_{1},\dots,B^{\prime}_{m}\\})$

coincide when (i) $T_{i}$ and $T^{\prime}_{i}$ ($1\leq i\leq n$) are
equivalent theories, and (ii) $B_{i}$ and $B^{\prime}_{i}$ ($1\leq i\leq m$)
are equivalent $w$-conditions.

For a theory $T$ of logic $\mathcal{L}$, we call a theory $\overline{T}$ in
logic $\mathcal{L}^{\prime}$, compatible to $\mathcal{L}$, complementary when
$sem(\overline{T})=Int(\sigma_{\mathcal{L}})\setminus sem(T)$. For example, in
case of pl-logic, theories $F$ and $\neg F$ are complementary. Similarly, a
theory $(\neg a\wedge\neg b)\vee(a\wedge b)$ in pl-logic over vocabulary
$\\{a,b\\}$ is complementary to theory (4) in lp-logic over $\\{a,b\\}$. It is
easy to see that given a theory in any logic we can always find, for instance,
a pl-logic or sat-logic theory complementary to it. Yet, given a theory in
some arbitrary logic we may not always find a theory complementary to it in
the same logic. For example, consider vocabulary $\\{a,b\\}$ and a wc-theory
$a\wedge b$. There is no complementary wc-theory to it over vocabulary
$\\{a,b\\}$.

Let $(T,w@l)$ be a w-condition; consider the following definitions:

$\begin{array}[]{l}{(T,w@l)}^{+}=\begin{cases}(T,w@l)&\hbox{when $w\geq 0$,
otherwise }\\\ (\overline{T},-1\cdot w@l)\\\ \end{cases}\\\ {}\\\
{(T,w@l)}^{-}=\begin{cases}(T,w@l)&\hbox{when $w\leq 0$, otherwise }\\\
(\overline{T},-1\cdot w@l)\\\ \end{cases}\end{array}$

where $\overline{T}$ denotes some theory complementary to $T$. It is easy to
see that + (and -) forms a family of mappings. Applying a member in this
family to a w-condition always results in a w-condition with nonnegative and
nonpositive weights respectively.

For a w-system $(\mathcal{H},\\{B_{1},\dots,B_{m}\\})$, we define

$\begin{array}[]{l}{(\mathcal{H},\\{B_{1},\dots,B_{n}\\})}^{+}=(\mathcal{H},\\{{B_{1}}^{+},\dots,{B_{n}}^{+}\\})\\\
{(\mathcal{H},\\{B_{1},\dots,B_{n}\\})}^{-}=(\mathcal{H},\\{{B_{1}}^{-},\dots,{B_{n}}^{-}\\}).\\\
\end{array}$ (24)

The following proposition tells us that negative/positive weights within
w-systems may be eliminated in favour of the opposite sign when theories
complementary to theories of w-conditions are found.

###### Proposition 16

Optimal/min-optimal models of w-systems $\mathcal{W}$, ${\mathcal{W}}^{+}$,
${\mathcal{W}}^{-}$ coincide.

The result above can be seen as a consequence of the following proposition:

###### Proposition 17

Optimal/min-optimal models of w-systems

  * •

$(\mathcal{H},\\{(T,w@l)\\}\cup\mathcal{Z})$ and

  * •

$(\mathcal{H},\\{(\overline{T},-1\cdot w@l)\\}\cup\mathcal{Z})$

coincide.

Proposition 16 suggests that in case of significantly expressive logic the
presence of both negative and positive weights in w-conditions is nearly a
syntactic sugar. Let us illustrate the applicability of this result in the
realm of optimization programs. First, we say that

  * •

a weak constraint (12) is positively-singular if either its weight $w\geq 0$
or $m=1$;

  * •

a weak constraint (12) is negatively-singular if either its weight $w\leq 0$
or $m=1$.

For example, the only weak constraint/wc-logic w-condition of o-program (16)
follows

$(a\wedge\neg b,-2@1).$

This weak constraint is negatively-singular. Let us denote it by $C_{1}$.

Given a positively-singular weak constraint/wc-logic w-condition $B=(T,w@l)$,
it is easy to see that a mapping

$B^{\uparrow}=\begin{cases}B&\hbox{when $w\geq 0$, otherwise }\\\ (\neg
a,-1\cdot w@l)&\hbox{when $T$ has the form $a$}\\\ (a,-1\cdot w@l)&\hbox{when
$T$ has the form $\neg a$}\\\ \end{cases}$

is in the ${B}^{+}$ family. Given a negatively-singular weak constraint/wc-
logic w-condition $B$, $B^{\uparrow}$ mapping is defined as above by replacing
$w\geq 0$ condition with $w\leq 0$. For instance, $C_{1}^{\uparrow}=C_{1}$. It
is easy to see that this mapping is in the ${B}^{-}$ family.

Similarly, given a positively-singular weak constraint/wc-logic w-condition
$B$ of the form (15), it is easy to see that a mapping

$B^{sat}=\begin{cases}\Big{(}~{}\eqref{eq:wcwcc},-1\cdot w@l\Big{)}&\hbox{when
$w\geq 0$, otherwise }\\\ B&\\\ \end{cases}$

is in the ${B}^{-}$ family. Given a negatively-singular weak constraint/wc-
logic w-condition $B$ of the form (15), $B^{sat}$ mapping is defined as above
by replacing $w\geq 0$ condition with $w\leq 0$. It is easy to see that this
mapping is in the ${B}^{+}$ family. Note that the resulting w-condition of
$(\cdot)^{sat}$ mapping is in sat-logic. As an example, consider negatively-
singular w-condition $C_{1}$,

$C_{1}^{sat}=(\neg a\vee b,2@1).$

We call optimization program positively-singular (negatively-singular) when
all of its w-conditions are positively-singular (negatively-singular). For a
positively/negatively-singular optimization program
$(\Pi,\\{B_{1},\dots,B_{n}\\})$,

$\begin{array}[]{lll}(\Pi,\\{B_{1},\dots,B_{n}\\})^{\uparrow}&=&(\Pi,\\{B_{1}^{\uparrow},\dots,B_{n}^{\uparrow}\\}),\\\
(\Pi,\\{B_{1},\dots,B_{n}\\})^{sat}&=&(\Pi,\\{B_{1}^{sat},\dots,B_{n}^{sat}\\}).\end{array}$

For example, let $\mathcal{P}_{1}$ denote negatively-singular o-program (16).
Then, $\mathcal{P}_{1}^{\uparrow}=\mathcal{P}_{1}$ and
$\mathcal{P}_{1}^{sat}=(\Pi_{1},\\{(\neg a\vee b,2@1)\\})$.

Propositions 5 and 16 tell us that optimal answer sets of
positively/negatively-singular o-program $\mathcal{P}$ coincide with min-
optimal models of w-system $\mathcal{P}^{\uparrow}$. Also, they tell us that
optimal answer sets of positively/negatively-singular o-program $\mathcal{P}$
coincide with min-optimal models of w-system $\mathcal{P}^{sat}$.

We note that the restriction on an optimization program to be
positively/negatively-singular is not essential. For example, we now describe
a procedure that given an arbitrary program constructs positively-singular
one. In particular, given a program for every weak constraint $C$ of the form
(12), whose weight is negative

  * •

adding to its hard fragment a rule of the form

$a^{C}\leftarrow a_{1},\dotsc,a_{\ell},\ not\ a_{\ell+1},\dotsc,\ not\ a_{m},$

where $a_{C}$ is a freshly introduced atom and

  * •

replacing weak constraint $C$ with

$:\sim a^{C}[w@l]$

produces a positively-singular optimization program. The answer sets of these
two programs are in one to one correspondence. Dropping freshly introduced
atoms $a^{C}$ from the answer sets of the newly constructed program results in
the answer sets of the original program. This fact is easy to see given the
theorem on explicit definitions (Ferraris,,2005). Alternatively, we can apply
the transformation described above to every weak constraint $C$ of the form
(12), whose $m>1$. In this case the resulting program is both positively-
singular and negatively-singular. Alviano, (2018) describes a normalization
procedure in this spirit.

###  6.2 Eliminating Levels

We call a w-system $\mathcal{W}$ (strictly) positive when all of its
w-conditions have (positive) nonnegative weights. Similarly, we call a
w-system $\mathcal{W}$ (strictly) negative when all of its w-conditions have
(negative) nonpositive weights. As we showed earlier the w-conditions with $0$
weights may safely be dropped so as such the difference between, for example,
strictly positive and positive programs is inessential.

We now show that the notion of level in the definition of w-conditions is
immaterial from the expressivity point of view, i.e., they can be considered
as syntactic sugar. Yet, they are convenient mechanism for representing what
is called hierarchical optimization constraints. It was also shown in practice
that it is often of value to maintain hierarchy of optimization requirements
in devising algorithmic solutions to search problems with optimization
criteria (Argelich et al.,,2009). Here we illustrate that given an arbitrary
w-system we can rewrite it using w-conditions of the form $(T,w)$. This change
simplifies the definition of an optimal model by reducing it to a single
condition; indeed, see Definition 7. Intuitively, we adjust weights $w$ across
the w-conditions in a way that mimics their distinct levels. A procedure in
style was reported by Alviano, (2018) for the case of o-programs. In this
work, we generalize that result to arbitrary w-systems that immediately makes
it applicable to logical frameworks that go beyond logic programs. We also
provide a formal proof of the result that was missing in the mentioned paper
by Alviano,.

Let pair $\mathcal{W}=(\mathcal{H},\mathcal{Z})$ be strictly positive level-
normal w-system. As illustrated earlier restricting w-systems to being
positive can be seen as an inessential restriction; recall Proposition 16. We
define the number $M_{i}$ ($0\leq i<|{\lambda({\mathcal{W}})}|$) as

$M_{i}=\begin{cases}1&\hbox{when $i=0$, otherwise }\\\
\displaystyle{1+\sum_{(T,w@i)\in\mathcal{Z}}}w.&\\\ \end{cases}$

Intuitively, this number gives us the upper bound, incremented by 1, for the
sum of the values of the weights of the w-conditions of level $i$ (we identify
$M_{0}$ with $1$). We now define the number that serves the role of the factor
for adjusting each weight associated with some level. For level $i$ $(1\leq
i\leq|{\lambda({\mathcal{W}})}|)$, let $f_{i}$ be the number computed as

$f_{i}=\displaystyle{\prod_{0\leq j<i}{M_{j}}}.$

By $\mathcal{Z}^{1}$ we denote the set of w-conditions constructed from
$\mathcal{Z}$ as follows

$\\{(T,f_{i}\cdot w)\mid(T,w@i)\in\mathcal{Z}\\}$ (25)

By $\mathcal{W}^{1}$ we denote the w-system resulting from replacing
$\mathcal{Z}$ with $\mathcal{Z}^{1}$.

###### Proposition 18

Optimal/min-optimal models of strictly positive level-normal w-systems
$\mathcal{W}=(\mathcal{H},\mathcal{Z})$ and
$\mathcal{W}^{1}=(\mathcal{H},\mathcal{Z}^{1})$ coincide.

Recall an example of level-normal w-system (21). Property 3 tells us that its
models and optimal/min-optimal models coincide with these of strictly positive
level-normal w-system

$(F_{1},\\{(a,1),(a\vee\neg b,2),(b,1@2)\\}).$

Let us denote this w-system as $\mathcal{W}_{1}$. For w-system
$\mathcal{W}_{1}$,

$\begin{array}[]{lll}M_{0}=1&M_{1}=4&\\\ &f_{1}=1&f_{2}=4\\\ \end{array}$

W-system $\mathcal{W}_{1}^{1}$ follows

$(F_{1},\\{(a,1),(a\vee\neg b,2),(b,4)\\}).$

Proposition 18 tells us that optimal/min-optimal models of w-systems
$\mathcal{W}_{1}$ and $\mathcal{W}_{1}^{1}$ coincide.

##  7 Optimization Programs as pw-MaxSAT/pw-MinSAT Problems

Logic programs under answer set semantic and propositional formulas are
closely related (see, for instance, work by Lierler, (2017) for an overview of
translations). For example, for so called “tight” programs a well known
completion procedure (Clark,,1978) transforms a logic program into a
propositional formula so that the answer sets of the former coincide with the
models of the later. Once this formula is clausified the problem becomes a SAT
problem. For nontight programs extensions of completion procedure are
available (Lin and Zhao,; Janhunen,,2002; 2006). Some of those extensions
introduce auxiliary atoms. Yet, the appearance of these atoms is inessential
as models of resulting formulas are in one to one correspondence with original
answer sets. The later can be computed from the former by dropping the
auxiliary atoms. The bottom line is that a number of known translations from
logic programs to SAT exists. Numerous answer set solvers, including but not
limited to cmodels (Giunchiglia et al.,,2006) and lp2sat (Janhunen,,2006),
rely on this fact by translating a given logic program into a SAT formula and
then applying SAT solvers for computing models/answer sets. For a logic
program $\Pi$ over vocabulary $\sigma$ (that we identify with a module in lp-
logic), by $F_{\Pi}$ we denote a SAT formula, whose models coincide with these
of $\Pi$. For example, recall that $F_{1}$ and $\Pi_{1}$ denote sat-formula
(2) and logic program (4). Formula $F_{1}$ forms one of the possible formulas
$F_{\Pi_{1}}$. In fact, $F_{1}$ corresponds to the clausified completion of
program $\Pi_{1}$, which has the form

$(a\leftrightarrow\neg b)\wedge(b\leftrightarrow\neg a).$

In previous sections we illustrated how multiple levels and negative weights
in w-systems/singular optimization programs can be eliminated in favor of a
single level and positive weights. Thus, without loss of generality we
consider here singular optimization programs with a single level. The
following result is a consequence of Propositions 15 and 16.

###### Proposition 19

Optimal answer sets of a positive-singular o-program
$(\Pi,\\{B_{1},\dots,B_{m}\\})$, whose all conditions are of the same level
$1$, coincide with optimal models of pw-MaxSAT problem
${(F_{\Pi},\\{B_{1}^{sat},\dots,B_{n}^{sat}\\})}^{-1\cdot}$.

The next proposition follows from Proposition 16.

###### Proposition 20

Optimal answer sets of a negatively-singular o-program
$(\Pi,\\{B_{1},\dots,B_{m}\\})$, whose all conditions are of the same level
$1$, coincide with optimal models of pw-MinSAT problem
${(F_{\Pi},\\{B_{1}^{sat},\dots,B_{n}^{sat}\\})}$.

This result tells us, for example, that optimal answer sets of optimization
program (16) coincide with optimal models of pw-MinSAT problem (10).

Propositions 19 and 20 tells us how to utilize MaxSAT/MinSAT solvers for
finding optimal answer sets of a program in similar ways as SAT solvers are
currently utilized for finding answer sets of logic programs as exemplified by
such answer set solvers as cmodels or lp2sat.

##  8 Proofs

We often show results for optimal models only, as the arguments for min-
optimal models follow the same lines. Given recursive Definition 9 of
$l$-(min)-optimal models, inductive argument is a common technique in proof
construction about properties of such models. Below, we refer to the induction
on levels of a considered w-system $\mathcal{W}$, where we assume elements in
${\lambda({\mathcal{W}})}$ to be arranged in the descending order $m_{1},\dots
m_{n}$ ($n=|{\lambda({\mathcal{W}})}|$); so that the base case is illustrated
for the greatest level $m_{1}$, whereas inductive hypothesis is assumed for
level $m_{i}$ and then illustrated to hold for level $m_{i+1}$. Note how,
${m_{i+1}}^{\uparrow}=m_{i}$.

###  8.1 Proofs for Formal Results in Section 3

An inductive proof on levels of $\mathcal{W}$ relying on the definition of
$l$-optimal models suffices for Lemma 1. We omit it for its simplicity. Lemma
2 follows immediately from Lemma 1 and an observation that for a pair $I$,
$I^{\prime}$ of $l$-optimal/$l$-min-optimal models of w-system $\mathcal{W}$
the following equality holds

$\displaystyle{{\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}}}=\displaystyle{{\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models B}]}}}.$
(26)

This observations stems from the definition of $l$-optimal/$l$-min-optimal
models. There is one more lemma that we find of use in proving Proposition 1.
The claim of the lemma can be shown by induction on levels of $\mathcal{W}$.

###### Lemma 3

For a w-system $\mathcal{W}=(\mathcal{H},\mathcal{Z})$, level
$l^{\prime}\in{\lambda({\mathcal{W}})}$, and a model $I^{\prime}$ of
$\mathcal{W}$, if $I$ is $l^{\prime}$-optimal model of $\mathcal{W}$ such that
for all levels $l\geq l^{\prime}$ equality (26) holds then $I^{\prime}$ is an
$l^{\prime}$-optimal model of $\mathcal{W}$ as well.

######  Proof 8.1 (Proof of Proposition 1).

We consider the relation between Definitions 8 and 9. We will illustrate the
equivalence between optimal models defined in different terms. We omit an
argument for min-optimal models as it follows these lines. First, we
illustrate that any optimal model per Definition 8 is also an optimal model
per Definition 9. We call this direction Left-to-right. Second, we illustrate
that any optimal model per Definition 9 is also an optimal model per
Definition 8. We call this direction Right-to-left.

Left-to-right. Per Definition 8 model $I^{*}$ of w-system $\mathcal{W}$ is
optimal if there is no model $I^{\prime}$ of $\mathcal{W}$ that max-dominates
$I^{*}$. Consider such model $I^{*}$. We now illustrate that $I^{*}$ is also
an optimal model of $\mathcal{W}$ per Definition 9. In other words, $I^{*}$ is
$l$-optimal model for every level $l\in{\lambda({\mathcal{W}})}$. By
contradiction. Assume the later statement is not the case: there is a level
$l^{\prime}\in{\lambda({\mathcal{W}})}$ such that $I^{*}$ is not an
$l^{\prime}$-optimal model; take $l$ to be the greatest value in
${\lambda({\mathcal{W}})}$ that satisfies this property. Consequently, $I^{*}$
does not satisfies equation

$I^{*}=\displaystyle{\operatorname*{arg\,max}_{I}{\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}}}$ (27)

where

  * •

$I$ ranges over models of $\mathcal{W}$ if $l$ is the greatest level in
${\lambda({\mathcal{W}})}$,

  * •

$I$ ranges over ${l}^{\uparrow}$-optimal models of $\mathcal{W}$, otherwise.

Case 1. $l$ is the greatest level in ${\lambda({\mathcal{W}})}$. There is a
model $I^{\prime}$ of $\mathcal{W}$ such that

$\displaystyle{{\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}}}>\displaystyle{{\sum_{B\in\mathcal{W}_{l}}{[{I^{*}\models B}]}}}.$ (28)

Consequently, $I^{\prime}$ max-dominates $I^{*}$. We derive a contradiction.

Case 2. $l$ is not the greatest level in ${\lambda({\mathcal{W}})}$. Due to
the choice of $l$, there is a ${l}^{\uparrow}$-optimal model $I^{\prime}$ of
$\mathcal{W}$ such that inequality (28) holds. By Lemmas 1 and 2, for every
level $l^{\prime\prime}\in{\lambda({\mathcal{W}})}$ such that
$l^{\prime\prime}\geq{l}^{\uparrow}$ equality (26) holds, where we replace $l$
by $l^{\prime\prime}$ and $I$ by $I^{*}$. Consequently, $I^{\prime}$ max-
dominates $I^{*}$. We derive a contradiction.

Right-to-left. Per Definition 9 model $I^{*}$ of w-system $\mathcal{W}$ is
optimal if it is $l$-optimal for every level $l\in{\lambda({\mathcal{W}})}$.
Consider such model $I^{*}$. We now illustrate that $I^{*}$ is also an optimal
model of $\mathcal{W}$ per Definition 8. In other words, there is no model
$I^{\prime}$ of $\mathcal{W}$ that max-dominates $I^{*}$. By contradiction.
Assume the later statement is not the case: there is a level
$l\in{\lambda({\mathcal{W}})}$ and a model $I^{\prime}$ such that following
conditions are satisfied:

  1. 1.

for any level $l^{\prime}>l$ the following equality holds

$\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I^{*}\models
B}]}}=\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I^{\prime}\models
B}]}}$

  2. 2.

the inequality (28) holds for level $l$.

Case 1. $l$ is the greatest level. Consequently, $I^{*}$ does not satisfy
equation (27). We derive a contradiction.

Case 2. $l$ is not the greatest level.

Case 2.1 There is level $l^{\prime\prime}>l$ such that $I^{\prime}$ is not
$l^{\prime\prime}$-optimal model of $\mathcal{W}$. By Lemma 3 we conclude that
model $I^{*}$ is not $l^{\prime\prime}$-optimal model of $\mathcal{W}$
(indeed, assume the opposite and one derives the contradiction to the
statement of the lemma). We derive a contradiction.

Case 2.2 Model $I^{\prime}$ is $l^{\prime\prime}$-optimal model of
$\mathcal{W}$ for every level $l^{\prime\prime}>l$. By Lemma 3 we conclude
that model $I^{*}$ is $l^{\prime\prime}$-optimal model of $\mathcal{W}$ for
every level $l^{\prime\prime}>l$. Consequently, both $I^{\prime}$ and $I^{*}$
are ${l}^{\uparrow}$-optimal models of $\mathcal{W}$. Condition (28)
contradicts the fact that $I^{*}$ is a solution to equation (27).

###  8.2 Proofs for Formal Results in Section 4

######  Proof 8.2 (Proof of Proposition 2).

Consider an arbitrary interpretation $I^{*}$ over $\sigma$. We show that
$I^{*}$ is a solution to MaxSAT problem $F$ if and only if $I^{*}$ is an
optimal model of w-system $(T_{\sigma},\\{(C,{1})\mid C\in F\\})$. Note how
the considered w-system is of a special form so that Definition 7 is
applicable. Interpretation $I^{*}$ is a solution to MaxSAT problem $F$ if and
only if

$I^{*}=arg\max_{I}{\sum_{C\in F}{[{I\models C}]}},$

where $I$ ranges over all interpretations over $\sigma$. Interpretation
$I^{*}$ is an optimal model of w-system $(T_{\sigma},\\{(C,{1})\mid C\in
F\\})$ if and only if

$I^{*}=arg\max_{I}{\sum_{B\in\\{(C,{1})\mid C\in F\\}}{[{I\models B}]}},$

where $I$ ranges over all models of $T_{\sigma}$, which are all
interpretations over $\sigma$.

Note how taking the definitions (5) and (7) into account we conclude that for
any interpretation $I$ over $\sigma$,

$\sum_{B\in\\{(C,{1})\mid C\in F\\}}{[{I\models B}]}=\sum_{C\in F}{[{I\models
C}]}.$

Proofs of Propositions 3 and 4 follow the logic of the presented proof of
Proposition 2. In proofs of these propositions, we have to rely on the fact
that given a weighted MaxSAT/MinSAT problem $P$ over $\sigma$ and any
interpretation $I$ over $\sigma$,

$\sum_{(C,w)\in P}{[{I\models(C,w)}]}=\sum_{(C,w)\in P}{w\cdot[{I\models
C}]}.$

######  Proof 8.3 (Proof of Proposition 5).

This proposition considers the relation between

  * •

an optimization logic program $(\Pi,W)$ over $\sigma$ and

  * •

w-system $\big{(}\Pi,\\{(D,{w@l})\mid D[w@l]\in W\\}\big{)}$ – where $\Pi$ is
an lp-logic module and pairs of the form $(D,{w@l})$ are wc-logic
w-conditions.

It is important to note that for any model $J$ and any level $k$, the
following equality holds

$\sum_{B\in\\{(D,{w@{k}})\mid D[w@{k}]\in W\\}}{[{J\models
B}]}=\sum_{D[w@k]\in W}w\cdot{[{J\models D}]}.$

With this observation, the argument is straightforward given Definition 8 of
min-optimal models of w-systems.

###  8.3 Proofs for Formal Results in Section 5

######  Proof 8.4 (Proof of Proposition 6).

Consider an arbitrary interpretation $I^{*}$ over $\sigma$. We show that
$I^{*}$ is a solution to min-one problem $F$ over $\sigma$ characterized by
$\xi$ if and only if $I^{*}$ is an optimal model of w-system
$\mathcal{W}=(F,\\{(\neg a,1)\mid a\in\xi\\})$. Interpretation $I^{*}$ is a
solution to min-one problem $F$ if and only if

$I^{*}=arg\min_{I}{|I\cap\xi|}=arg\min_{I}{\sum_{a\in
I\cap\xi}1}=arg\max_{I}{\sum_{a\in\xi\hbox{ and }a\not\in I\cap\xi}1},$ (29)

where $I$ ranges over models of $F$. Note how the considered w-system is of a
special form so that Definition 7 is applicable. Interpretation $I^{*}$ is an
optimal model of w-system $\mathcal{W}$ if and only if

$I^{*}=\displaystyle{\operatorname*{arg\,max}_{I}{\sum_{a\in\xi}{[{I\models\neg
a}]}}=arg\max_{I}{\sum_{a\in\xi\hbox{ and }a\not\in I\cap\xi}1}},$ (30)

where $I$ ranges over models of $\mathcal{W}$. Right hand sides of conditions
(29) and (30) coincide, which concludes the proof.

######  Proof 8.5 (Proof of Proposition 8).

Consider an arbitrary interpretation $I^{*}$ over $\sigma$. Take $I^{*}$ to be
an optimal model of w-system (18), where

$a_{1},a_{2},\dots,a_{n}$ (31)

is a permutation of $\xi$. We show that $I^{*}$ is a solution to min-one⊆
problem $F$ (over $\sigma$ characterized by $\xi$). By contradiction. Assume
the last claim is not the case. Given that $I^{*}$ is an optimal model of
w-system (18), it is hence a model of $F$. Thus, for $I^{*}$ not to be a
solution to min-one⊆ problem $F$ there must exist model $I$ of $F$ such that
$I\cap\xi\subset I^{*}\cap\xi$. We now show that $I$ max-dominates $I^{*}$,
which will lead us to contradiction with the assumption that $I^{*}$ is an
optimal model. Take the rightmost occurrence of atoms $a_{i}$ in permutation
(31) such that $a_{i}\in(I^{*}\cap\xi)\setminus I$. From the fact that
$I\cap\xi$ is a subset of $I^{*}\cap\xi$, it follows for any $j>i$, $a_{j}$ in
permutation (31) is such that either $a_{j}\in I$ and $a_{j}\in I^{*}$ or
$a_{j}\not\in I$ and $a_{j}\not\in I^{*}$. In other words, for any $j>i$,
$[{I\models\neg a_{j}}]=[{I^{*}\models\neg a_{j}}]$; and for $j$,
$[{I\models\neg a_{j}}]=1$ and $[{I^{*}\models\neg a_{j}}]=0$. We just
illustrated that for level $i$ among the levels of the considered w-system the
conditions for $I$ max-dominating $I^{*}$ are satisfied.

######  Proof 8.6 (Proof of Proposition 9).

We consider the notation exactly as in the ”let”-statement of the statement of
the proposition. By contradiction. Assume that $I$ is not an optimal model of
w-system (18). Then there is a model $I^{\prime}$ of $F$ that max-dominates
$I$. Hence, there is a level $l$ (an index in permutation) so that (a) for any
level $l^{\prime}>l$, $[{I\models\neg a_{l^{\prime}}}]=[{I^{\prime}\models\neg
a_{l^{\prime}}}]$ and (b) for level $l$, $[{I^{\prime}\models\neg
a_{l}}]>[{I\models\neg a_{l^{\prime}}}]$. By (b), we conclude (c) $a_{l}$ is
such that $a_{l}\in I$ and $a_{l}\not\in I^{\prime}$. From (a) and the fact
that the considered permutation orders atoms of $\xi$ that occur in $I$ prior
to the atoms of $\xi$ that do not occur in $I$, we conclude that (d) there is
no atom in $\xi$ that is not in $I$ but is in $I^{\prime}$. From (c) and (d)
it follows that $I^{\prime}\cap\xi\subset I$. We derive a contradiction.

######  Proof 8.7 (Proof of Proposition 10).

Consider an arbitrary interpretation $I^{*}$ over $\sigma$. We show that
$I^{*}$ is a solution to distancesat problem $F$ over $\sigma$ characterized
by $\hat{I}$ if and only if $I^{*}$ is an optimal model of w-system (19). Per
definition, interpretation $I^{*}$ is a solution to distancesat problem $F$ if
and only if

$I^{*}=\operatorname*{arg\,min}_{I}{|(\hat{I}\setminus
I)\cup(I\setminus\hat{I})|},$

where $I$ ranges over models of $F$. With the use of Venn diagrams it is easy
to see that we may rewrite this expression as

$I^{*}=\operatorname*{arg\,max}_{I}{|\big{(}\hat{I}\cap
I\big{)}\cup\big{(}(\sigma\setminus
I)\cap(\sigma\setminus\hat{I})\big{)}|}=\operatorname*{arg\,max}_{I}{|\big{(}\hat{I}\cap
I\big{)}\cup\big{(}\sigma\setminus(I\cup\hat{I})\big{)}|}.$

Obviously, sets $\hat{I}\cap I$ and $\sigma\setminus(I\cup\hat{I})$ are
disjoint. Consequently,

$I^{*}=\operatorname*{arg\,max}_{I}{|\hat{I}\cap
I|+|\sigma\setminus(I\cup\hat{I})|}=\operatorname*{arg\,max}_{I}{\sum_{a\in\hat{I}\hbox{
and }a\in I}{1}+\sum_{a\in\sigma\hbox{ and }a\not\in\hat{I}\hbox{ and
}a\not\in I}{1}}.$ (32)

Note how the considered w-system is of a special form so that Definition 7 is
applicable. Interpretation $I^{*}$ is an optimal model of w-system (19) if and
only if

$I^{*}=\displaystyle{\operatorname*{arg\,max}_{I}{\sum_{a\in\hat{I}}{[{I\models
a}]}+\sum_{a\in\sigma\setminus\hat{I}}{[{I\models\neg
a}]}}=\operatorname*{arg\,max}_{I}{\sum_{a\in\hat{I}\hbox{ and }a\in
I}{1}+\sum_{a\in\sigma\hbox{ and }a\not\in\hat{I}\hbox{ and }a\not\in
I}{1}}},$ (33)

where $I$ ranges over models of $F$. Right hand sides of conditions (32) and
(33) coincide, which concludes the proof.

######  Proof 8.8 (Proof of Proposition 11).

Consider an arbitrary interpretation $I^{*}$ over $\sigma$. Take $I^{*}$ to be
an optimal model of w-system (20), where

$a_{1},a_{2},\dots,a_{n}$ (34)

is a permutation of $\sigma$. We show that $I^{*}$ is a solution to
distancesat⊆ problem $F$ (over $\sigma$ characterized by $\hat{I}$). By
contradiction. Assume the last claim is not the case. Given that $I^{*}$ is an
optimal model of w-system (20), it is hence a model of $F$. Thus, for $I^{*}$
not to be a solution to distancesat⊆ problem $F$ there must exist model $I$ of
$F$ such that

$\Big{(}(\hat{I}\setminus
I)\cup(I\setminus\hat{I})\Big{)}\subset\Big{(}(\hat{I}\setminus
I^{*})\cup(I^{*}\setminus\hat{I})\Big{)}.$

To satisfy this condition it follows that $I$ is such that

  * (i)

it contains all elements from $\hat{I}\cap I^{*}$ and

  * (ii)

it contains no elements that are not in $\hat{I}\cup I^{*}$.

We now show that $I$ max-dominates $I^{*}$, which will lead us to
contradiction with the assumption that $I^{*}$ is an optimal model. Take the
rightmost occurrence of atoms $a_{i}$ in permutation (34) such that either

  * •

$a_{i}\in I$ and $a_{i}\in\hat{I}$ and $a_{i}\not\in I^{*}$ (and, hence
$[{I\models a_{j}}]=1$ and $[{I^{*}\models a_{j}}]=0$) or

  * •

$a_{i}\not\in I$ and $a_{i}\not\in\hat{I}$ and $a_{i}\in I^{*}$ (and, hence
$[{I\models\neg a_{j}}]=1$ and $[{I^{*}\models\neg a_{j}}]=0$).

Given the choice of index $i$ above, we analyze the possibilities for all
occurrences $a_{j}$ with $j>i$ in permutation (34). They are such that either

  * •

$a_{j}\in I$ and $a_{j}\in\hat{I}$ and $a_{j}\in I^{*}$ (and, hence
$[{I\models a_{j}}]=1=[{I^{*}\models a_{j}}]=1$ ), or

  * •

$a_{j}\in I$ and $a_{j}\not\in\hat{I}$ and $a_{j}\in I^{*}$ (and, hence
$[{I\models\neg a_{j}}]=0=[{I^{*}\models\neg a_{j}}]=0$ ), or

  * •

$a_{j}\in I$ and $a_{j}\not\in\hat{I}$ and $a_{j}\not\in I^{*}$ (this is an
impossible case due to condition (ii)), or

  * •

$a_{j}\not\in I$ and $a_{j}\in\hat{I}$ and $a_{j}\in I^{*}$ (this is an
impossible case due to condition (i)), or

  * •

$a_{j}\not\in I$ and $a_{j}\in\hat{I}$ and $a_{j}\not\in I^{*}$ (and, hence
$[{I\models a_{j}}]=0=[{I^{*}\models a_{j}}]=0$ ), or

  * •

$a_{j}\not\in I$ and $a_{j}\not\in\hat{I}$ and $a_{j}\not\in I^{*}$ (and,
hence $[{I\models\neg a_{j}}]=0=[{I^{*}\models\neg a_{j}}]=0$).

The conditions within the parenthesis in every considered case are sufficient
to conclude that for for level $i$ among the levels of the considered w-system
the conditions for $I$ max-dominating $I^{*}$ are satisfied.

###  8.4 Proofs for Formal Results in Section 6

Proof of Proposition 12 follows from the fact that the numeric value of any
level itself is inessential in the key computations associated with
establishing optimal models. Rather, the order of levels with respect to
greater relation matters (recall the definition of ${(\cdot)}^{\uparrow}$
operation). It is easy to see that changing levels of the w-conditions using
the procedure described in Proposition 12 preserves original order of the
levels with respect to greater relation.

Proposition 13 follows immediately from Proposition 14. We show that
Proposition 14 holds.

######  Proof 8.9 (Proof of Proposition 14).

Let $l$ be the level so that there is a set $S\subseteq\mathcal{Z}_{l}$ of
w-conditions such that for any distinct ${l}^{\uparrow}$-optimal models $I$
and $I^{\prime}$ of $\mathcal{W}$ the following equality holds

$\sum_{B\in S}{[{I\models B}]}=\sum_{B\in S}{[{I^{\prime}\models B}]}.$

Let us denote the number associated with the sum in this equality by letter
$c$, i.e., $\displaystyle{c=\sum_{B\in S}{[{I\models B}]}}$ (where $I$ is any
${l}^{\uparrow}$-optimal model of $\mathcal{W}$).

Note that for every level $l^{\prime}>l$,
$\mathcal{W}_{l^{\prime}}={\mathcal{W}}[{\setminus{S}}]_{l^{\prime}}$. Using
simple inductive argument on levels of $\mathcal{W}$ that are greater than $l$
suffices to show that $l^{\prime}$-optimal models of $\mathcal{W}$ and
${\mathcal{W}}[{\setminus{S}}]$ coincide. Consequently,
${l}^{\uparrow}$-optimal models of $\mathcal{W}$ and
${\mathcal{W}}[{\setminus{S}}]$ coincide.

We now show that $l$-optimal models of $\mathcal{W}$ and
${\mathcal{W}}[{\setminus{S}}]$ coincide. We have to illustrate that equation
(6) and

$I^{*}=\displaystyle{\operatorname*{arg\,max}_{I}{\sum_{B\in{\mathcal{W}_{l}\setminus
S}}{[{I\models B}]}}}$

have the same solutions, when $I$ ranges over ${l}^{\uparrow}$-optimal models
of $\mathcal{W}$. This is apparent from the fact that the right hand side
(RHS) of the equation (6) can be rewritten as

$\begin{array}[]{l}\displaystyle{\operatorname*{arg\,max}_{I}\Big{(}{\sum_{B\in{\mathcal{W}_{l}\setminus
S}}{[{I\models B}]}}+{\sum_{B\in S}{[{I\models B}]}\Big{)}}}=\\\
\displaystyle{\operatorname*{arg\,max}_{I}\Big{(}\sum_{B\in{\mathcal{W}_{l}\setminus
S}}{[{I\models B}]}+c\Big{)}}=\\\
\displaystyle{\operatorname*{arg\,max}_{I}{\sum_{B\in{\mathcal{W}_{l}\setminus
S}}{[{I\models B}]}}}.\end{array}$

Using simple inductive argument on levels of $\mathcal{W}$ that are less than
$l$ suffices to show that $l^{\prime}$-optimal models of $\mathcal{W}$ and
${\mathcal{W}}[{\setminus{S}}]$ coincide, where $l^{\prime}$ is any level less
than $l$.

######  Proof 8.10 (Proof of Proposition 15).

To show that the optimal models of $\mathcal{W}$ coincide with the min-optimal
models of ${\mathcal{W}}^{-1\cdot}$, it is sufficient to show that for any
level in ${\lambda({\mathcal{W}})}$, $l$-optimal models of $\mathcal{W}$
coincide with $l$-min-optimal models of ${\mathcal{W}}^{-1\cdot}$. We first
note that models of $\mathcal{W}$ and ${\mathcal{W}}^{-1\cdot}$ coincide. By
induction on levels of $\mathcal{W}$.

Base case. $l$ is the greatest level. A model $I^{*}$ of $\mathcal{W}$ is
$l$-optimal if and only if $I^{*}$ satisfies equation (27), where $I$ ranges
over models of $\mathcal{W}$. It is easy to see that we can rewrite this
equation as

$I^{*}=\displaystyle{\operatorname*{arg\,min}_{I}{\sum_{B\in\mathcal{W}_{l}}-1\cdot{[{I\models
B}]}}}.$

It immediately follows from the construction of ${\mathcal{W}}^{-1\cdot}$ that
this equation can be rewritten as

$I^{*}=\displaystyle{\operatorname*{arg\,min}_{I}{\sum_{B\in{\mathcal{W}}^{-1\cdot}_{l}}{[{I\models
B}]}}}.$

Thus $I^{*}$ is an $l$-min-optimal model of ${\mathcal{W}}^{-1\cdot}$ as the
equation above is exactly the one from the definition of $l$-min-optimal
models of ${\mathcal{W}}^{-1\cdot}$; plus recall that models of $\mathcal{W}$
and ${\mathcal{W}}^{-1\cdot}$ coincide.

Inductive case argument follows similar lines.

Proposition 16 follows immediately from Proposition 17. We show that
Proposition 17 holds.

######  Proof 8.11 (Proof of Proposition 17).

We show the argument for optimal models for the case of w-systems
$\mathcal{W}=(\mathcal{H},\\{(T,w@l)\\}\cup\mathcal{Z})$ and
$\mathcal{W}^{\prime}=(\mathcal{H},\\{(\overline{T},-1\cdot
w@l)\\}\cup\mathcal{Z})$. The argument for the case of min-optimal models
follows the same lines.

To prove that the optimal models of $\mathcal{W}$ coincide with the optimal
models of $\mathcal{W}^{\prime}$, it is sufficient to show that for any level
$l^{\prime}$ in ${\lambda({\mathcal{W}})}$, $l^{\prime}$-optimal models of
$\mathcal{W}$ coincide with $l^{\prime}$-optimal models of
$\mathcal{W}^{\prime}$. We first note that models of $\mathcal{W}$ and
${\mathcal{W}^{\prime}}$ coincide. By induction on levels of $\mathcal{W}$.

Base case. $l^{\prime}$ is the greatest level.

Case 1. $l^{\prime}\neq l$. The case is trivial as
$\mathcal{W}_{l^{\prime}}={\mathcal{W}^{\prime}}_{l^{\prime}}$.

Case 2. $l^{\prime}=l$. A model $I^{*}$ of $\mathcal{W}$ (or
$\mathcal{W}^{\prime}$) is $l$-optimal model of $\mathcal{W}$ if and only if
$I^{*}$ satisfies equation (27), where $I$ ranges over models of
$\mathcal{W}$. In other words, for any model $I$ of $\mathcal{W}$ (or
$\mathcal{W}^{\prime}$) the inequality

$\displaystyle{{\sum_{B\in\mathcal{W}_{l}}{[{I^{*}\models
B}]}}\geq{\sum_{B\in\mathcal{W}_{l}}{[{I\models B}]}}}.$ (35)

holds. This inequality can be equivalently rewritten as

$\begin{array}[]{l}\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I^{*}\models
B}]}}+[{I^{*}\models\\{(T,w@l)\\}}]}\geq\\\
\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I\models
B}]}}+[{I\models\\{(T,w@l)\\}}]}.\end{array}$ (36)

Note that the following condition holds

$\mathcal{W}_{l}\setminus\\{(T,w@l)\\}=\mathcal{W}^{\prime}_{l}\setminus\\{(\overline{T},-1\cdot
w@l)\\}.$ (37)

We now illustrate that under all possible cases we conclude that inequality
(35), where $\mathcal{W}_{l}$ is replaced by $\mathcal{W}^{\prime}_{l}$, holds
for arbitrary model $I$ of $\mathcal{W}$ (or $\mathcal{W}^{\prime}$).
Consequently, $I^{*}$ satisfies equation (27), where $\mathcal{W}_{l}$ is
replaced by $\mathcal{W}^{\prime}_{l}$ and $I$ ranges over models of
$\mathcal{W}^{\prime}$. Thus, $I^{*}$ is $l$-optimal model of
$\mathcal{W}^{\prime}$. We also note that the same cases are applicable to
illustrate another direction. Namely, from the fact that $I^{*}$ satisfies
equation (27), where $\mathcal{W}_{l}$ is replaced by
$\mathcal{W}^{\prime}_{l}$ and $I$ ranges over models of
$\mathcal{W}^{\prime}$ we can conclude that $I^{*}$ satisfies equation (27)
where $I$ ranges over models of $\mathcal{W}$. To support this claim, the
arguments of the cases below can be read from bottom to top.

Case 2.1: $I^{*}\models\\{(T,w@l)\\}$ and $I\models\\{(T,w@l)\\}$. Or,
equivalently, $I^{*}\not\models\\{(\overline{T},-1\cdot w@l)\\}$ and
$I\not\models\\{(\overline{T},-1\cdot w@l)\\}$. Consequently,

$[{I^{*}\models\\{(\overline{T},-1\cdot
w@l)\\}}]=0=[{I\models\\{(\overline{T},-1\cdot w@l)\\}}].$ (38)

Inequality (36) can be rewritten as

$\begin{array}[]{l}\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I^{*}\models
B}]}}}+w\geq\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I\models
B}]}}+w}.\end{array}$

Consequently, the following inequality holds

$\begin{array}[]{l}\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I^{*}\models
B}]}}}\geq\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I\models
B}]}}}.\end{array}$

From this inequality, it immediately follows that the following holds

$\begin{array}[]{l}\displaystyle{{\sum_{B\in\mathcal{W}^{\prime}_{l},B\neq\\{(\overline{T},-1\cdot
w@l)\\}}{[{I^{*}\models B}]}}+[{I^{*}\models\\{(\overline{T},-1\cdot
w@l)\\}}]}\geq\\\
\displaystyle{{\sum_{B\in\mathcal{W}^{\prime}_{l},B\neq\\{(\overline{T},-1\cdot
w@l)\\}}{[{I\models B}]}}+[{I\models\\{(\overline{T},-1\cdot
w@l)\\}}]}.\end{array}$ (39)

as conditions (37) and (38) hold. By inequality (39), inequality (35) where
$\mathcal{W}_{l}$ is replaced by $\mathcal{W}^{\prime}_{l}$ holds.

Case 2.2: $I^{*}\models\\{(T,w@l)\\}$ and $I\not\models\\{(T,w@l)\\}$. Or,
equivalently, $I^{*}\not\models\\{(\overline{T},-1\cdot w@l)\\}$ and
$I\models\\{(\overline{T},-1\cdot w@l)\\}$. Consequently,

$[{I^{*}\models\\{(\overline{T},-1\cdot w@l)\\}}]=0\hbox{ and
}[{I\models\\{(\overline{T},-1\cdot w@l)\\}}]=-w.$ (40)

Inequality (36) can be rewritten as

$\begin{array}[]{l}\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I^{*}\models
B}]}}}+w\geq\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I\models
B}]}}}.\end{array}$

Consequently,

$\begin{array}[]{l}\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I^{*}\models
B}]}}}\geq\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I\models
B}]}}}-w.\end{array}$

From this inequality, it immediately follows that the inequality (39) holds as
conditions (37) and (40) hold. By inequality (39), inequality (35) where
$\mathcal{W}_{l}$ is replaced by $\mathcal{W}^{\prime}_{l}$ holds.

Case 2.3: $I^{*}\not\models\\{(T,w@l)\\}$ and $I\models\\{(T,w@l)\\}$. Or,
equivalently, $I^{*}\models\\{(\overline{T},-1\cdot w@l)\\}$ and
$I\not\models\\{(\overline{T},-1\cdot w@l)\\}$. Consequently,

$[{I^{*}\models\\{(\overline{T},-1\cdot w@l)\\}}]=-w\hbox{ and
}[{I\models\\{(\overline{T},-1\cdot w@l)\\}}]=0.$ (41)

Similarly to Case 2.2. we derive that from inequality (36) follows that

$\begin{array}[]{l}\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I^{*}\models
B}]}}-w}\geq\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I\models
B}]}}}.\end{array}$

From this inequality, it immediately follows that the inequality (39) holds as
conditions (37) and (41) hold. By inequality (39), inequality (35) where
$\mathcal{W}_{l}$ is replaced by $\mathcal{W}^{\prime}_{l}$ holds.

Case 2.4: $I^{*}\not\models\\{(T,w@l)\\}$ and $I\not\models\\{(T,w@l)\\}$. Or,
equivalently, $I^{*}\models\\{(\overline{T},-1\cdot w@l)\\}$ and
$I\models\\{(\overline{T},-1\cdot w@l)\\}$. Consequently,

$[{I^{*}\models\\{(\overline{T},-1\cdot
w@l)\\}}]=-w=[{I\models\\{(\overline{T},-1\cdot w@l)\\}}].$ (42)

We derive that from inequality (36) follows that

$\begin{array}[]{l}\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I^{*}\models
B}]}}}\geq\displaystyle{{\sum_{B\in\mathcal{W}_{l},B\neq\\{(T,w@l)\\}}{[{I\models
B}]}}}.\end{array}$

From this inequality, it immediately follows that the inequality (39) holds as
conditions (37) and (42) hold. By inequality (39), inequality (35) where
$\mathcal{W}_{l}$ is replaced by $\mathcal{W}^{\prime}_{l}$ holds.

Inductive case argument follows similar lines.

######  Proof 8.12 (Proof of Proposition 18).

We focus on the claim of identical optimal models of $\mathcal{W}$ and
$\mathcal{W}^{1}$ (the claim about min-optimal follows the same lines). We
first note that models of $\mathcal{W}$ and $\mathcal{W}^{1}$ are identical.

Recall Definition 8. It is easy to see that our claim follows in case when for
any pair $I$ and $I^{\prime}$ of models of $\mathcal{W}$ (or
$\mathcal{W}^{1}$), $I^{\prime}$ max-dominates $I$ in $\mathcal{W}$ if and
only if $I^{\prime}$ max-dominates $I$ in $\mathcal{W}^{\prime}$. Take $n$
denote a number of levels in $\mathcal{W}$.

Right-to-left. Assume that $I^{\prime}$ max-dominates $I$ in $\mathcal{W}$.
Per Definition 8, there exists a level $l\in{\lambda({\mathcal{W}})}$ such
that following conditions are satisfied:

  1. 1.

for any level $l^{\prime}>l$ the following equality holds

$\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I\models
B}]}}=\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I^{\prime}\models
B}]}}$

  2. 2.

the following inequality holds for level $l$

$\displaystyle{\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}}>\displaystyle{\sum_{B\in\mathcal{W}_{l}}{[{I\models B}]}}$ (43)

In the left-to-right direction of the proof we refer to the text in italics as
max-dominating condition.

The goal is to illustrate that the following inequality holds

$\displaystyle{\sum_{B\in\mathcal{W}^{1}}{[{I^{\prime}\models
B}]}}>\displaystyle{\sum_{B\in\mathcal{W}^{1}}{[{I\models B}]}},$ (44)

which translates into the fact that $I^{\prime}$ max-dominates $I$ in
$\mathcal{W}^{1}$.

We will now write two chains of inequalities for LHS and RHS expressions of
(44) that support the claim of condition (44). Note how the last element of
each chain amounts to the same expression. After every chain we provide
explanations supporting their less trivial transformations.

The first chain follows

$\begin{array}[]{r}\displaystyle{\sum_{B\in\mathcal{W}^{1}}{[{I^{\prime}\models
B}]}}=\\\ \displaystyle{\sum_{1\leq
i\leq{n}}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}}=\\\ \displaystyle{\sum_{1\leq
i<{l}}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}+\sum_{l<i\leq
n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{{\mathbf{I}^{\prime}}\models
B}]}\big{)}}}=\\\ \displaystyle{\sum_{1\leq
i<{l}}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}+\sum_{l<i\leq
n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{{\mathbf{I}}\models
B}]}\big{)}}}\geq\\\ \displaystyle{\sum_{1\leq i<{l}}{\big{(}f_{i}\cdot
0\big{)}}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}+\sum_{l<i\leq n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}}=\\\
\displaystyle{f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{{\mathbf{I}^{\prime}}\models
B}]}+\sum_{l<i\leq n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}}\geq\\\
\displaystyle{f_{l}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{{\mathbf{I}}\models
B}]}+\sum_{l<i\leq n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}}>\\\
\displaystyle{-1+f_{l}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{{\mathbf{I}}\models
B}]}+\sum_{l<i\leq n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}}\end{array}$

The third equality in the chain is due to Condition 1. The appearance of the
first inequality in the chain is due to the fact that

$\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models B}]}\geq 0$

as $0$ is “the most pessimistic” case for the “cost” of w-conditions at the
$i$-th level, when model $I$ does not satisfy any of the respective
w-conditions. The appearance of the second inequality in the chain is due to
the observation that from the condition (43) it follows that

$\begin{array}[]{clc}\displaystyle{\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}}&\geq&\displaystyle{\sum_{B\in\mathcal{W}_{l}}{[{I\models B}]}}+1\\\
f_{l}\cdot\displaystyle{\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}}&\geq&\displaystyle{f_{l}\cdot\big{(}\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}}+1\big{)}\\\
f_{l}\cdot\displaystyle{\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}}&\geq&\displaystyle{f_{l}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}}.\end{array}$

The second chain follows

$\begin{array}[]{r}\displaystyle{\sum_{B\in\mathcal{W}^{1}}{[{I\models
B}]}}=\\\ \displaystyle{\sum_{1\leq
i<{l}}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}+\sum_{l<i\leq n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}\leq\\\ \displaystyle{\sum_{1\leq
i<{l}}{\big{(}f_{i}\cdot(M_{i}-1)\big{)}}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}+\sum_{l<i\leq n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}}=\\\ \displaystyle{M_{1}-1+M_{1}\cdot
M_{2}-M_{1}+\dots+M_{1}\cdot...\cdot M_{l-1}-M_{1}\cdot...\cdot M_{l-2}+}\\\
\displaystyle{f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}+\sum_{l<i\leq n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}}=\\\ \displaystyle{-1+M_{1}\cdot...\cdot
M_{l-1}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I\models B}]}+\sum_{l<i\leq
n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models B}]}\big{)}}}=\\\
\displaystyle{-1+f_{l}+f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I\models
B}]}+\sum_{l<i\leq n}{\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}}\end{array}$

The appearance of the inequality in the chain above is due to the fact that

$\sum_{B\in\mathcal{W}_{i}}{[{I\models B}]}\leq(M_{i}-1)$

as $M_{i}$ accounts for the sum, incremented by one, of all the weights in
w-conditions of $\mathcal{W}_{i}$, which is “the most optimistic” case for the
“cost” of w-conditions at the $i$-th level when model $I$ satisfies all of the
respective w-conditions.

Left-to-right. Assume that $I$ max-dominates $I^{\prime}$ in
$\mathcal{W}^{1}$. Per Definition 8, inequality (44) holds.

The goal is to illustrate that max-dominating condition (see right-to-left
direction) holds, which translates into the fact that $I^{\prime}$ max-
dominates $I$ in $\mathcal{W}$. From inequality (44) we derive that

$\displaystyle{\sum_{1\leq
i\leq{n}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}>\displaystyle{\sum_{1\leq
i\leq{n}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models B}]}\big{)}}.$
(45)

We now show that there is $l$ among $1..n$ such that (i)

$\displaystyle{f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I^{\prime}\models
B}]}}>\displaystyle{f_{l}\cdot\sum_{B\in\mathcal{W}_{l}}{[{I\models B}]}}$

holds and (ii) for any $l^{\prime}>l$,

$\displaystyle{f_{l^{\prime}}\cdot\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I^{\prime}\models
B}]}}=\displaystyle{f_{l^{\prime}}\cdot\sum_{B\in\mathcal{W}_{l^{\prime}}}{[{I\models
B}]}}.$ (46)

With that max-dominating condition immediately follows.

By contradiction. Assume no such level $l$ exists such that both conditions
(i) and (ii) hold.

Case 1: Assume there is no level $l$ for which condition (i) holds. This
immediately contradicts assumption (45).

Case 2: There is $l$ among $1..n$ such that (i) holds. Take $l$ to be the
greatest level among $1..n$ for which (i) holds. Assume that (ii) does not
hold. Consequently, there is $l^{\prime\prime}>l$ such that

$\displaystyle{f_{l^{\prime\prime}}\cdot\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I^{\prime}\models
B}]}}<\displaystyle{f_{l^{\prime\prime}}\cdot\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]}}.$ (47)

Take $l^{\prime\prime}$ to be the greatest level with such property.
(Consequently, for any level $l^{\prime}>l^{\prime\prime}$ equality (46)
holds.) We now illustrate that from this fact the inequality

$\displaystyle{\sum_{1\leq
i\leq{n}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}<\displaystyle{\sum_{1\leq
i\leq{n}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models B}]}\big{)}}.$
(48)

follows, which contradicts assumption (45). We now write two chains of
inequalities for LHS and RHS expressions of (48) to support this claim. After
every chain we provide explanations supporting their less trivial
transformations. The first chain follows

$\begin{array}[]{l}\displaystyle{\sum_{1\leq
i\leq{n}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}=\\\ \displaystyle{\sum_{1\leq
i\leq{l^{\prime\prime}}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}=\\\ \displaystyle{\sum_{1\leq
i\leq{l^{\prime\prime}-1}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}+f_{l^{\prime\prime}}\cdot\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I^{\prime}\models
B}]}\leq\\\ \displaystyle{\sum_{1\leq
i\leq{l^{\prime\prime}-1}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I^{\prime}\models
B}]}\big{)}}+f_{l^{\prime\prime}}\cdot(\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]}-1)\leq\\\ \displaystyle{\sum_{1\leq
i\leq{l^{\prime\prime}-1}}{\big{(}f_{i}\cdot(M_{i}-1)\big{)}}+f_{l^{\prime\prime}}\cdot(\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]}-1)}=\\\
\displaystyle{-1+f_{l^{\prime\prime}}\cdot\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]}}\end{array}$

The first equality is due to the choice of $l^{\prime\prime}$ so that for any
level $l^{\prime}>l^{\prime\prime}$ equality (46) holds. The first inequality
is due to the observation that from inequality (47) the following conditions
follow immediately

$\begin{array}[]{l}\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I^{\prime}\models
B}]}}<\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]}}.\\\
\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I^{\prime}\models
B}]}}\leq\displaystyle{\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]}}-1.\\\ \end{array}$

The second inequality and the last equality follow the reasoning of the second
chain presented in right-to-left direction.

The second chain follows

$\begin{array}[]{l}\displaystyle{\sum_{1\leq
i\leq{n}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}=\\\ \displaystyle{\sum_{1\leq
i\leq{l^{\prime\prime}}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}=\\\ \displaystyle{\sum_{1\leq
i\leq{l^{\prime\prime}-1}}\big{(}f_{i}\cdot\sum_{B\in\mathcal{W}_{i}}{[{I\models
B}]}\big{)}}+f_{l^{\prime\prime}}\cdot\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]}\geq\\\
\displaystyle{f_{l^{\prime\prime}}\cdot(\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]})}>\\\
\displaystyle{-1+f_{l^{\prime\prime}}\cdot(\sum_{B\in\mathcal{W}_{l^{\prime\prime}}}{[{I\models
B}]})}\end{array}$

##  9 Conclusions

We proposed the extension of abstract modular systems to weighted systems in a
way that modern approaches to optimizations stemming from a variety of
different logic-based formalisms can be studied in unified terminological ways
so that their differences and similarities become clear not only on intuitive
but also formal level.

In this article we utilize the presented weighted systems as an abstraction of
search-optimization problems and capture such formalisms as MaxSAT and ASP-WC
by illustrating that these can be seen as instances of weighted systems. We
present multiple general equivalence transformations, which include
interchangeability of logic modules having the same models, preservation of
optimal and min-optimal models when weighted conditions yielding the same sum
for all models are eliminated, and convertibility between optimal and min-
optimal models by multiplying all weights with $-1$. Moreover, transformations
to eliminate either negative or positive weights, map several levels to a
single level by scaling up weights, and turn ASP-WC programs into MaxSAT are
developed. Some similar transformations/normalizations were described as early
as 2002 by Simons et al., and later by Alviano, (2018) in the context of ASP-
WC. Here, they are lifted into an abstract settings allowing us the
application of the results within different frameworks. Proofs for all of the
stated theoretical results are provided.

We trust that the proposed unifying framework of w-systems will allow
developers of distinct automated paradigms to better grasp similarities and
differences of the kind of optimization criteria their paradigms support. In
practice, translational approaches are popular in devising solvers. These
approaches rely on the relation between automated reasoning paradigms and
rather than devising a unique search algorithm for a paradigm of interest
propose a translation to another framework so that the solvers for that
frameworks can be of use. This work is a stepping stone towards extending
these translational approaches with the support for optimization statements.
In particular, an immediate and an intuitive future work direction is
extending a translational based answer set solver cmodels with capabilities to
process optimization statements by enabling it to interface with a
MaxSAT/MinSAT solver in place of a SAT solver. The formal results of this
paper support the validity of this approach (see Proposition 19 and 20). It is
also apparent how min-one solvers can be used for finding solutions to min-
one-asp problems introduced here.

In addition, this work served a role of a spring board for a unifying
framework studied in (Lierler, 2022) that looked into formalisms which mix
propositional and non-propositional (e.g., integer) variables in their
languages and optimization statements. This supports the claim of explanatory
and simplifying utility of this paper.

Acknowledgments We would like to acknowledge Mario Alviano, Martin Gebser,
Jorge Fandinno, Torsten Schaub, Miroslaw Truszczynski, and Da Shen for
valuable discussions related to this work. The project was partially supported
by NSF grant 1707371.

## References

  * Alviano, (2018) Alviano, M. 2018\.  Algorithms for solving optimization problems in answer set programming.  Intelligenza Artificiale, 12, 1–14.
  * Alviano et al., (2020) Alviano, M., Dodaro, C., Marques-Silva, J., and Ricca, F. 2020\.  Optimum stable model search: algorithms and implementation.  Journal of Logic and Computation, 30, 4, 863–897.
  * Alviano et al., (2018) Alviano, M., Romero, J., and Schaub, T. Preference relations by approximation.  In KR 2018, pp. 2–11. AAAI Press.
  * Andres et al., (2012) Andres, B., Kaufmann, B., Matheis, O., and Schaub, T. Unsatisfiability-based optimization in clasp.  In Dovier, A. and Costa, V. S., editors, Technical Communications of the 28th International Conference on Logic Programming (ICLP’12) 2012, volume 17 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 211–221, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * Argelich et al., (2008) Argelich, J., Li, C. M., Manyà, F., and Planes, J. 2008\.  The first and second max-sat evaluations.  J. Satisf. Boolean Model. Comput., 4, 251–278.
  * Argelich et al., (2009) Argelich, J., Lynce, I., and Marques-Silva, J. On solving boolean multilevel optimization problems.  In Proceedings of the 21st International Jont Conference on Artifical Intelligence 2009, IJCAI’09, 393–398, San Francisco, CA, USA. Morgan Kaufmann Publishers Inc.
  * Bailleux and Marquis, (2006) Bailleux, O. and Marquis, P. 2006\.  Some computational aspects of distance-sat.  J. Autom. Reason., 37, 4, 231–260.
  * Brewka et al., (2015) Brewka, G., Delgrande, J. P., Romero, J., and Schaub, T. asprin: Customizing answer set preferences without a headache.  In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA. 2015, pp. 1467–1474.
  * Brewka and Eiter, (2007) Brewka, G. and Eiter, T. Equilibria in heterogeneous nonmonotonic multi-context systems.  In Proceedings of National Conference on Artificial Intelligence, AAAI 2007 2007, pp. 385–390.
  * Calimeri et al., (2020) Calimeri, F., Faber, W., Gebser, M., Ianni, G., Kaminski, R., Krennwallner, T., Leone, N., Ricca, F., Schaub, T., and et al. 2020\.  ASP-Core-2 input language format.  Theory and Practice of Logic Programming, 20, 2, 294–309.
  * Clark, (1978) Clark, K. Negation as failure.  In Gallaire, H. and Minker, J., editors, Logic and Data Bases 1978, pp. 293–322. Plenum Press, New York.
  * Creignou et al., (2001) Creignou, N., Khanna, S., and Sudan, M. 2001\.  Complexity Classifications of Boolean Constraint Satisfaction Problems.  Society for Industrial and Applied Mathematics, USA.
  * Davis et al., (1962) Davis, M., Logemann, G., and Loveland, D. 1962\.  A machine program for theorem proving.  Communications of the ACM, 5(7), 394–397.
  * Di Rosa and Giunchiglia, (2013) Di Rosa, E. and Giunchiglia, E. 2013\.  Combining approaches for solving satisfiability problems with qualitative preferences.  AI Commun., 26, 4, 395–408.
  * Ensan and Ternovska, (2019) Ensan, A. and Ternovska, E. A language-independent framework for reasoning about preferences for declarative problem solving.  In Herzig, A. and Popescu, A., editors, Frontiers of Combining Systems 2019, pp. 57–73, Cham. Springer International Publishing.
  * Ferraris, (2005) Ferraris, P. Answer sets for propositional theories.  In International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR) 2005, pp. 119–131.
  * Fu and Malik, (2006) Fu, Z. and Malik, S. On solving the partial max-sat problem.  In Biere, A. and Gomes, C. P., editors, Theory and Applications of Satisfiability Testing - SAT 2006 2006, pp. 252–265, Berlin, Heidelberg. Springer Berlin Heidelberg.
  * Giunchiglia et al., (2006) Giunchiglia, E., Lierler, Y., and Maratea, M. 2006\.  Answer set programming based on propositional satisfiability.  Journal of Automated Reasoning, 36, 345–377.
  * Giunchiglia and Maratea, (2006) Giunchiglia, E. and Maratea, M. Solving optimization problems with dll.  In 2006 Conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 – September 1, 2006, Riva Del Garda, Italy 2006, 377–381, NLD. IOS Press.
  * Janhunen, (2006) Janhunen, T. 2006\.  Some (in)translatability results for normal logic programs and propositional theories.  Journal of Applied Non-Classical Logics,, 35–86.
  * Li et al., (2011) Li, C.-M., Zhu, Z., Manyà, F., and Simon, L. Minimum satisfiability and its applications.  In Twenty-Second International Joint Conference on Artificial Intelligence - Volume Volume One 2011, IJCAI’11, 605–610. AAAI Press.
  * Lierler, (2017) Lierler, Y. 2017\.  What is answer set programming to propositional satisfiability.  Constraints, 22, 307–337.
  * Lierler, (2021) Lierler, Y. An abstract view on optimizations in sat and asp.  In 17th European Conference on Logics in Artificial Intelligence (JELIA) 2021\.
  * Lierler, (2022) Lierler, Y. 2022\.  Unifying framework for optimizations in non-boolean formalisms.  Theory and Practice of Logic Programming,, 1–33.
  * Lierler and Truszczynski, (2015) Lierler, Y. and Truszczynski, M. An abstract view on modularity in knowledge representation.  In Proceedings of the AAAI Conference on Artificial Intelligence 2015\.
  * Lifschitz et al., (1999) Lifschitz, V., Tang, L. R., and Turner, H. 1999\.  Nested expressions in logic programs.  Annals of Mathematics and Artificial Intelligence, 25, 369–389.
  * Lin and Zhao, (2002) Lin, F. and Zhao, Y. ASSAT: Computing answer sets of a logic program by SAT solvers.  In Proceedings of National Conference on Artificial Intelligence (AAAI) 2002, pp. 112–117. MIT Press.
  * Mitchell, (2005) Mitchell, D. G. A SAT solver primer.  In EATCS Bulletin (The Logic in Computer Science Column) 2005, volume 85, pp. 112–133.
  * Nieuwenhuis and Oliveras, (2006) Nieuwenhuis, R. and Oliveras, A. On SAT modulo theories and optimization problems.  In Biere, A. and Gomes, C. P., editors, Theory and Applications of Satisfiability Testing - SAT 2006 2006, pp. 156–169, Berlin, Heidelberg. Springer Berlin Heidelberg.
  * Robinson et al., (2010) Robinson, N., Gretton, C., Pham, D.-N., and Sattar, A. Cost-optimal planning using weighted MaxSAT.  In ICAPS 2010 Workshop on Constraint Satisfaction Techniques for Planning and Scheduling (COPLAS10) 2010\.
  * Simons et al., (2002) Simons, P., Niemelä, I., and Soininen, T. 2002\.  Extending and implementing the stable model semantics.  Artificial Intelligence, 138, 181–234.