Treewidth-aware Reductions of Normal ASP to SAT Is Normal ASP Harder than SAT after All

2025-05-06 0 0 821.6KB 44 页 10玖币

侵权投诉

Treewidth-aware Reductions of Normal ASP to

SAT– Is Normal ASP Harder than SAT after

All?

Markus Hecher

TU Wien, Vienna, Austria

hecher@dbai.tuwien.ac.at

October 10, 2022

Abstract

Answer Set Programming (ASP) is a paradigm for modeling and solv-

ing problems for knowledge representation and reasoning. There are

plenty of results dedicated to studying the hardness of (fragments of)

ASP. So far, these studies resulted in characterizations in terms of com-

putational complexity as well as in ﬁne-grained insights presented in form

of dichotomy-style results, lower bounds when translating to other for-

malisms like propositional satisﬁability (SAT), and even detailed param-

eterized complexity landscapes. A generic parameter in parameterized

complexity originating from graph theory is the so-called treewidth, which

in a sense captures structural density of a program. Recently, there was an

increase in the number of treewidth-based solvers related to SAT. While

there are translations from (normal) ASP to SAT, no reduction that pre-

serves treewidth or at least keeps track of the treewidth increase is known.

In this paper we propose a novel reduction from normal ASP to SAT

that is aware of the treewidth, and guarantees that a slight increase of

treewidth is indeed suﬃcient. Further, we show a new result establishing

that, when considering treewidth, already the fragment of normal ASP is

slightly harder than SAT (under reasonable assumptions in computational

complexity). This also conﬁrms that our reduction probably cannot be

signiﬁcantly improved and that the slight increase of treewidth is unavoid-

able. Finally, we present an empirical study of our novel reduction from

normal ASP to SAT, where we compare treewidth upper bounds that

are obtained via known decomposition heuristics. Overall, our reduction

works better with these heuristics than existing translations.

1 Introduction

Answer Set Programming (ASP) [20] is an active research area of knowledge

representation and reasoning. ASP provides a declarative modeling language

arXiv:2210.03553v1 [cs.AI] 7 Oct 2022

and problem solving framework [54] for hard computational problems, which

has been widely applied [7, 81, 82, 59, 86, 1]. There are very eﬃcient ASP

solvers [54, 3, 21] as well as several recent (language) extensions [21, 22, 24, 23].

In ASP, questions are encoded into rules and constraints that form a program

(over atoms), whose solutions are called answer sets.

In terms of computational complexity, the consistency problem of decid-

ing the existence of an answer set is well-studied, i.e., the problem is ΣP

complete [35]. Some fragments of ASP have lower complexity though. A

prominent example is the class of head-cycle-free (HCF) programs [9], which

is a generalization of the class of normal programs and requires the absence of

cycles in a dependency graph representation of the program. Deciding whether

such a program has an answer set is NP-complete.

There is also a wide range of more ﬁne-grained studies [88] for ASP, also

in parameterized complexity [27, 80, 31, 52], where certain (combinations of)

parameters [50, 71] are taken into account. In parameterized complexity, the

“hardness” of a problem is classiﬁed according to the impact of a parameter for

solving the problem. There, one often distinguishes the runtime dependency

of the parameter, e.g., levels of exponentiality [76, 79] in the parameter, re-

quired for problem solving. Concretely, under the reasonable Exponential Time

Hypothesis (ETH) [63], propositional satisﬁability ( SAT)is single exponential

in the structural parameter treewidth, whereas evaluating Quantiﬁed Boolean

formulas (QBFs) of quantiﬁer depth two is [72] double exponential1in the

treewidth k.

For ASP there is growing research on treewidth [64, 44, 41], which even

involves grounding [11, 14]. Algorithms of these works exploit structural re-

strictions (in form of treewidth) of a given program, and often run in polyno-

mial time in the program size, while being exponential only in the treewidth.

Intuitively, treewidth gives rise to a tree decomposition, which allows solving nu-

merous NP-hard problems in parts (via dynamic programming) and indicates

the maximum number of variables one has to investigate in such parts during

evaluation. There were also dedicated competitions [28] and notable progresses

in SAT [49, 25] and other areas [8].

Naturally, there are numerous reductions of ASP [26, 9, 74, 65, 4] and ex-

tensions thereof [19, 17] to SAT. These reductions have been investigated in the

context of resulting formula size and number of auxiliary variables. However,

structural dependency in form of, e.g., treewidth, has not been considered yet.

Notably, there are existing reductions causing a sub-quadratic blow-up in the

number of variables (auxiliary variables), which is unavoidable [73] if the answer

sets should be preserved (bijectively). However, if one considers the structural

dependency in form of treewidth, existing reductions could cause quadratic or

even unbounded overhead in the treewidth.

On the contrary, we present a novel reduction for HCF programs that in-

creases the treewidth kat most sub-quadratically (k·log(k)). This is indeed inter-

esting as there is a close connection [6] between resolution-width and treewidth,

1Double exponentiality refers to runtimes of the form 22O(k)·n.

resulting in eﬃcient SAT solver runs on instances of small treewidth. As a

result, our reduction could be of use for solving approaches based on SAT

solvers [75, 65]. Then, we establish lower bounds, under ETH, for exploit-

ing treewidth for consistency of normal programs. This renders normal ASP

“harder” than SAT. At the same time we prove that one cannot signiﬁcantly

improve the reduction, i.e., avoid the sub-quadratic increase of treewidth.

Contributions. Concretely, we provide the following.

1. First, we present a novel reduction from HCF programs to SAT, which

only requires linearly many auxiliary variables plus a number of auxiliary

variables that is linear in the instance size and slightly superexponential in

the treewidth of the SAT instance. This is achieved by guiding the whole

reduction along a tree decomposition of the program. Thereby the re-

duction only increases the treewidth sub-quadratically, i.e., the treewidth

of the resulting SAT formula is slightly larger than the treewidth of the

given program.

2. Then, we develop and discuss a slightly diﬀerent reduction from HCF pro-

grams to SAT, where we show a bijective correspondence between answer

sets of the program and models of the propositional formula for a certain

sub-class of programs. This reduction, while preserving bijectivity for

certain programs, comes at the cost of a quadratic increase of treewidth.

3. We show that avoiding a sub-quadratic increase in the treewidth is very

unlikely. Concretely, we establish that under the widely believed Exponen-

tial Time Hypothesis (ETH), one cannot decide ASP in time 2o(k·log(k)) ·n,

with treewidth kand program size n. This is in contrast to the runtime

for deciding SAT: 2O(k)·nwith treewidth kand size nof the formula.

As a result, this establishes that the consistency of normal ASP programs

is already harder than SAT using treewidth. Note that this is surprising

as both problems are of similar hardness according to classical complexity

(NP-complete).

4. Finally, we present an empirical study of the ﬁrst contribution, where we

compare treewidth upper bounds that are obtained via existing decom-

position heuristics. Interestingly, compared with existing translations, in

both acyclic and cyclic scenarios, our reduction overall works better with

these heuristics than existing translations.

This is an extended version of a paper [60] at the 17th International Conference

on Principles of Knowledge Representation and Reasoning (KR 2020). In addi-

tion to the conference version, this work contains additional examples and more

detailed explanations. Further, we added the second contribution and worked

out details in terms of bijective preservation of answer sets. We were also able

to simplify the reduction of the third contribution and discuss relations to other

works in detail. Further, we added an empirical study of treewidth, where we

compare treewidth upper bounds of our reduction and an exisiting translation

via an eﬃcient decomposer based on heuristics.

Related Work. For disjunctive ASP and extensions thereof, algorithms have

been proposed [64, 83, 44] running in time linear in the instance size, but double

exponential in the treewidth. Under ETH, one cannot signiﬁcantly improve this

runtime, using a result [72] for QBFs with quantiﬁer depth two and a standard

reduction [35] from this QBF fragment to disjunctive ASP. Unsurprisingly, SAT

only requires single exponential runtime [85] in the treewidth. However, for

normal and HCF programs only a slightly superexponential algorithm [41] for

solving consistency is known so far. Still, the question whether the slightly

superexponentiality can be avoided was left open. The proposed algorithm was

used for counting answer sets involving projection [57], which is at least double

exponential [45] in the treewidth.

There are also further studies on certain classes of programs and their rela-

tionships in the form of whether there exist certain reductions between these

classes, thereby bijectively preserving the answer sets. These studies result in

an expressive power hierarchy among program classes [65]. Note that while

existing results [73] and the expressive power hierarchy weakly indicate that

normal ASP might be slightly harder than SAT, these results mostly deal with

bijectively preserving all answer sets. However, our work considers the plain

consistency problem, where ASP and SAT are both NP-complete.

2 Preliminaries

Before we discuss our reductions, we brieﬂy recall some basics.

Answer Set Programming (ASP). We assume familiarity with propositional

satisﬁability (SAT) [13, 67], and follow standard deﬁnitions of propositional

ASP [20, 66]. Let `,m,nbe non-negative integers such that `≤m≤n,

a1,. . .,anbe distinct propositional atoms. Moreover, we refer by literal to a

propositional variable (atom) or the negation thereof. A program Π is a set of

rules of the form

a1∨ · · · ∨ a`←a`+1, . . . , am,¬am+1,...,¬an.

For a rule r, we let Hr:={a1, . . . , a`},B+

r:={a`+1, . . . , am}, and B−

r:=

{am+1, . . . , an}. We denote the sets of atoms occurring in a rule ror in a

program Π by at(r):=Hr∪B+

r∪B−

rand at(Π) :=Sr∈Πat(r). A rule r

is normal if |Hr| ≤ 1 and unary if |B+

r| ≤ 1. Then, a program Π is normal

or unary if all its rules r∈Π are normal or unary, respectively. The positive

dependency digraph DΠof Π is the directed graph deﬁned on the set of atoms

from Sr∈ΠHr∪B+

r, where for every rule r∈Π two atoms a∈B+

rand b∈Hr

are joined by an edge (a, b). A head-cycle of DΠis an {a, b}-cycle2for two

distinct atoms a,b∈Hrfor some rule r∈Π. Program Π is head-cycle-free

2Let G= (V, E) be a digraph and W⊆V. Then, a (directed) cycle in Gis a W-cycle if it

contains all vertices from W.

dbc

Figure 1: Dependency graph DΠof Π (cf., Example 1).

(HCF) if DΠcontains no head-cycle [9] and we say Π is tight if there is no

directed cycle in DΠ[38].

An interpretation Iis a set of atoms. Isatisﬁes a rule rif (Hr∪B−

r)∩I6=∅

or B+

r\I6=∅.Iis a model of Π if it satisﬁes all rules of Π, in symbols I|= Π.

For brevity, we view propositional formulas as sets of formulas (e.g., clauses)

that need to be satisﬁed, and use the notion of interpretations, models, and

satisﬁability analogously. The Gelfond-Lifschitz (GL) reduct of Π under Iis

the program ΠIobtained from Π by ﬁrst removing all rules rwith B−

r∩I6=∅

and then removing all ¬zwhere z∈B−

rfrom the remaining rules r[58]. Iis an

answer set of a program Π if Iis a minimal model of ΠI. The problem of decid-

ing whether an ASP program has an answer set is called consistency, which is

ΣP

2-complete [35]. If the input is restricted to normal programs, the complexity

drops to NP-complete [12, 78]. A head-cycle-free program Π can be translated

into a normal program in polynomial time [9]. Further, the answer sets of a tight

program can be represented by means of the models of a propositional formula,

obtainable in linear time via, e.g., Clark’s completion [26]. The following charac-

terization of answer sets is often applied when considering normal programs [74].

For a given set A⊆at(Π) of atoms, a function ϕ:A→ {0,...,|A| − 1}is an

ordering over A. Let Ibe a model of a normal program Π, and ϕbe an order-

ing over I. We say a rule r∈Π is suitable for proving a∈Iif (i) a∈Hr, (ii)

B+

r⊆I, (iii) I∩B−

r=∅, as well as (iv) I∩(Hr\ {a}]) = ∅. An atom a∈I

is proven if there is a rule r∈Πproving a, which is the case if ris suitable for

proving aand ϕ(b)< ϕ(a) for every b∈B+

r. Then, Iis an answer set of Π

if (i) Iis a model of Π, and (ii) Iis proven, i.e., every a∈Iis proven. This

characterization vacuously holds also for head-cycle-free programs [9], since in

HCF programs, vaguely speaking, all but one atom of the head of any rule can

be “shifted” to the negative body [30].

Example 1. Consider the given program Π:={

z }| {

a∨b←;

z }| {

c∨e←d;

z }| {

d←b, ¬e;

z }| {

e←b, ¬d;

z }| {

b←e, ¬d;

z }| {

d← ¬b}. Observe that Πis not tight, since the depen-

dency graph DΠof Figure 1 contains the cycle b, d, e. However, the program Π

is head-cycle-free since there is neither an {a, b}-cycle, nor a {c, e}-cycle in DΠ.

Therefore, rule r1allows shifting [30] and actually corresponds to the two rules

a← ¬band b← ¬a. Analogously, rule r2can be seen as the rules c←d, ¬e

and e←d, ¬c. Then, I:={b, c, d}is an answer set of Π, since I|= Π, and we

can prove with ordering ϕ:={b7→ 0, d 7→ 1, c 7→ 2}atom bby rule r1, atom d

by rule r3, and atom cby rule r2. Further answer sets of Πare {b, e},{a, c, d},

and {a, d, e}.

The characterization above already fails for simple programs that are not

HCF. Consider for example program Π0:={a∨b←;a←b;b←a}, which

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

Treewidth-awareReductionsofNormalASPtoSAT{IsNormalASPHarderthanSATafterAll?MarkusHecherTUWien,Vienna,Austriahecher@dbai.tuwien.ac.atOctober10,2022AbstractAnswerSetProgramming(ASP)isaparadigmformodelingandsolv-ingproblemsforknowledgerepresentationandreasoning.Thereareplentyofresultsdedicatedtostudyin...

展开>> 收起<<

Treewidth-aware Reductions of Normal ASP to SAT Is Normal ASP Harder than SAT after All.pdf

共44页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Treewidth-aware Reductions of Normal ASP to SAT Is Normal ASP Harder than SAT after All

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: