2 Review: Abstract logic; logic programs

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. This definition ignores any syntactic details behind the concepts of a formula and a theory. A vocabulary is 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$ .

1. 1. $L_{\mathcal{L}}$ is a language (the language of the logic ${\mathcal{L}}$ ),

2. 2. $\sigma_{\mathcal{L}}$ is a vocabulary (the vocabulary of the logic ${\mathcal{L}}$ ),

3. 3. $\mathit{sem}_{\mathcal{L}}:2^{L_{\mathcal{L}}} \rightarrow 2^{{\mathit{Int}}(\sigma_{\mathcal{L}})}$ is a function assigning collections of interpretations to theories in $L_{\mathcal{L}}$ (the 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.

Literals over a vocabulary $\sigma$ are expressions a and $\neg a$ , where a is an atom from $\sigma$ . A (logic) rule over $\sigma$ is of the form

(2) \begin{equation}\begin{array}{l}a_0\leftarrow a_1,\dotsc, a_\ell,\ not\ a_{\ell+1},\dotsc,\ not\ a_m, \end{array}\end{equation}

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$ . A logic program over $\sigma$ is a set of rules over $\sigma$ . The expression $a_0$ is the head of the rule. The expression on the right hand side of the arrow is the body. We write $\mathit{hd}(\Pi)$ for the set of nonempty heads of rules in logic program $\Pi$ . It is customary for a given vocabulary $\sigma$ , to identify a set X of atoms over $\sigma$ with (i) the complete and consistent set of literals over $\sigma$ constructed as $X\cup\{\neg a \mid a\in\sigma\setminus X\}$ , and with (ii) an assignment function that assigns the truth value true to every atom in X and false to every atom in $\sigma\setminus X$ . In the sequel, we may refer to sets of atoms as assignments and the other way around following this convention. We say that a set X of atoms satisfies rule (2), if X satisfies the propositional formula

\begin{equation*}a_1\wedge\dotsc\wedge a_\ell\wedge\ \neg a_{\ell+1}\wedge\dotsc\wedge\ \neg a_m\rightarrow a_0.\end{equation*}

The reduct $\Pi^X$ of a program $\Pi$ relative to a set X of atoms is obtained by first removing all rules (2) 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

\begin{equation*}a_0\leftarrow a_1,\ldots, a_\ell.\end{equation*}

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. Reference Lifschitz, Tang and Turner1999). For example, program

(3) \begin{equation}\begin{array}{l}a\leftarrow not\ b\\b\leftarrow not\ a\end{array}\end{equation}

has two answer sets $\{a\}$ and $\{b\}$ .

A set X of atoms from a vocabulary $\sigma$ is an input answer set of a logic program $\Pi$ over $\sigma$ if X is an answer set of the program $\Pi\cup (X\setminus \mathit{hd}(\Pi))$ (Lierler and Truszczynski Reference Lierler and Truszczynski2011). For example, if we consider program (3) as a program over vocabulary $\{a,b,c\}$ , then program (3) has four input answer sets: $\{a\}$ , $\{b\}$ , $\{a,c\}$ , $\{b,c\}$ .

Brewka and Eiter (Reference Brewka and Eiter2007) showed that their 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 F over $\sigma$ ,

captures propositional logic. We call this logic ${\mathcal{L}}$ the pl-logic and theories (that we later call modules) in the pl-logic, pl-theories/modules. If we restrict elements of L to be clauses, then we call ${\mathcal{L}}$ a sat-logic.

Similarly, 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/input answer sets of $\Pi$ over $\sigma$ ,

captures logic programs under the answer set/input answer set semantics. We call these logics the lp-logic and ilp-logic, respectively, and theories/modules in these logics, lp-theories/modules and ilp-theories/modules.

3 Extended logic for CAS programs and SMT formulas

Constraint Satisfaction Problems and Constraint Answer Set Programs A pair [V, D], where V is a set of variables and D is a set of values for variables in V or the domain for V, is called a specification. A constraint over specification [V, D] is a pair $\langle t,\mathbb{R} \rangle$ , where t is a tuple of some (possibly all) variables from V and $\mathbb{R}$ is a relation on D of the same arity as t. A collection of constraints over [V, D] is a constraint satisfaction problem (CSP) over [V, D]. An evaluation of V is a function assigning to every variable in V a value from D. An evaluation $\nu$ satisfies a constraint $\langle (x_1,\ldots,x_n), \mathbb{R} \rangle$ (or is a solution of this constraint) if $(\nu(x_1),\ldots, \nu(x_n)) \in \mathbb{R}$ . An evaluation satisfies (or is a solution to) a CSP if it satisfies every constraint of the problem. Let $c=\langle t,\mathbb{R}\rangle$ be a constraint and D the domain of its variables. Let k denote the arity of t. The constraint $\overline{c}=\langle t,D^k\setminus \mathbb{R}\rangle$ is the complement (or dual) of c. Clearly, an evaluation of variables in t satisfies c if and only if it does not satisfy $\overline{c}$ . Frequently, constraints are stated implicitly without a reference to explicit relation. In particular, constraints over integers or reals are often formulated by means of common arithmetic relation symbols.

When we refer to some class of constraints we assume that all of its members are over the same specification. We call a function from a vocabulary $\sigma$ to a class $\mathcal{C}$ of constraints a $({\sigma}, {\mathcal{C}})$ -denotation. From now on given a vocabulary $\sigma$ , we assume that some of its atoms are marked as irregular/constraint atoms. We utilize subscripts r and c to refer to regular atoms – atoms not marked as constraint ones – and constraint atoms, respectively. Thus, given vocabulary $\sigma$ : $\sigma_r$ forms the subset of $\sigma$ containing all regular atoms and $\sigma_c$ forms the subset of $\sigma$ containing all constraint atoms.

We present the definition of answer sets for CAS programs as proposed by Lierler (Reference Lierler2014) using the notation of this paper.

• $X\cap\mathit{At}(P)_r\subseteq\mathit{hd}(P)$ ,

• X is an input answer set of P, and

• the following CSP has a solution ^{Footnote 1}

  (4) \begin{equation}\begin{array}{l}\{\gamma(a)\mid a\in X\cap\mathit{At}(P)_c\}\cup \{\overline{\gamma(a)}\mid a\in \mathit{At}(P)_c\setminus X\}.\end{array}\end{equation}

A pair $(X,\nu)$ is an extended answer set of CAS program P if X is an answer set of P and $\nu$ is a solution to (4).

Example 2 Consider specification $s_1$ and a class $\mathcal{C}_1$ of constraints consisting of constraint $c_1$ and its complement, where $s_1$ and $c_1$ are defined in Example 1. Take vocabulary $\sigma_1$ contain two regular atoms a,b and an irregular atom $|x\neq 0|$ ; and assume $({\sigma_1}_c,\mathcal{C}_1)$ -denotation that maps irregular atom $|x\neq 0|$ to constraint $c_1$ . Let $P_1$ be CAS program over $\sigma_1$ , $\mathcal{C}_1$ , and $({\sigma_1}_c,\mathcal{C}_1)$ -denotation consisting of rules in (3) and rule

\begin{equation*}\leftarrow a, |x\neq 0|.\end{equation*}

Take $\nu_0$ , $\nu_1$ , $\nu_2$ be evaluations assigning x to 0, 1, and 2, respectively. The extended answer sets of $P_1$ are $(\{a\},\nu_0)$ , $(\{b\},\nu_0)$ , $(\{b,|x\neq 0|\},\nu_1)$ , $(\{b,|x\neq 0|\},\nu_2)$ .

Lierler and Truszczynski (Reference Lierler and Truszczynski2015) introduced abstract modular systems based of conglomerations of theories over various logics. They illustrated that such systems can be used to capture CAS programs: in particular, they may capture answer sets of a given CAS program. Here, we introduce an extended notion of a logic so that we may speak of abstract systems capturing the meaning of CAS programs in terms of extended answer sets. We then show that the concept of extended logic is helpful in capturing problems expressed as satisfiability modulo theories (SMT).

Extended Logic For a vocabulary $\sigma$ , set V of variables, and domain D, we call a pair $(I,\nu)$ , where I is an interpretation over $\sigma$ and $\nu$ is an evaluation from V to D, an extended interpretation over $\sigma$ , V, D. We write ${\mathit{Int}}(\sigma,V,D)$ for the family of all extended interpretations over $\sigma$ , V, D.

Definition 3 (Extended Logic) An extended logic or e-logic ${\mathcal{L}}+$ is a tuple

\begin{equation*}(L_{{\mathcal{L}}+},\sigma_{{\mathcal{L}}+},\Delta_{{\mathcal{L}}+}, \Upsilon_{{\mathcal{L}}+},\mathit{sem}_{{\mathcal{L}}+}),\end{equation*}

where

1. 1. $L_{{\mathcal{L}}+}$ is a language

2. 2. $\sigma_{{\mathcal{L}}+}$ is a vocabulary

3. 3. $\Delta_{{\mathcal{L}}+}$ is a domain – a set of values – (the domain of the logic ${\mathcal{L}}+$ )

4. 4. $\Upsilon_{{\mathcal{L}}+}$ is a set of variables over domain $\Delta_{{\mathcal{L}}+}$ (the variables of the logic ${\mathcal{L}}+$ )

5. 5. $\mathit{sem}_{{\mathcal{L}}+}$ : is a function assigning collections of extended interpretations $(I,\nu)$ to theories in $L_{{\mathcal{L}}+}$ , where $(I,\nu)$ is an element in ${\mathit{Int}}(\sigma_{{\mathcal{L}}+},\Upsilon_{{\mathcal{L}}+},\Delta_{{\mathcal{L}}+})$ .

In the sequel, we will default to naming the members of the tuples of extended logic ${\mathcal{L}}+$ as in this definition. It is easy to see that an extended logic generalizes the concept of a logic: we can identify any logic ${\mathcal{L}}=(L_{{\mathcal{L}}},\sigma_{{\mathcal{L}}},\mathit{sem}_{{\mathcal{L}}})$ with its extended counterpart ${\mathcal{L}}+=(L_{{\mathcal{L}}},\sigma_{{\mathcal{L}}},\emptyset, \emptyset,\mathit{sem}_{{\mathcal{L}}})$ , where $\mathit{sem}_{{\mathcal{L}}}$ in ${\mathcal{L}}+$ is identified with a function that maps theories into pairs whose first element is an interpretation of $\mathit{sem}_{{\mathcal{L}}}$ in ${\mathcal{L}}$ application and the second element is empty function.

We now illustrate that extended logic captures CAS programs under extended answer set semantics. Then, we show how SMT formulas are captured by this formalism. Indeed, provided class $\mathcal{C}$ of constraints over specification [V, D] and a $({\sigma_c}, {\mathcal{C}})$ -denotation, the extended logic $(L,\sigma,D,V,\mathit{sem})$ , where

1. 1. L is the set of CAS rules over vocabulary $\sigma$ ;

2. 2. $\mathit{sem}(P)$ , for a theory $P\subseteq L$ , over class $\mathcal{C}$ of constraints and $({\sigma_c}, {\mathcal{C}})$ -denotation, is the set of extended answer sets of P,

captures CAS programs under extended answer set semantics. We call this logic CAS logic.

Satisfiability Modulo Theories as Theories in Extended Logic Here we state the definition of a SMT formula (Barrett and Tinelli, Reference Barrett and Tinelli2014) following the lines by Lierler and Susman (Reference Lierler and Susman2017) using terminology introduced in this work. An alternative name for SMT formulas could have been constraint formulas.

• X is a model of propositional classical logic theory ${\mathcal{F}}$ , and

• the CSP (4) with P replaced by ${\mathcal{F}}$ has a solution.

A pair $(X,\nu)$ is an extended model, denoted $(X,\nu)\models {\mathcal{F}}$ , if X is model of ${\mathcal{F}}$ and $\nu$ is a solution to (4) with P replaced by ${\mathcal{F}}$ .

SMT formulas can be captured by extended logic theories just as CAS programs. Provided class $\mathcal{C}$ of constraints over specification [V, D] and a $({\sigma_c}, {\mathcal{C}})$ -denotation, the extended logic $(L,\sigma,D,V,\mathit{sem})$ , where

1. 1. L is the set of propositional formulas over vocabulary $\sigma$ ;

2. 2. $\mathit{sem}({\mathcal{F}})$ , for a theory ${\mathcal{F}}\subseteq L$ over class $\mathcal{C}$ of constraints and $({\sigma_c}, {\mathcal{C}})$ -denotation, is the set of extended models of ${\mathcal{F}}$ ,

captures SMT formulas. We call this logic SMT-logic (over constraints $\mathcal{C}$ ). If we restrict elements of L to be conjunctions of literals

(5) \begin{equation} a_1\wedge\dotsc\wedge a_\ell\wedge\ \neg a_{\ell+1}\wedge\dotsc\wedge\ \neg a_m.\end{equation}

then we call this extended logic a Restricted SMT or RSMT-logic.

Example 3 Example 2 defines $\sigma_1$ , $\mathcal{C}_1$ , and $({\sigma_1}_c,\mathcal{C}_1)$ -denotation considered here. Let clauses

\begin{equation*}\{a\vee b,~\neg a,~\neg a\vee \neg |x\neq 0|\}\end{equation*}

over $\sigma_1$ , $\mathcal{C}_1$ , and $({\sigma_1}_c,\mathcal{C}_1)$ -denotation form an SMT-logic theory H. Recall how (i) Example 2 is a continuation of Example 1, where domain of variable x was specified as $\{0,1,2\}$ and (ii) valuations $\nu_0,\nu_1,\nu_2$ are chosen to assign x to 0, 1, 2, respectively. There are three extended interpretations that are extended models to the considered SMT-logic theory H:

\begin{equation*}(\{b\},\nu_0),~~ (\{b,|x\neq 0|\},\nu_1),~~ (\{b,|x\neq 0|\},\nu_2).\end{equation*}

Integer CSP as Extended Logic An integer expression has the form

\begin{equation*}b_1 x_1 +\cdots + b_n x_n,\end{equation*}

where $b_1,\dots,b_n$ are integers $\mathbb{Z}$ and $x_1,\dots,x_n$ are variables over $\mathbb{Z}$ . When $b_i=1$ ( $1\leq i\leq n$ ) we may omit it from the expression. We call a constraint integer when it is over specification whose domain is $\mathbb{Z}$ and is encoded implicitly via the form $e\bowtie k,$ where e is an integer expression, k is an integer, and $\bowtie$ belongs to $\{<,>,\leq,\geq,=,\neq\}$ . We call a CSP an integer constraint satisfaction problem when it is composed of integer constraints.

Integer CSPs can be captured by extended logic theories. Indeed, an extended logic $(L,\emptyset,\mathbb{Z},V,\mathit{sem})$ , where

1. 1. L is the set of integer constraints over $[{V}, {\mathbb{Z}}]$ ;

2. 2. $\mathit{sem}({\mathcal{F}})$ , for a theory ${\mathcal{F}}\subseteq L$ , is the set of pairs $(\emptyset,\nu)$ , where evaluation $\nu$ is a solution to ${\mathcal{F}}$ ,

captures integer CSPs. We call this logic an I-CSP-logic. If the domain of this extended logic is that of nonnegative integers $\mathbb{Z}^+$ then we call this logic a nonnegative I-CSP-logic.

4 Extended weighted abstract modular systems or EW-systems

Lierler and Truszczynski (Reference Lierler and Truszczynski2015) propose (model-based) abstract modular systems or AMS that allow us to construct heterogeneous systems based of “modules” stemming from a variety of logics. We now generalize their framework by incorporating the notion of an extended logic.

Let T be an extended ${\mathcal{L}}+$ -module. An extended interpretation $(I,\nu)$ over $\sigma_{{\mathcal{L}}+}$ , $\Delta_{{\mathcal{L}}+}$ , $\Upsilon_{{\mathcal{L}}+}$ is an extended model of T, whereas I is a model of T if $(I,\nu)\in\mathit{sem}_{{\mathcal{L}}+}(T)$ .

By $L_T$ , $\sigma_T$ , $\Delta_T$ , $\Upsilon_T$ , and $\mathit{sem}_T$ we refer to the elements $L_{{\mathcal{L}}+},\sigma_{{\mathcal{L}}+},\Delta_{{\mathcal{L}}+}, \Upsilon_{{\mathcal{L}}+},$ and $\mathit{sem}_{{\mathcal{L}}+}$ of module T logic ${\mathcal{L}}+$ , respectively. As before, we use words theory and modules interchangeably. Furthermore, for a theory/module in SMT-logic we often refer to these as SMT formulas. For a theory/module in CAS-logic we refer to it as a CAS 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 a set V of variables and an evaluation $\nu$ defined over some superset of V, by $\nu_{|V}$ we denote an evaluation over V constructed from $\nu$ so that $\nu_{|V}(v)=\nu(v)$ for any variable v in V. For example, let V be the set of variables $\{x,y\}$ , and evaluation $\nu$ defined over $\{x,y,z\}$ assigns x and y to 1 and variable z to 2. Evaluation $\nu_{|V}$ is defined on domain V and assigns both of its variables value 1.

We now generalize the notion of an extended model to vocabularies and evaluations that go beyond the one of a considered module in a straight forward manner. For an e-module T and an extended interpretation $(I,\nu)$ over $\sigma$ , V, D so that $\sigma_T\subseteq \sigma$ , $\Upsilon_T\subseteq V$ , $\Delta_T\subseteq D$ , we say that $(I,\nu)$ is an extended model of T, denoted $(I,\nu)\models T$ , if $(I_{|{\sigma_T}},\nu_{|\Upsilon_T})\in \mathit{sem}_T$ . We can generalize the concept of a model in a similar way.

We call extended logics $(L,\sigma,D, V,\mathit{sem})$ and $(L',\sigma',D', V',\mathit{sem}')$ (and, respectively e-modules in these logics) coherent if $D=D'$ , whenever $V\cap V'\neq \emptyset$ . In other words if e-logics are coherent and they share variables then the domains of these e-logics coincide.

• 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}}$ ,

• the union of the variables of the logics of the modules in ${\mathcal{H}}$ forms the set of variables of ${\mathcal{H}}$ , denoted by $\Upsilon_{\mathcal{H}}$ ,

• the union of the domains of the logics of the modules in ${\mathcal{H}}$ forms the domain of ${\mathcal{H}}$ , denoted by $\Delta_{\mathcal{H}}$ .

An extended interpretation $(I,\nu)$ over $\sigma_{\mathcal{H}}$ , $\Upsilon_{\mathcal{H}}$ , $\Delta_{\mathcal{H}}$ is an extended model of ${\mathcal{H}}$ whereas I is a model of ${\mathcal{H}}$ , when for every module $B\in{\mathcal{H}}$ , $(I,\nu)$ is an extended model of B. When an EAMS consists of a single module $\{F\}$ we identify it with module F itself. Just as the concept of an extended logic presented here is a generalization of logic by Brewka and Eiter, the concept of EAMS is a generalization of AMS by Lierler and Truszczynski (Reference Lierler and Truszczynski2015).

Extended W-systems In practice, we are frequently interested not only in identifying models of a given logical formulation of a problem (hard fragment), but also identifying models that are deemed optimal according to some criteria (soft fragment). Frequently, multi-level optimizations are of interest. Lierler and Truszczynski (Reference Lierler and Truszczynski2015) argued how AMS and, consequently, EAMS as its generalization are geared towards capturing heterogeneous solutions for formulating hard constraints. Lierler (Reference Lierler2021) used abstract modular systems to formulate a concept of w-systems that enable soft constraints. W-systems are adequate to capture the MaxSAT/MinSAT family of problems (Robinson et al. Reference Robinson, Gretton, Pham and Sattar2010) as well as logic programs with weak constraints (Alviano Reference Alviano2018). W-systems provide us with means of studying these distinct logic frameworks under a unified viewpoint.

• w is an integer,

• c is a function from variables in $\Upsilon_T$ to reals, and

• l is a positive integer.

We refer to integers l and w as levels and weights, respectively. We refer to function c as coefficients function.

Let B be an ew-condition $(T,w;{\bf c}@\ell)$ . Intuitively, by $\sigma_B$ , $\Delta_B$ , and $\Upsilon_B$ we refer to $\sigma_T$ , $\Delta_T$ , and $\Upsilon_T$ , respectively. Let $(I,\nu)\in {\mathit{Int}}(\sigma_T,\Upsilon_T,\Delta_T)$ be an extended interpretation; it is an extended model of B, denoted $(I,\nu)\models B$ , when $(I,\nu)$ is an extended model of T, also in this case I is called a model, denoted $I\models B$ .

The notion of an (extended) model for ew-condition is generalized to vocabularies and evaluations that go beyond the one of a considered ew-condition in a straight forward manner (as it was done earlier for the case of e-modules). For an extended interpretation $(I,\nu)$ over $\sigma$ , V, D so that $\sigma_B\subseteq \sigma$ , $\Upsilon_B\subseteq V$ , $\Delta_B\subseteq D$ , we say that $(I,\nu)$ is an extended model of ew-condition B, denoted $(I,\nu)\models B$ , if $(I_{|{\sigma_T}},\nu_{|\Upsilon_T})\models B$ . The concept of a model is generalized in a similar way.

Intuitively, the role of weights w in ew-condition $B=(T,w;{\bf c}@\ell)$ is to distinguish the quality of models/extended models of B given their propositional part; the role of the coefficient c is to distinguish the quality of extended models of B given their evaluation part. These intuitions become more apparent in the next definition, where we associate “cost” expressions with the models of ew-conditions. We elaborate more on these expressions after their definitions.

For an extended interpretation $(I,\nu)$ over $\sigma$ , V, D so that $\sigma_B\subseteq \sigma$ , $\Upsilon_B\subseteq V$ , $\Delta_B\subseteq D$ , a mapping $[{(I,\nu)\models B}]$ is defined as

(6) \begin{equation}[{(I,\nu)\models B}]=\begin{cases} \displaystyle{\sum_{x\in \Upsilon_B}{\nu(x)\cdot {\bf c}(x)}} &\hbox{when $(I,\nu)\models B$} \\ 0&\hbox{otherwise.}\end{cases}\end{equation}

For an interpretation I over $\sigma$ so that $\sigma_B\subseteq \sigma$ , a mapping $[{I\models B}]$ is defined as follows

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

We view expressions $[{(I,\nu)\models B}]$ and $[{I\models B}]$ as costs associated with two distinct parts of an (extended) interpretation of a considered ew-condition B. Indeed, the former expression accounts for “the quality” of an evaluation associated with an extended interpretation and utilizes the coefficient of ew-condition B to compute that. The later expression accounts for “the quality” of “logical/propositional part” of an interpretation by considering the weight of ew-condition B. It is easy to see that nonzero values for costs are associated only with (extended) interpretations that are also models. These cost expressions are used in formulating the definitions of optimal (extended) models of ew-systems defined next. These ew-systems take ew-conditions as the tool for distinguishing quality of their (extended) models. Formulas (6) and (7) are used within expressions (8) and (10) utilized in the definitions of optimal models and optimal extended models of ew-systems, respectively. In the sequel, Examples 4, 5, 6 illustrate the use of instances of cost expressions (6) and (7) within formulas (8) and (10).

Before introducing the key concept of this paper – ew-systems – we present a number of useful abbreviations. We identify ew-conditions of the form

• $(T,w;{\bf c}@1)$ with expressions $(T,w;{\bf c})$ : that is, when the level is missing it is considered to be 1.

• $(T,w;\emptyset@\ell)$ with expressions $(T,w@\ell)$ : that is, when the coefficients function is empty.

• $(T,w;{\bf c}@\ell)$ with expressions $(T,w@\ell)$ , when the coefficients function c assigns 0 to every element in its domain.

For example, (T,w) stands for ew-condition, whose level is 1 and whose coefficients function is either empty or assigns 0 to every element in its domain.

For a collection ${\mathcal{Z}}$ of ew-conditions, its vocabulary, denoted by $\sigma_{\mathcal{Z}}$ , its set of variables, denoted by $\Upsilon_{\mathcal{Z}}$ , its domain, denoted by $\Delta_{\mathcal{Z}}$ is defined following the lines of these concepts for EAMS. We say that ew-condition $(T,w;{\bf c}@\ell)$ is coherent with an EAMS ${\mathcal{H}}$ if

• $\sigma_T\subseteq\sigma_{\mathcal{H}}$ ,

• $\Upsilon_T\subseteq \Upsilon_{\mathcal{H}}$ ,

• given any module H in ${\mathcal{H}}$ , $\Delta_T=\Delta_H$ whenever $\Upsilon_T\cap \Upsilon_H\neq \emptyset$ .

Let ${\mathcal{W}}=({\mathcal{H}},{\mathcal{Z}})$ be an ew-system. The vocabulary of ${\mathcal{H}}$ forms the vocabulary of ${\mathcal{W}}$ , denoted by $\sigma_{\mathcal{W}}$ . Similarly, $\Upsilon_{\mathcal{W}}=\Upsilon_{\mathcal{H}}$ and $\Delta_{\mathcal{W}}=\Delta_{\mathcal{H}}$ . An extended interpretation $(I,\nu)$ in ${\mathit{Int}}(\sigma_{\mathcal{W}}, \Upsilon_{\mathcal{W}}, \Delta_{\mathcal{W}})$ is an extended model of ${\mathcal{W}}$ , whereas I is a model, if $(I,\nu)$ is an extended model of ${\mathcal{H}}$ .

For a level l, by ${\mathcal{W}}_l$ we denote the subset of ${\mathcal{Z}}$ that includes all ew-conditions whose level is l. By ${\lambda({{\mathcal{W}}})}$ , we denote the set $\{l\mid (T,w;{\bf c}@\ell)\in {\mathcal{Z}}\}$ of all levels associated with ew-system ${\mathcal{W}}$ . 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 10 (Optimal models of ew-systems) For level $l\in{\lambda({{\mathcal{W}}})}$ , a model $I^*$ of ew-system ${\mathcal{W}}$ is l-optimal if $I^*$ satisfies equation

(8) \begin{equation}I^*=\displaystyle{arg\max_{I} {\sum_{B\in{\mathcal{W}}_l}{ [{I\models B}]}}},\end{equation}

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 (8) (and occurrences of word optimal are replaced by min-optimal in the definition; we drop this remark from the later similar definitions).

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}}})}$ .

We now provide intuitions for subexpression

(9) \begin{equation} {\sum_{B\in{\mathcal{W}}_l}{ [{I\models B}]}}\end{equation}

of the formula (8). Given an interpretation I, formula (9) can be seen as a cost of this interpretation with respect to level l of ew-system ${\mathcal{W}}$ . This cost is computed by summing all the weights of the ew-conditions of ${\mathcal{W}}_l$ for which this interpretation I is a model. When ew-system ${\mathcal{W}}$ contains only ew-conditions of a single level then formula (9) equips us with the cost of the considered interpretation with respect to the overall system.

Definition 11 (Extended Optimal Models of Ew-systems) For level $l\in{\lambda({{\mathcal{W}}})}$ , an extended model $(I^*,\nu^*)$ of ew-system ${\mathcal{W}}$ is l-optimal if $(I^*,\nu^*)$ satisfies equation

(10) \begin{equation}(I^*,\nu^*)=\displaystyle{arg\max_{(I^*,\nu^*)} {\sum_{B\in{\mathcal{W}}_l}{ ([{I\models B}] + [{(I,\nu)\models B}])}}},\end{equation}

where

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

• $(I,\nu)$ ranges over ${l}^\uparrow$ -optimal extended models of ${\mathcal{W}}$ , otherwise.

We call a model l-min-optimal if max is replaced by min in the equation above. An extended model $(I^*,\nu^*)$ of ${\mathcal{W}}$ is optimal if $(I^*,\nu^*)$ is l-optimal model for every level l in ${\lambda({{\mathcal{W}}})}$ . An extended model $(I^*,\nu^*)$ of ${\mathcal{W}}$ is min-optimal if $(I^*,\nu^*)$ is l-min-optimal model for every level l in ${\lambda({{\mathcal{W}}})}$ .

We now provide intuitions for subexpression

(11) \begin{equation}\sum_{B\in{\mathcal{W}}_l}{ ([{I\models B}] + [{(I,\nu)\models B}])}\end{equation}

of the formula (10). Given an extended interpretation $(I,\nu)$ , formula (11) can be seen as a cost of this interpretation with respect to level l of ew-system ${\mathcal{W}}$ . This cost is computed by considering all the ew-conditions of ${\mathcal{W}}_l$ for which this extended interpretation is a model and summing all their weights together with the values provided by linear expression formed within cost expression provided at the first line of (6). When ew-system ${\mathcal{W}}$ contains only ew-conditions of a single level then formula (11) equips us with the cost of the considered extended interpretation with respect to the overall system.

If we compare the notion of a optimal/min-optimal model versus a optimal/min-optimal extended model then the former does not take into account the numeric values associated with evaluations corresponding to extended models associated with the considered model; whereas the latter combines the quality of both parts of extended model.

Lierler (Reference Lierler2022) noted that the definition of optimal models in terms of “ $arg\max$ ”-equation comes from the traditions of literature related to MaxSAT problem. In answer set (logic) programming community, the conditions on optimality of answer sets is stated in terms of “domination” relation. Here we follow the steps by Lierler (Reference Lierler2022) and provide an alternative definition to optimal models of ew-systems in terms of domination.

1. 1. for any level $l'>l$ the following equality holds

   \begin{equation*}\displaystyle{ \sum_{B\in{\mathcal{W}}_{l'}}{ [{I\models B}]}}=\displaystyle{ \sum_{B\in{\mathcal{W}}_{l'}}{ [{I'\models B}]}}\end{equation*}

2. 2. the following inequality holds for level l

   \begin{equation*}\displaystyle{ \sum_{B\in{\mathcal{W}}_l}{ [{I'\models B}]}}<\displaystyle{ \sum_{B\in{\mathcal{W}}_l}{ [{I\models B}]}}\end{equation*}

Model I’ 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’ of ${\mathcal{W}}$ that max-dominates $I^*$ . A model $I^*$ of ${\mathcal{W}}$ is min-optimal if there is no model I’ of ${\mathcal{W}}$ that min-dominates $I^*$ .

1. 1. for any level $l'>l$ the following equality holds

   \begin{equation*}\displaystyle{{\sum_{B\in{\mathcal{W}}_{l'}}{ ([{I\models B}] + [{(I,\nu)\models B}])}}}=\displaystyle{{\sum_{B\in{\mathcal{W}}_{l'}}{ ([{I'\models B}] + [{(I',\nu')\models B}])}}}\end{equation*}

2. 2. the following inequality holds for level l

   \begin{equation*}\displaystyle{{\sum_{B\in{\mathcal{W}}_{l}}{ ([{I'\models B}] + [{(I',\nu')\models B}])}}}<\displaystyle{{\sum_{B\in{\mathcal{W}}_{l}}{ ([{I\models B}] + [{(I,\nu)\models B}])}}}\end{equation*}

Extended model $(I',\nu')$ max-dominates $(I,\nu)$ if we change less-than symbol by greater-than symbol in the inequality of Condition 2.

An extended model $(I^*,\nu^*)$ of ${\mathcal{W}}$ is optimal if there is no extended model $(I',\nu')$ of ${\mathcal{W}}$ that max-dominates $(I^*,\nu^*)$ . An extended model $(I^*,\nu^*)$ of ${\mathcal{W}}$ is min-optimal if there is no extended model $(I',\nu')$ of ${\mathcal{W}}$ that min-dominates $(I^*,\nu^*)$ .

5 Instances of Ew-systems

5.1 MaxSMT-family and optimization modulo theories

Lierler (Reference Lierler2021, Reference Lierler2022) illustrated the utility of w-systems – a precursor of ew-systems – by using these to capture the definitions of MaxSAT, weighted MaxSAT, and partially weighted MaxSAT (or, pw-MaxSAT) (Robinson et al. Reference Robinson, Gretton, Pham and Sattar2010). Here we look into capturing weighted MaxSMT and pw-MaxSMT.

We start by introducing some useful notation. For a vocabulary $\sigma$ , a specification [V, D], and an e-logic ${\mathcal{L}}+$ so that $\sigma_{{\mathcal{L}}+}=\sigma$ , $\Delta_{{\mathcal{L}}+}=D$ , $\Upsilon_{{\mathcal{L}}+}=V$ , an e-module $T_{{\mathcal{L}}+}$ is called $\sigma,V,D$ -theory/ $\sigma,V,D$ -module when $sem(T_{{\mathcal{L}}+})=Int(\sigma,V,D)$ . In other words, any extended interpretation in $Int(\sigma,V,D)$ is an extended model of a $\sigma,V,D$ -theory, and, consequently, any interpretation in $Int(\sigma)$ is a model of a $\sigma,V,D$ -theory. Note how specific language of e-logic of a $\sigma,V,D$ -theory becomes immaterial. Thus, we allow ourselves to denote an arbitrary $\sigma,V,D$ -theory by $T_{\sigma,V,D}$ disregarding the reference to its e-logic. Also recall that the (extended) interpretations/models of any theory are generalized to signatures that go beyond original signature of the considered theory.

Definition 14 (Weighted MaxSMT problems and their solutions) A weighted MaxSMT problem (Nieuwenhuis and Oliveras Reference Nieuwenhuis and Oliveras2006) over vocabulary $\sigma$ , class $\mathcal{C}$ of constraints and $({\sigma_c}, {\mathcal{C}})$ -denotation is defined as a set S of pairs $({{\mathcal{F}}}, {w})$ , where ${\mathcal{F}}$ is an SMT formula over $\sigma$ , $\mathcal{C}$ , and $({\sigma_c}, {\mathcal{C}})$ -denotation so that ${\mathcal{F}}$ is a clause, and w is a positive integer. ^{Footnote 2} An interpretation $I^*\in Int(\sigma)$ is a solution to weighted MaxSMT problem S, when it satisfies the equation

\begin{equation*}\displaystyle{I^*=\mathrm{arg\,max}_{I}{\sum_{({\mathcal{F}},w)\in S}{w\cdot [{I\models {\mathcal{F}}}]}}},\hbox{ where}\\ \end{equation*}

(12) \begin{equation}[{I\models {\mathcal{F}}}]=\begin{cases} \displaystyle{1} &\hbox{when $I\models {\mathcal{F}}$} \\ 0&\hbox{otherwise}\end{cases}\end{equation}

and I ranges over all interpretations in $Int(\sigma)$ .

Example 4 Consider specification $s_1$ , class $\mathcal{C}_1$ of constraints consisting of $c_1$ and its complement, vocabulary $\sigma_1$ , and $({\sigma_1}_c,\mathcal{C}_1)$ -denotation from Example. Set

\begin{equation*}\{(a\vee b,2), (\neg a,3), (\neg a\vee \neg|x\neq 0|,1)\}\end{equation*}

exemplifies a weighted MaxSMT problem. Its solutions are $\{b\}$ and $\{b,|x\neq 0|\}$ .

Proposition 2 Let S be a weighted MaxSMT problem. The optimal models of ew-system $(T_{\sigma_S,\Upsilon_S,\Delta_S},S)$ – where each element in S is understood as an ew-condition, whose theory is in SMT-logic – form the set of solutions for weighted MaxSMT problem S. Proposition 2 allows us to view ew-systems as a mean to state definitions of semantics of various formalisms captured by e-logics with optimizations in a uniform way. Indeed, we can formulate a definition of semantics of weighted MaxSMT problem by means of its relation to a respective ew-system: For a weighted MaxSMT problem S over vocabulary $\sigma$ , class $\mathcal{C}$ of constraints and $({\sigma_c}, {\mathcal{C}})$ -denotation, an optimal model of ew-system $(T_{\sigma_S,\Upsilon_S,\Delta_S},S)$ is a solution to S. In the sequel, we often take this approach to present the definitions of various optimization formalisms and their possible extensions. This allows us to bypass the complexity of varying terminology and notation coming from papers that introduce these formalisms. It is also worth to reiterate that we speak of papers stemming from various research communities that have their own traditions.

Note how in ew-system $(T_{\sigma_S,\Upsilon_S,\Delta_S},S)$ , where S is a weighted MaxSMT problem,

• levels of all ew-conditions are identical (set to 1) and

• the coefficients function assigns all variables to 0.

These observations lend themselves to a natural generalization of weighted MaxSMT problem.

Definition 15 (Generalized weighted MaxSMT problems and their (extended) solutions) A generalized weighted MaxSMT problem over class $\mathcal{C}$ of constraints is defined as a set S of ew-conditions in SMT-logic over $\mathcal{C}$ . Optimal models and optimal extended models of ew-system $(T_{\sigma_S,\Upsilon_S,\Delta_S},S)$ form solutions and extended solutions of S. Note how extended solutions of S take into account the quality of evaluation that is part of extended model. Also, levels become naturally incorporated into the framework.

Example 5 Let us continue Example 4. Let $f_x$ be a coefficients function defined as $f_x(0)=10$ , $f_x(1)=100$ , $f_x(2)=1000$ . The following set $\{(a\vee b,2), (\neg a,3), (\neg a\vee \neg|x\neq 0|,1;f_x)\}$ over $\sigma_1$ , $\mathcal{C}_1$ , and $({\sigma_1}_c,\mathcal{C}_1)$ -denotation forms a generalized weighted MaxSMT problem. Its solutions are $\{b\}$ and $\{b,|x\neq 0|\}$ . Its extended solution is $(\{b,|x\neq 0|\},\nu_2)$ , where $\nu_2$ is introduced in Example 2. If we redefine $f_x$ as follows $f_x(0)=1000$ , $f_x(1)=100$ , $f_x(2)=10$ , then the extended solution to considered problem is $(\{b\},\nu_0)$ .

We now define/generalize partially weighted MaxSMT (pw-MaxSMT) problem inspired by the notion of partially weighted MaxSAT problem (Robinson et al. Reference Robinson, Gretton, Pham and Sattar2010).

Definition 16 (Generalized partially weighted MaxSMT problems and their (extended) solutions) A generalized partially weighted MaxSMT (or gpw-MaxSMT) problem over vocabulary $\sigma$ , class $\mathcal{C}$ of constraints over specification [V, D] and $({\sigma_c}, {\mathcal{C}})$ -denotation is defined as ew-system (H,S), where H is a theory in SMT-logic over $\mathcal{C}$ and S is a collection of ew-conditions whose theories are in SMT-logic over $\mathcal{C}$ . Formula H is referred to as hard problem fragment, whereas S forms soft problem fragment. Optimal models and optimal extended models of ew-system (H,S) form solutions and extended solutions of (H,S).

5.1.1 $\nu\mathrm{Z}$ approach

As mentioned in the introduction, often the complete spectrum of capabilities of automated reasoning systems is described in papers and tutorials by means of examples appealing to intuitions of the readers. We argue that the presented framework provides convenient means to make such presentations formal. For example, Bjø rner et al. (2015), the authors of SMT solver $\nu\mathrm{Z}$ , state that

$\nu\mathrm{Z}$ extends the functionality of Z3 (de Moura and Bjørner 2008) to include optimization objectives. It allows users to solve SMT constraints and at the same time formulate optimality criteria for the solutions.

They then specify that $\nu\mathrm{Z}$ adds to SMT-LIB (Barrett et al. Reference Barrett, Fontaine and Tinelli2016; Barrett et al. Reference Barrett, Stump and Tinelli2010) – standard descriptions/language of background theories used in SMT systems – a command of the form

This command is said to assert soft constraint F, optionally with an integer weight n. ^{Footnote 3} If no weight is given, the default weight is 1. Code similar to the one presented in LHS of Figure 1 and the respective output of system $\nu\mathrm{Z}$ presented in RHS of the figure are used by Bjø rner et al. (2015) to illustrate a use of soft constraints.

Fig. 1.

LHS: SMT-LIB code suggesting to maximize $3 \cdot a2 + 5 \cdot \overline{a1}$ . RHS: $\nu\mathrm{Z}$ finds a solution where $x = y= 0$ .

We now elaborate on this example by Bjø rner et al. (2015) to uncover its implicit assumptions about readers intuitions and interpretations of the seen code and its behavior. Given code in Figure 1 (LHS) as an input, system z3-4.8.12 produces a model where x and y are both assigned to 0 suggesting that a1 and a2 are assigned to false. The authors of $\nu\mathrm{Z}$ informally state that code in Figure 1 (LHS) maximizes expression

(13) \begin{equation}3 \cdot a2 + 5 \cdot \overline{a1}.\end{equation}

To make this claim precise we recall that system $\nu\mathrm{Z}$ looks for models of a provided SMT formula specified in its $\mathtt{assert}$ statements – an implication $a2\rightarrow a1$ in this running example, where a1 and a2 are constraint atoms associated with (via $\mathtt{define-fun}$ statements) integer constraints $x>0$ and $x<y$ , respectively. Expressions a2 and $\overline{a1}$ in (13) should be interpreted in relation with some model X for the encoded SMT formula so that, for instance,

• a2 is mapped to 0 if model X assigns a2 to false, and 1 otherwise; similarly

• $\overline{a1}$ is mapped to 1 if model X assigns a1 to false, and 0 otherwise.

It is easy to see that there are three models to the implication $a2\rightarrow a1$ . Furthermore, for each of these three models there is an evaluation that maps integer variables x and y into values that satisfy integer constraints associated with constraint atoms a1 and a2. Thus, all these models form solutions to the SMT formula specified in Figure 1. These models together with the respective value of expression (13) follow:

\begin{equation*}\begin{array}{lll}a1 &a2&3 \cdot a2 + 5 \cdot \overline{a1} \\false&false& 5\\true&true& 3\\true&false&0\end{array}\end{equation*}

It is easy to see that the model listed first maximizes value of expression (13) in comparison to other models.

Generalized partially weighted MaxSMT problems and their solutions can be seen as formal specification of the language supported by the SMT solver $\nu\mathrm{Z}$ . Indeed, the statements that follow the key word $\mathtt{assert}$ correspond to hard problem fragment; whereas the statements that follow the key word $\mathtt{assert-soft}$ form soft problem fragment. In other words, we view $\nu\mathrm{Z}$ code as a specification of a gpw-MaxSMT problem, whereas we consider system $\nu\mathrm{Z}$ to compute solutions for given gpw-MaxSMT problems. Let us go back to the $\nu\mathrm{Z}$ code in Figure 1. It specifies the gpw-MaxSMT problem over vocabulary $\{a1,a2\}$ , class of integer constraints over specification $[{\{x,y\}}, {\mathbb{Z}}]$ , and denotation that maps a1 and a2 into integer constraints $x>0$ and $x<y$ , respectively; so that hard problem fragment consists of propositional formula $a2\rightarrow a1$ , and soft problem fragment consists of ew-conditions (a2,3) and $(\neg a1,5)$ . It is easy to see that interpretation mapping a1 and a2 to false forms a solution to the constructed gpw-MaxSMT problem.

Above, we complemented an earlier description of $\nu\mathrm{Z}$ input–output provided by an example with formal specification of these entities. It is also due to note that gpw-MaxSMT problems are more general than SMT-LIB specifications supported by $\nu\mathrm{Z}$ . For example, the notion of a level is present in gpw-MaxSMT specifications of its soft fragment. Also, the notion of an extended solution is defined for gpw-MaxSMT problems. This may provide inspirations for possible extensions to system $\nu\mathrm{Z}$ .

5.1.2 Cost-variable approach

Sebastiani and Tomasi (Reference Sebastiani and Tomasi2012) observed that MaxSMT and its variants encapsulated by gpw-MaxSMT when (non-extended) solutions are considered support optimizations that focus on “propositional part” of a problem encoded within SMT framework. They then proposed an alternative approach that ranks extended models of an SMT formula by value of one of its variables occurring in constraints associated with an SMT formula disregarding any information of a model from a propositional side. In particular, the value of that variable is to be minimized.

We now use ew-systems to capture an optimization satisfiability module problem (OMT) by Sebastiani and Tomasi (Reference Sebastiani and Tomasi2012). To proceed to the definition recall the notion of a $\sigma,V,D$ -theory, denoted $T_{\sigma,V,D}$ , introduced in the beginning of Section 5.1.

Definition 17 (OMT problems and their solutions) An OMT problem over vocabulary $\sigma$ , class $\mathcal{C}$ of constraints over specification [V, D] and $({\sigma_c}, {\mathcal{C}})$ -denotation and variable v occurring in V is defined as ew-system (H,S), where H is a theory in SMT-logic over $\sigma$ , $\mathcal{C}$ , and $({\sigma_c}, {\mathcal{C}})$ -denotation and S consists of a single ew-condition of the form $(T_{\emptyset,\{v\},D},0;(v)\mapsto 1)$ ; We call min-optimal extended models of this ew-systems solutions to OMT. The use of ew-condition $(T_{\emptyset,\{v\},D},0;(v)\mapsto 1)$ in this definition as the only criterion for optimization captures the idea of OMT that relies on the choice of a single variable in constraints to be minimized. Indeed, the first component $T_{\emptyset,\{v\},D}$ of this ew-condition is such that any (extended) interpretation of theory H in SMT-logic with variable v occurring in it is a model of $T_{\emptyset,\{v\},D}$ . The cost of any extended interpretation will be identified with the value of x assigned by this interpretation based on formula (11) used in the definition of the min-optimal extended model (for this instance, ${\mathcal{W}}_l$ in (11) is a singleton composed of $T_{\emptyset,\{v\},D}$ ). Indeed, take $(I,\nu)$ be an arbitrary model of $B=T_{\emptyset,\{v\},D}$ , then $[{I\models B}]=0$ and $[{(I,\nu)\models B}]=\nu(x)$ ; the sum of these values used within formula (11) amounts to $\nu(x)$ . This value is then used to decide on min-optimality of the model within expression (10), where max is replaced by min.

Example 6 Example 3 defines an SMT-logic theory H that has three extended models

\begin{equation*}(\{b\},\nu_0),~~ (\{b,|x\neq 0|\},\nu_1),~~ (\{b,|x\neq 0|\},\nu_2),\end{equation*}

where valuations $\nu_0,\nu_1,\nu_2$ are chosen to assign x to 0, 1, 2, respectively. A sample OMT problem follows

\begin{equation*}\Big(H,\big\{\big(T_{\emptyset,\{x\},\{0,1,2\}},0;(x)\mapsto 1\big)\big\}\Big)\end{equation*}

A solution for this OMT problem is an extended interpretation $(\{b\},\nu_0)$ – the one that minimizes the value of x.

5.3 Optimizations in CAS programs

We now turn our attention to CASP. At first, we review optimization statements of answer set programming. We illustrate how they can be understood within CASP framework. For this task we utilize ew-systems: just as we utilized ew-systems to capture generalization from pw-MaxSAT to pw-MaxSMT realm. We then look into clingcon style optimization statements native to CASP framework. We illustrate that ew-systems are general enough to encapsulate clingcon programs with optimizations. Systems clingcon-2 (Ostrowski and Schaub Reference Ostrowski and Schaub2012) and clingcon-3 (Banbara et al. Reference Banbara, Kaufmann, Ostrowski and Schaub2017) vary in the syntax of the languages they accept and algorithmic/implementation details. In case of this paper it is interesting to look at these systems in separation as they provide different support for optimization statements.

5.3.1 Optimizations in logic programming

We now review a definition of a logic program with weak constraints following the lines of Calimeri et al. (Reference Calimeri, Faber, Gebser, Ianni, Kaminski, Krennwallner, Leone, Ricca and Schaub2013). A weak constraint has the form

(14) \begin{equation}:\sim a_1,\dotsc, a_\ell,\ not\ a_{\ell+1},\dotsc,\ not\ a_m[w@\ell],\end{equation}

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

(15) \begin{equation}:\sim a_1,\dotsc, a_\ell,\ not\ a_{\ell+1},\dotsc,\ not\ a_m\end{equation}

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

(16) \begin{equation} a_1\wedge\dotsc\wedge a_\ell\wedge\ \neg a_{\ell+1}\wedge\dotsc\wedge\ \neg a_m.\end{equation}

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 forms 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@\ell]\in W\}$ . Set X of atoms over $\sigma$ is an answer set of ${\mathcal{P}}$ when it is an answer set of $\Pi$ .

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

1. 1. for any level l’ that is greater than l the following equality holds

   \begin{equation*}\displaystyle{ \sum_{D[w@\ell']\in W}{w \cdot[{X\models D}]}} =\displaystyle{\sum_{D[w@\ell']\in W}{w \cdot[{X'\models D}]}}\end{equation*}

2. 2. the following inequality holds for level l

   \begin{equation*}\displaystyle{\sum_{D[w@\ell]\in W}{w \cdot[{X'\models D}]}}<\displaystyle{ \sum_{D[w@\ell]\in W}{w \cdot[{X\models D}]}}\end{equation*}

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

We now exemplify the definition of an optimization program. Let $\Pi_1$ be logic program (3). An optimal answer set of optimization program

(17) \begin{equation}(\Pi_1,\{:\sim a,not\ b. -2@1\})\end{equation}

is $\{a\}$ .

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

(18) \begin{equation}\#minimize\{w_1@\ell_1:lit_1,\dots,w_n@\ell_n:lit_n \},\end{equation}

where $lit_i$ is either an atom $a_i$ or an expression $not\ a_i$ . This statement stands for n weak constraints

\begin{equation*}:\sim lit_1[w_1@\ell_1]~~\dots~~:\sim lit_n[w_n@\ell_n].\end{equation*}

Similarly, statement

(19) \begin{equation}\#maximize\{w_1@\ell_1:lit_1,\dots,w_n@\ell_n:lit_n \},\end{equation}

stands for n weak constraints

\begin{equation*}:\sim lit_1[-w_1@\ell_1]~~\dots~~:\sim lit_n[-w_n@\ell_n].\end{equation*}

Lierler (Reference Lierler2021) illustrated how o-programs can be identified with w-systems – a pre-cursor of ew-systems.

5.3.2 clingcon-2 style optimizations

Recall minimize statement (18). System clingcon-2 allows a user to write such statements using the following restrictions. All of these statements occurring in a program must either

• come with expressions $lit_i$ ( $1\leq i\leq n$ ) constructed from regular atoms of CAS program, or

• come with expressions $lit_i$ ( $1\leq i\leq n$ ) constructed from constraint variables stemming from irregular atoms of CAS program. Also, $w_i@\ell_i$ expressions are dropped in this case. ^{Footnote 4}

Thus, a user might either impose optimization criteria that pertain regular atoms or constraint variables associated with irregular atoms but not both. At the same time we note that the clingcon-2 authors provide no declarative semantics for programs with optimizations, but rather explain the behavior of the systems by means of examples. In what follows we capture the semantics of two variants of clingcon-2 formally. We refer to programs of clingcon-2 supporting optimization statements over regular atoms clingcon-2.1 programs. We refer to programs of clingcon-2 supporting optimization statements over constraint variables clingcon-2.2 programs.

clingcon-2.1 programs.

We now extend CAS programs with weak constraints in a similar way as MaxSMT extends SMT with “soft SMT clauses”.

Definition 20 (Optimization CAS program and their optimal (extended) answer sets) An optimization CAS program (or oCAS-program) over vocabulary $\sigma$ , class $\mathcal{C}$ of constraints, and $(\sigma_c,\mathcal{C})$ -denotation is an ew-system (P,W), where P is a CAS program over $\sigma$ , $\mathcal{C}$ and $(\sigma_c,\mathcal{C})$ -denotation, and W is a finite set of weak constraints over $\sigma$ , where we identify weak constraints of the form $D[w@\ell]$ with ew-condition $(D,w@\ell)$ in RSMT-logic over $\sigma$ , $\mathcal{C}$ , and $({\sigma_c}, {\mathcal{C}})$ -denotation. We call oCAS-program clingcon-2 style, when there is an additional restriction on its weak constraints W to be over signature $\sigma_r$ . Min-optimal models and min-optimal extended models of ew-system (P,W) form optimal answer sets and optimal extended answer sets of oCAS-program (P,W). Note how the syntax of weak constraints supports optimizations that consider “propositional part” of a problem encoded within CASP. Indeed, coefficients functions of ew-conditions in oCAS-programs are assumed to be the zero functions. Thus, it is easy to see that any optimal extended answer set $(X,\nu)$ of some CAS program is such, whenever X is an optimal answer set of this program; the quality of evaluation $\nu$ of the extended answer set is immaterial. Recall how “minimize” statements (18) are abbreviations for the set of weak constraints (see Section 5.3.1). In this regard, clingcon-2.1 programs are captured by clingcon-2 style oCAS-programs, in other words, the definitions of optimal answer sets and optimal extended answer sets of oCAS-program capture formally the semantics of clingcon-2.1 programs.

We also note that this observation allows us to utilize pw-MaxSMT solvers (such as, for example, solver $\nu\mathrm{Z}$ discussed here) for finding solutions to clingcon-2.1 programs. Indeed, the essential difference between clingcon-2.1 programs and pw-MaxSMT formalism boils down to the first component of the pairs capturing these objects. In one case we deal with CAS programs, in another with SMT formulas. Theory behind SMT-based CASP solver ezsmt (Lierler and Susman Reference Lierler and Susman2017; Shen and Lierler Reference Shen and Lierler2018) relies on the established link between these two. Here, we paved the way at enhancing ezsmt with the support for optimization statements.

clingcon-2.2 programs. We now elaborate on clingcon-2.2 programs. We start by quoting Ostrowski and Schaub (Reference Ostrowski and Schaub2012), who provide examples of optimization statements with constraint variables and informal discussions in order to illustrate their behavior. We supplement this quote with additional comments using square brackets to ease the understanding of the narrative. The clingcon-2.2 programs allow expressions of the kind

and its developers say that this is an instance of

a maximize statement over constraint variables. This is also a new feature of clingcon. We maximize the sum over a set of variables and/or expressions. In this case, we try to maximize

\begin{equation*}\mathtt{work(adam) \$+work(smith) \$+ work(lea) \$+ work(john)}.\end{equation*}

[During grounding (see, for instance, an account for grounder gringo Gebser et al. Reference Gebser, Schaub and Thiele2007b) – a process that is a common first step in solving ASP programs, where ASP variables are instantiated for suitable object constants – it was established that ASP variable A may take four values, namely, adam, smith, lea and john.] … To find a constraint optimal solution, we have to combine the enumeration techniques of clasp [by Gebser et al. Reference Gebser, Kaufmann, Neumann and Schaub2007a – answer set solver within clingcon] with the ones from the Constraint Programming (CP) solver. Therefore, when we first encounter a full propositional assignment, we search for an optimal (w.r.t. to the optimize statement) assignment of the constraint variables using the search engine of the CP solver. Let us explain this with the following constraint logic program.

Assume clasp has computed the full assignment $\{Fx \$* x \$< 25, Fa\}$ [irregular atom named $x \$* x \$< 25$ and regular atom a are assigned value false; intuitively the mentioned irregular atom is mapped into inequality $x * x < 25$ with constraint variable x]. Afterwards, we search for the constraint optimal solution to the constraint variable x, which yields $\{x \rightarrow 5\}$ . Given this optimal assignment, a constraint can be added to the CP solver that all further solutions shall be below/above this optimum $(x<5)$ . This constraint will now restrict all further solutions to be “better”. We enumerate further solutions, using the enumeration techniques of clasp. So the next assignment is $\{Tx \$* x \$< 25, Ta\}$ and the CP solver finds the optimal constraint variable assignment $\{x \rightarrow 1\}$ . Each new solution restricts the set of further solutions, so our constraint is changed to $(x\$<1)$ , which then allows no further solutions to be found.

To formalize the claims of this quote let us capture clingcon-2.2 programs as a Constraint Answer Set (CAS) program P extended with an expression of the form

(20) \begin{equation}\$minimize\{lit_1,\dots,lit_n \},\end{equation}

where $lit_i$ ( $1\leq i\leq n$ ) is a constraint variable stemming from irregular atoms of the considered CAS program. Ew-systems can be used to characterize clingcon-2.2 programs as follows.

Definition 21 (clingcon-2.2 programs and their optimal answer sets) A clingcon-2.2 program P (where P is a CAS program over $\sigma$ , $\mathcal{C}$ and $(\sigma_c,\mathcal{C})$ -denotation) extended with minimization statement (20) is ew-system (P,W), where W is a single ew-condition $(T_{\sigma_P,\Upsilon_P,\Delta_P},0;c)$ so that c is a coefficients function that to every constraint variable in $\Upsilon_P$ assigns 1 when it appears in (20) and 0 otherwise. Models of this ew-systems are called answer sets of P, while min-optimal models are called optimal answer sets of P.

Note how clingcon-2.1 and clingon-2.2 programs allow the user to either optimize propositional side of a problem or constraint side of the problem but never both. We now provide a definition for CAS programs with optimizations restoring to the method adopted earlier in stating the definition for gpw-MaxSMT problem. This allows us to incorporate quality of “constraint” part of the solution into assessment of overall quality of considered solution. This way quality of propositional and constraint part of solution is taken into account.

Definition 22 (CAS program with generalized optimizations; their optimal (extended) answer sets) A CAS program with generalized optimizations over vocabulary $\sigma$ , class $\mathcal{C}$ of constraints, and $({\sigma_c}, {\mathcal{C}})$ -denotation is defined as ew-system (H,S), where H is a theory in CAS-logic over $\sigma$ , $\mathcal{C}$ , and $({\sigma_c}, {\mathcal{C}})$ -denotation and S is a collection of ew-conditions, whose theories are in RSMT-logic over $\sigma$ , $\mathcal{C}$ , and $({\sigma_c}, {\mathcal{C}})$ -denotation. Min-optimal models and min-optimal extended models of ew-system (H,S) form optimal answer sets and optimal extended answer sets of CAS program with generalized optimizations (H,S).

Note how in this definition ew-conditions are more general than in oCAS-programs or Clingcon 2.2 programs.

5.3.3 clingcon-3 style optimizations

Banbara et al. (Reference Banbara, Kaufmann, Ostrowski and Schaub2017) introduce optimizations supported within clingcon-3. They propose minimize statements for CAS programs that have the form

(21) \begin{equation}\$minimize\{b_1\cdot x_1+c_1@\ell_1,~\dots,~b_n\cdot x_n+c_n@\ell_n \},\end{equation}

where $b_i$ and $c_i$ are integers, $x_i$ are variables stemming from the constraint part of the program, and $\ell_i$ is a level – positive integer. In addition, for any two expressions $b\cdot x+c@\ell$ and $b'\cdot x'+c'@\ell$ occurring in (21) variables x and x’ are distinct. Such minimize statements induce optimal extended answer sets as follows. For the remainder of this subsection, let P be a CAS program P’ extended with minimize statement of the form (21). Any (extended) answer set of P’ is an (extended) answer set of P. For a variable assignment $\nu$ and an integer l,

\begin{equation*}{\sum_{l}^\nu}=\sum_{b\cdot x+c@\ell\in (21)}{b\cdot \nu(x) +c}.\end{equation*}

Definition 23 (Optimal answer sets of CAS programs due to Banbara et al. Reference Banbara, Kaufmann, Ostrowski and Schaub2017) Let $(X,\nu)$ and $(X',\nu')$ be extended answer sets of P. Extended answer set $(X',\nu')$ dominates $(X,\nu)$ if there exists a level $l\in \{\ell_1,\dots,\ell_n\}$ ( $\ell_1,\dots,\ell_n$ are levels occurring in (21)) such that

1. 1. for any level $l'\in \{\ell_1,\dots,\ell_n\}$ that is greater than l the following equality holds

   \begin{equation*}\displaystyle{\sum_{l'}^\nu} =\displaystyle{\sum_{l'}^{\nu'}},\end{equation*}

2. 2. the following inequality holds for level l

   \begin{equation*}\displaystyle{\sum_{l}^{\nu'}} <\displaystyle{\sum_{l}^{\nu}},\end{equation*}

Extended answer set $(X^*,\nu^*)$ of P is optimal if there is no extended answer set $(X',\nu')$ that dominates $(X^*,\nu^*)$ .

For every level l appearing in (21), by

• $w_l$ we denote the sum $\displaystyle{\sum_{b\cdot x +c@\ell \in ~(21)} c}$ of constant terms in integer expressions associated with each level;

• $c_l$ we denote coefficient function from $\Upsilon_{P'}$ to $\mathbb{Z}$ that maps each variable x occurring in $\Upsilon_{P'}$ and in expression $b\cdot x +c@\ell$ in (21) to b, while all other variables in $\Upsilon_{P'}$ are mapped to 0.

As earlier we can identify any CAS program with the CAS-logic module. For the CAS program P’ extended with the minimize statement (21), we identify (21) with the set consisting of the following ew-conditions

• for every level l appearing in (21), ew-condition $(T_{\sigma_{P'},\Upsilon_{P'},\Delta_{P'}},w_l@\ell)$ ; and

• for every level l appearing in (21), ew-condition $(T_{\sigma_{P'},\Upsilon_{P'},\Delta_{P'}},0;c_l@\ell)$ .

Once more we can use ew-systems to provide an alternative definition for CAS programs with minimization statements of the kind introduced in this subsection. Let P be a CAS program P’ extended with minimize statements of the form (21) over vocabulary $\sigma$ , class $\mathcal{C}$ of constraints, and $(\sigma_c,\mathcal{C})$ -denotation. Min-optimal extended models of ew-system (P’,S) – where S is a collection of ew-conditions identified/associated with (21) of P – are optimal answer sets of P.

6 Formal properties of Ew-systems

Lierler (Reference Lierler2021) stated many interesting formal results for the case of w-systems; Lierler (Reference Lierler2022) presented proofs for these results. Many of these results/proofs can be lifted to the case of ew-systems. Here we present a series of formal results about ew-systems. Word Property denotes the results that follow rather immediately from the definitions of a model/optimal (extended) model.

• ew-system ${\mathcal{W}}$ and

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

• ew-system ${\mathcal{W}}$ and

• ew-system resulting from ${\mathcal{W}}$ by replacing each of its ew-conditions of the form $(T,w,{\bf c}@\ell)$ with ew-condition $(T,w@\ell)$ .

This property points at the fact that c component of ew-conditions are only relevant when optimality of extended models is considered.

We now state simple properties that pertain extended models of ew-systems.

• ew-system ${\mathcal{W}}$ and

• ew-system resulting from ${\mathcal{W}}$ by dropping all of its ew-conditions whose form is $(T,0@\ell)$

We call an ew-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}}})}$ . Lierler (Reference Lierler2021) stated propositions in spirit of Propositions 4 and 5 presented below for the case of w-systems. Here we lift these results to the case of ew-systems.

• ew-system ${\mathcal{W}}$ and

• the level-normal ew-system constructed from ${\mathcal{W}}$ by replacing each level $\ell_i$ occurring in its ew-conditions with its ascending sequence order number i, where we arrange elements in ${\lambda({{\mathcal{W}}})}$ in a sequence in ascending order $\ell_1,\ell_2,\dots \ell_{|{\lambda({{\mathcal{W}}})}|}$ .

Proposition 5 For an ew-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’ of ${\mathcal{W}}$ the equality

(22) \begin{equation} \sum_{B\in{\mathcal{W}}_{l}}{ [{I\models B}]}= \sum_{B\in{\mathcal{W}}_{l}}{ [{I'\models B}]} \end{equation}

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

The proposition above formulated for the case of extended models follows.

Proposition 6 For an ew-system ${\mathcal{W}}=({\mathcal{H}},{\mathcal{Z}})$ , if every level $l\in{\lambda({{\mathcal{W}}})}$ is such that for any distinct extended models $(I,\nu)$ and $(I',\nu')$ of ${\mathcal{W}}$ the equality

(23) \begin{equation}\displaystyle{\sum_{B\in{\mathcal{W}}_l}{ ([{I\models B}] + [{(I,\nu)\models B}])}=\sum_{B\in{\mathcal{W}}_l}{ ([{I'\models B}] + [{(I',\nu')\models B}])}}\end{equation}

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

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

For a coefficients function c mapping variables into reals by ${\bf c}^{-1}$ we denote a function on the same set of variables as c defined as follows

\begin{equation*}{\bf c}^{-1}(x)=-1\cdot {\bf c}(x).\end{equation*}

For ew-condition $(T,w;{\bf c}@\ell)$ , we define two mappings into related ew-conditions

\begin{equation*} \begin{array}{l} {(T,w;{\bf c}@\ell)}^{-1\cdot}=(T,-1\cdot w;{\bf c}@\ell),\\ {(T,w;{\bf c}@\ell)}^{-1\cdot-1\cdot}=(T,-1\cdot w;{\bf c}^{-1}@\ell).\\ \end{array} \end{equation*}

For ew-system $({\mathcal{H}},\{B_1,\dots, B_n\})$ , we define two mappings into related ew-systems using concepts above

\begin{equation*}\begin{array}{l}{({\mathcal{H}},\{B_1,\dots, B_n\})}^{-1\cdot}=({\mathcal{H}},\{{B_1}^{-1\cdot},\dots, {B_n}^{-1\cdot}\})\\{({\mathcal{H}},\{B_1,\dots, B_n\})}^{-1\cdot-1\cdot}=({\mathcal{H}},\{{B_1}^{-1\cdot-1\cdot},\dots, {B_n}^{-1\cdot-1\cdot}\})\\\end{array}\end{equation*}

With this newly introduced notation we can now claim the relation between optimal and min-optimal (extended) models of ew-systems.

Eliminating Negative (or Positive) Weights We call e-logics ${\mathcal{L}}$ and ${\mathcal{L}}'$ compatible when their vocabularies, domains, and variables coincide, that is, $\sigma_{\mathcal{L}}=\sigma_{{\mathcal{L}}'}$ , $\Delta_{{\mathcal{L}}}=\Delta_{{\mathcal{L}}'}$ , and $\Upsilon_{{\mathcal{L}}}=\Upsilon_{{\mathcal{L}}'}$ . Let ${\mathcal{L}}$ and ${\mathcal{L}}'$ be compatible logics, and T and T’ be theories in these logics, respectively. We call a theory T (and a w-condition $(T,w;{\bf c}@\ell)$ ) equivalent to a theory T’ (and a w-condition $(T',w;{\bf c}@\ell)$ , respectively), when $sem(T)= sem(T')$ .

Property 7 Models and optimal/min-optimal models/extended models of ew-systems

\begin{equation*}(\{T_1,\dots,T_n\},\{B_1,\dots,B_m\}) \hbox{ and } (\{T'_1,\dots,T'_n\},\{B'_1,\dots,B'_m\})\end{equation*}

coincide when (i) $T_i$ and $T'_i$ ( $1\leq i\leq n$ ) are equivalent theories, and (ii) $B_i$ and $B'_i$ ( $1\leq i\leq m$ ) are equivalent ew-conditions.

For a theory T of e-logic ${\mathcal{L}}$ , we call a theory $\overline{T}$ in e-logic ${\mathcal{L}}'$ , compatible to ${\mathcal{L}}$ , complementary when (i) $sem(T)\cap sem(\overline{T})=\emptyset$ , and (ii) $sem(T)\cup sem(\overline{T}) = {\mathit{Int}}(\sigma_{{\mathcal{L}}},\Upsilon_{{\mathcal{L}}},\Delta_{{\mathcal{L}}})$ .

Let $(T,w;{\bf c}@\ell)$ be an ew-condition; consider the following definitions:

\begin{equation*}\begin{array}{l}{(T,w;{\bf c}@\ell)}^+=\begin{cases} (T,w;{\bf c}@\ell)&\hbox{when $w\geq 0$, otherwise } \\ (\overline{T},-1\cdot w;{\bf c}@\ell) \\\end{cases}\\~\\{(T,w;{\bf c}@\ell)}^-=\begin{cases} (T,w;{\bf c}@\ell)&\hbox{when $w\leq 0$, otherwise } \\ (\overline{T},-1\cdot w;{\bf c}@\ell) \\ \end{cases}\\~\\{(T,w;{\bf c}@\ell)}^{+;+}=\begin{cases} (T,w;{\bf c}@\ell)&\hbox{when $w\geq 0$, otherwise } \\ (\overline{T},-1\cdot w;{\bf c}^{-1}@\ell) \\\end{cases}\\~\\{(T,w;{\bf c}@\ell)}^{-;-}=\begin{cases} (T,w;{\bf c}@\ell)&\hbox{when $w\leq 0$, otherwise }, \\ (\overline{T},-1\cdot w;{\bf c}^{-1}@\ell) \\\end{cases}\end{array}\end{equation*}

where $\overline{T}$ denotes some theory complement to T.

For an ew-system $({\mathcal{H}},\{B_1,\dots,B_m\})$ , we define

(24) \begin{equation}\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}^-\}),\\{({\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}\end{equation}

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

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

coincide.

• $({\mathcal{H}},\{(T,w;{\bf c}@\ell)\}\cup{\mathcal{Z}})$ and

• $({\mathcal{H}},\{(\overline{T},-1\cdot w;{\bf c}^{-1}@\ell)\}\cup{\mathcal{Z}})$

coincide.

The notation and results of the section on Eliminating Levels by Lierler (2021,Reference Lierler2022) can be lifted to the case of ew-systems and their optimal/min-optimal models in a straightforward manner (similar as the results for eliminating negative/positive weights are lifted here). Hence, we omit the review of these results. Yet, the “cost” expression associated with the second member of extended model is more complex so that the role of the levels seem to go beyond syntactic sugar when extended models are considered.

7 Proofs

Many of the formal properties of ew-systems presented in Section 6 echo similar results for w-systems – a precursor of ew-systems introduced by Lierler (Reference Lierler2021). Lierler (Reference Lierler2022) presented proofs for these results for w-systems. The logic and structure of proofs for the case of ew-systems follows the proofs for the case of w-systems. In this section, we often remark on the connection to the proofs by Lierler (Reference Lierler2022) and point at any details worth noting.

Just as in case for w-systems, we focus on results for optimal (extended) models only, as the arguments for min-optimal (extended) models follow the same lines. Given recursive Definitions 10 and 11 of l-(min)-optimal (extended) models, inductive argument is a common technique in proof construction about properties of such models. In particular, the induction on levels of a considered ew-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}$ .

Proof of Proposition 1. The statement of Proposition 1 echoes the statement of Proposition 1 by Lierler (Reference Lierler2022) for the case of w-systems. The proofs of the two claims (i) Definitions 10 and 12 are equivalent; and (ii) Definitions 11 and 13 are equivalent follow the lines of the proof provided for Proposition 1 by Lierler (Reference Lierler2022). In fact, for the claim (i) we can repeat the proof practically verbatim modulo the understanding that in place of w-system ${\mathcal{W}}$ we consider ew-system ${\mathcal{W}}$ as well as in place of w-conditions of ${\mathcal{W}}$ we consider ew-conditions of ${\mathcal{W}}$ . For the claim (ii), in addition to the proof of Proposition 1 by Lierler (Reference Lierler2022) will have to refer to extended interpretations in place of interpretations and to summations of the form

\begin{equation*}\sum_{B\in{\mathcal{W}}_l}{ ([{I\models B}] + [{(I,\nu)\models B}])}\end{equation*}

in place of summations of the form

\begin{equation*}\sum_{B\in{\mathcal{W}}_l}{ ([{I\models B}]}.\end{equation*}

Claims of Lemmas 1, 2, and 3 by Lierler (Reference Lierler2022) hold for the case of ew-systems and their l-optimal models and l-optimal extended models.

Proof of Proposition 2. Let S be a weighted MaxSMT problem and ${\mathcal{W}}_S=(T_{\sigma_S,\Upsilon_S,\Delta_S},S)$ be a respective ew-system – where each element in S is understood as an ew-condition, whose theory is in SMT-logic. Consider an arbitrary interpretation $I^*\in Int(\sigma_S)$ . We show that $I^*$ is a solution to weighted MaxSMT problem S if and only if $I^*$ is an optimal models of ${\mathcal{W}}_S$ . Per Definition 13, interpretation $I^*$ is a solution to S if and only if

\begin{equation*}\begin{array}{l}\displaystyle{I^*=\mathrm{arg\,max}_{I}{\sum_{({\mathcal{F}},w)\in S}{w\cdot [{I\models {\mathcal{F}}}]}}},\end{array}\end{equation*}

where I ranges over all interpretations in $Int(\sigma_S)$ . By the definition of $T_{\sigma_S,\Upsilon_S,\Delta_S}$ , any interpretation in $Int(\sigma_S)$ is its model. Per Definition 10, interpretation $I^*$ is an optimal model of ${\mathcal{W}}_S$ if and only if

\begin{equation*}I^*=\displaystyle{ arg\max_{I} {\sum_{({\mathcal{F}},w)\in S}{ [{I\models ({\mathcal{F}},w)}]}}},\end{equation*}

where I ranges over all interpretations in $Int(\sigma_S)$ .

Taking definitions (7) and (12) into account and an understanding that each element in S can be seen as an ew-condition, whose theory is in SMT-logic, we conclude that for any interpretation I in $Int(\sigma_S)$

\begin{equation*} {\sum_{({\mathcal{F}},w)\in S}{w\cdot [{I\models {\mathcal{F}}}]}}= {\sum_{({\mathcal{F}},w)\in S}{ [{I\models ({\mathcal{F}},w)}]}}.\end{equation*}

It is easy to see that any extended answer set of P is an extended model of (P’,S). Thus, the proof focuses on optimality condition.

Per Definition 19, $(X^*,\nu^*)$ is an optimal extended answer set if and only if there is no extended answer set $(X',\nu')$ that dominates $(X^*,\nu^*)$ . In other words, any answer set $(X',\nu')$ is such that for every level l occurring in (21) either

1. 1. there exists a level l’ occurring in (21) that is greater than l and the following inequality holds

   \begin{equation*}\displaystyle{\sum_{l'}^{\nu^*}} \neq \displaystyle{\sum_{l'}^{\nu'}},\end{equation*}
   or

2. 2. the following inequality holds for level l

   \begin{equation*}\displaystyle{\sum_{l}^{\nu'}} \geq \displaystyle{\sum_{l}^{\nu^*}},\end{equation*}

Per Definition 13, $(X^*,\nu^*)$ is min-optimal extended model of ew-system (P’,S) if and only if there is no extended model $(I',\nu')$ of (P’,S) that min-dominates $(X^*,\nu^*)$ . In other words, any extended model $(X',\nu')$ is such that for every level $l\in {\lambda({(P',S)})}$ either

1. 1. there exists a level $l'\in {\lambda({(P',S)})}$ that is greater than l and the following inequality holds

   \begin{equation*}\displaystyle{{\sum_{B\in (P',S)_{l'}}{ ([{X^*\models B}] + [{(X^*,\nu^*)\models B}])}}}\neq\displaystyle{{\sum_{B\in(P',S)_{l'}}{ ([{X'\models B}] + [{(X',\nu')\models B}])}}}\end{equation*}
   or

2. 2. the following inequality holds for level l

   \begin{equation*}\displaystyle{{\sum_{B\in(P',S)_{l}}{ ([{X'\models B}] + [{(X',\nu')\models B}])}}}\geq\displaystyle{{\sum_{B\in(P',S)_{l}}{ ([{X^*\models B}] + [{(X^*,\nu^*)\models B}]).}}}\end{equation*}

We first observe that by the construction of S any level l occurs in (21) if and only if $l\in {\lambda({(P',S)})}$ . Recall that any extended answer set of P is an extended model of (P’,S). It is now sufficient to show that given any extended model $(X,\nu)$ of (P’,S), the following equality holds for arbitrary level $l\in {\lambda({(P',S)})}$ :

(25) \begin{equation}\displaystyle{\sum_{l}^{\nu}}=\displaystyle{{\sum_{B\in (P',S)_{l}}{ ([{X\models B}] + [{(X,\nu)\models B}])}}}.\end{equation}

Indeed, per definition of ${\sum_{l}^\nu}$

(26) \begin{equation} {\sum_{l}^\nu}=\sum_{b\cdot x+c@\ell \hbox{ in } (21)}{(b\cdot \nu(x) +c)}= \sum_{b\cdot x+c@\ell \hbox{ in } (21)}{b\cdot \nu(x)}+\sum_{b\cdot x+c@\ell \hbox{ in } (21)}{c}. \end{equation}

Per S construction, $(P',S)_{l}$ consists of two ew-conditions

• $(T_{\sigma_{P'},\Upsilon_{P'},\Delta_{P'}},w_l@\ell)$ ; and

• $(T_{\sigma_{P'},\Upsilon_{P'},\Delta_{P'}},0;c_l@\ell)$ .

It is easy to see that

\begin{equation*}[(X,\nu)\models (T_{\sigma_{P'},\Upsilon_{P'},\Delta_{P'}},w_l@\ell)]= 0, \end{equation*}

\begin{equation*}[X\models (T_{\sigma_{P'},\Upsilon_{P'},\Delta_{P'}},0;c_l@\ell)]= 0. \end{equation*}

Per definitions of $w_l$ and $c_l$ , we derive that

\begin{equation*}[X\models (T_{\sigma_{P'},\Upsilon_{P'},\Delta_{P'}},w_l@\ell)]=w_l= \sum_{b\cdot x +c@\ell \hbox{ in}~(21)} {c}, \end{equation*}

and

\begin{equation*}[(X,\nu)\models (T_{\sigma_{P'},\Upsilon_{P'},\Delta_{P'}},0;c_l@\ell)]= \sum_{x\in \Upsilon_{P'}}{\nu(x)\cdot c_l(x)} = \sum_{b\cdot x+c@\ell \hbox{ in } (21)}{b\cdot \nu(x)}.\end{equation*}

Consequently,

(27) \begin{equation}{\sum_{B\in (P',S)_{l}}{ ([{X\models B}] + [{(X,\nu)\models B}])}}= \sum_{b\cdot x+c@\ell \hbox{ in } (21)}{b\cdot \nu(x)}+\sum_{b\cdot x+c@\ell \hbox{ in } (21)}{c}.\end{equation}

Equality (25) follows immediately from (26) and (27).

Proof of Proposition 4 follows from the fact that the numeric value of any level itself is inessential in the key computations associated with establishing optimal (extended) 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 this proposition preserves original order of the levels with respect to greater relation.

Propositions 5 and 6 follow immediately from Propositions 7 and 8, respectively. The statement of Proposition 7 echoes the statement of Proposition 8 by Lierler (Reference Lierler2022) for the case of w-systems. The statement of Proposition 8 lifts the statement of Proposition 7 from the case of models to the case of extended models. The proofs of Propositions 7 and 8 follow the lines of the proof provided for Proposition 8 by Lierler (Reference Lierler2022) modulo similar provisions as pointed at in the beginning of this section in Proof of Proposition 1 (sketch).

The statement and proof of Proposition 9 echoes the statement and proof of Proposition 9 by Lierler (Reference Lierler2022) for the case of w-systems. The structure of the following proof is in spirit of the proof of Proposition 9 by Lierler (Reference Lierler2022) and, yet, we state some of its details here as mapping ${(\cdot)}^{-1\cdot-1\cdot}$ is unique to this work.

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

\begin{equation*}(I^*,\nu^*)=\displaystyle{ \arg\min_{(I,\nu)} {\sum_{B\in{\mathcal{W}}_l}{ \Big( -1\cdot [{I\models B}] + (-1 \cdot [{(I,\nu)\models B}])\Big)}}.}\end{equation*}

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

\begin{equation*}(I^*,\nu^*)=\displaystyle{ \arg\min_{(I,\nu)} {\sum_{B\in{{\mathcal{W}}}^{-1\cdot-1\cdot}_l}{ ( [{I\models B}] + [{(I,\nu)\models B}])}}.}\end{equation*}

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

Inductive case argument follows similar lines.

Propositions 11 and 13 follow from Propositions 12 and 14, respectively. Proofs of Propositions 12 and 14 follow the lines of proof of Proposition 11 stated by Lierler (Reference Lierler2022).