While mathematical models act as vital decision support systems for operational Air Traffic Flow and Capacity Management (ATFCM), existing approaches isolate Air Traffic Flow Management (ATFM) from Dynamic Airspace Configuration (DAC). This separation introduces an unresolved circular dependency between fixed-demand and fixed-capacity assumptions. Although joint optimization resolves this gap, the enlarged search space renders exact models computationally intractable for medium- to large-scale instances. To bridge this gap, we propose ASPaeroFlow: a heuristic for the joint ATFCM; it combines instance-space decomposition heuristics with a local exact approach using Answer Set Programming. We benchmark ASPaeroFlow from small to industry-sized instances and compare it with exact and alternative approaches. The results indicate that (1) the heuristic provides a computational middle ground between exact methods and operational baselines; (2) simultaneous optimization can outperform sequential optimization on joint ATFCM; and (3) an ablation study indicates that DAC has a larger impact on solution quality than flow measures.

Assumption-based argumentation (ABA) is a powerful defeasible reasoning formalism which is based on the interplay of assumptions, their contraries, and inference rules. ABA with preferences (ABA+) generalizes the basic model by allowing a qualitative comparison of assumptions. The integration of preferences however comes with a cost. In ABA+, the evaluation under two central and well-established semantics-grounded and complete semantics-is not guaranteed to yield an outcome. Moreover, while ABA frameworks without preferences allow for a graph-based representation in Dung-style frameworks, an according instantiation for general ABA+ frameworks has not been established so far. In this work, we tackle both issues: First, we develop a novel abstract argumentation formalism based on set-to-set attacks. We show that our so-called Hyper Argumentation Frameworks (HYPAFs) capture the attack relation between assumptions in ABA+. Second, we exploit this correspondence between ABA+ and HYPAFs to obtain relaxed variants of complete and grounded semantics for HYPAFs that yield an extension for all frameworks by design, while still faithfully generalizing the established semantics of Dung-style Argumentation Frameworks. Finally, we discuss fundamental properties and provide a thorough complexity analysis for both the abstract HYPAFs as well as ABA+.

Fragments of propositional logic, i.e., tailored sub-languages designed for neatly structured data, are relevant in many practical settings. This paper studies belief update in fragments (e.g., Horn, Krom, affine) that obey a desirable semantic closure condition. We assume update is guided by the well-known Katsuno-Mendelzon (KM) postulates, which in full propositional logic characterize update operators as choice functions guided by total or partial preorders over possible worlds. Because many useful fragments cannot express every connective (e.g., they often lack closure under disjunction), the KM axioms must be rephrased and supplemented to keep updates rational in these less expressive environments. Our main result is a set of representation theorems: once the KM postulates are adjusted, they capture exactly the update operators generated by suitably constrained total or partial preorders within the fragment. In addition, we clarify how revision works in fragments when partial preorders are allowed and also present concrete, fragment-friendly update operators.

Answer Set Programming (Asp) is used in many real-world applications as an easy-to-use and efficient modeling paradigm. In Asp, rules (containing variables) are instantiated against facts to derive conclusions (i.e., grounding the program). However, a large number of variables and facts (more precisely: domain values) leads to the well-known “grounding bottleneck”: the variables in a rule are instantiated by every combination of domain values, leading to potentially infeasibly large ground programs. This is especially problematic for rules with large rule bodies containing many variables, as standard grounding approaches cause an exponential blowup in the total number of variables in a rule. This paper presents a novel method to overcome this obstacle. In contrast to the standard approach, our technique “decouples” the body atoms, i.e., the instantiation handles each body atom separately. In particular, our procedure translates a non-ground tight program to a ground disjunctive program that is exponential only in the maximum predicate arity, and is thus polynomial if this arity is fixed to a constant. We extend this to non-ground, normal programs, and ultimately use similar ideas to translate non-ground, disjunctive programs to ground epistemic logic programs—all while decoupling the body atoms. We demonstrate the feasibility of this new method experimentally by comparing it to standard Asp technology in terms of grounding size, grounding time and total runtime.

Operational Air Traffic Flow and Capacity Management (ATFCM) balances flight demand with available sector capacity, to ensure safe and efficient operations. Mathematical models enhance operational ATFCM performance by framing demand-capacity balancing as an optimization problem, maximizing efficiency while adhering to safety constraints. However, SOTA research optimizes the aircraft trajectories (called ATFM) or the sector configuration (called DAC) separately. This leaves a research gap of whether joint optimization of ATFM and DAC can bring benefits. We partially address this limitation by introducing a joint ATFCM model with an encoding in Answer Set Programming (ASP). The ASP implementation is evaluated against two baselines applied to our joint model: a SOTA Mixed Integer Programming (MIP) model and an iterative CASA-based heuristic. Computational experiments utilize an instance generator fitted to historical OpenSky Network flight data. Our results indicate that the ASP model outperforms the MIP model, while ASP remains competitive against heuristics on small instances. Furthermore, while DAC has the largest improvement on solving performance compared to rerouting and delaying, unrestricted variants of DAC or rerouting lead to search space thrashing.

Assumption-Based Argumentation (ABA) is a well-established formalism for modelling and reasoning over debates, with a wide range of applications. However, the high computational complexity of core reasoning tasks in ABA poses a significant challenge for its applicability. This issue is further aggravated when ABA frameworks (ABAFs) are instantiated into graph-based argumentation formalisms, such as Dung's Argumentation Frameworks (AFs) and Argumentation Frameworks with Collective Attacks (SETAFs). In knowledge representation and reasoning, a key strategy to address computational intractability is to optimise reasoning over a given knowledge base through divide-and-conquer algorithms. A paradigmatic example of this approach is splitting, where extensions of a given framework are computed incrementally, by restricting the search space to sub-frameworks only, and then combining the obtained results. This approach has been successfully applied to AFs, for which also a parametrised version has been introduced under stable semantics. However, the exponential growth produced by the instantiation might undermine the usefulness of splitting on the argument graphs induced by ABAFs. To address this issue, our work investigates the concept of splitting on the knowledge base rather than on its graph-based instantiation. Furthermore, we generalise splitting to its parametrised version for ABAFs.

We consider a particular subclass of normal programs that we call simple guess-and-check (SGC) programs. SGC programs consist of guess rules (i.e. rules without positive body atoms) and arbitrary constraints. Many simple combinatorial problems such as graph coloring can be encoded via SGC programs. Moreover, constraint-free SGC programs are known to have a close relation to abstract argumentation frameworks. Our main result shows that for SGC programs the notions of strong and uniform equivalence coincide (in contrast to general normal programs), but do not amount to classical equivalence (as is the case of positive programs). Moreover, we study the characteristics of SE-models for SGC programs; this allows to check whether an arbitrary program (part) can be equivalently formulated within the simpler class of SGC programs. Finally, we briefly discuss our results in relation to other classes of programs.

The grounding bottleneck in Answer Set Programming prohibits large instances from being solved. This is caused by a combinatorial explosion in the grounding phase of standard ground&solve systems. A promising alternative is Body-Decoupled Grounding (BDG), which grounds each body predicate on its own. However, BDG faces challenges in terms of worst-case grounding size and limited interoperability with other systems. This paper addresses shortcomings of BDG by introducing FastFound: an alternative foundedness check that significantly reduces grounding sizes, by grounding each predicate on its own. FastFound’s foundedness check is done implicitly, which leads to a quadratic reduction in grounding size. We start by introducing FastFound for tight normal rules, where we observe that this cannot be substantially improved. Then we extend FastFound to head-cycle-free programs and give novel interoperability results for full disjunctive programs. An experimental evaluation on our prototype shows promising results, as we solve more grounding-heavy tasks than both standard ground&solve systems and BDG.

argumentation has proven to be a versatile tool to model and analyze various problems in an argumentative setting. The addition of collective attacks syntactically extends Dung’s original argumentation frameworks (AFs), while retaining the most desirable properties—the resulting class of frameworks is called SETAFs. While most reasoning tasks in the realm of abstract argumentation have been shown to be intractable, real-world instances oftentimes are not entirely random but admit a certain structure that allows for efficient computational shortcuts. In certain cases, we can characterize this structure via an integer parameter, and exploit these insights with advanced algorithmic techniques. A thorough analysis of the computational aspects of SETAFs w.r.t. parameterized algorithms has not yet been conducted. We start the investigation of these approaches by applying the backdoor and treewidth approaches to SETAFs. A backdoor is a part of a problem instance, such that removing the backdoor leads to a simple structure. If we can find such a backdoor and guess the solution on this part (respectively, extensions), the rest of the solution follows almost effortlessly. Similarly, the treewidth of a problem instance is a parameter that characterizes the properties of the instance’s graph structure. Intuitively, the lower the treewidth of a graph, the more “tree-like” it is. Since most argumentation problems become easy on trees, one can exploit low treewidth for efficient algorithms. In this paper, we establish that for SETAFs with constant backdoor sizes general argumentation tasks become efficiently solvable—they are fixed-parameter tractable. We generalize the respective techniques that are known for the special case of Dung-style AFs and show that they also apply to the more general case of SETAFs. In addition, we can show an improvement in the asymptotic runtime compared to earlier approaches for AFs via two-valued guesses instead of the state-of-the-art three-valued approach. Along the way, we point out similarities and interesting situations arising from the more general setting. While treewidth is well-studied in the context of AFs with their graph structure, it cannot be directly applied to the (directed) hypergraphs representing SETAFs. We thus introduce two generalizations of treewidth based on different graphs that can be associated with SETAFs, that is, the primal graph and the incidence graph. We show that while some of these notions allow for parameterized tractability results, reasoning remains intractable for other notions, even if we fix the parameter to a small constant. We present parameterized algorithms for efficient reasoning on SETAFs via tree decompositions by characterizing extensions not only by labeling the arguments, but also by assigning (temporary) labels to the attacks.

The grounding bottleneck poses one of the key challenges that hinders the widespread adoption of answer set programming in industry. Hybrid grounding is a step in alleviating the bottleneck by combining the strength of standard bottom-up grounding with recently proposed techniques where rule bodies are decoupled during grounding. However, it has remained unclear when hybrid grounding shall use body-decoupled grounding (BDG) and when to use standard bottom-up grounding. In this paper, we address this issue by developing automated hybrid grounding: we introduce a splitting algorithm based on data-structural heuristics that detects when to use BDG and when standard grounding is beneficial. We base our heuristics on the structure of rules and an estimation procedure that incorporates the data of the instance. The experiments conducted on our prototypical implementation demonstrate promising results, which show an improvement on hard-to-ground scenarios, whereas on hard-to-solve instances, we approach state-of-the-art performance.

Underlying mechanisms of memorization in LLMs -- the verbatim reproduction of training data -- remain poorly understood. What exact part of the network decides to retrieve a token that we would consider as start of memorization sequence? How exactly is the models' behaviour different when producing memorized sentence vs non-memorized? In this work we approach these questions from mechanistic interpretability standpoint by utilizing transformer circuits -- the minimal computational subgraphs that perform specific functions within the model. Through carefully constructed contrastive datasets, we identify points where model generation diverges from memorized content and isolate the specific circuits responsible for two distinct aspects of memorization. We find that circuits that initiate memorization can also maintain it once started, while circuits that only maintain memorization cannot trigger its initiation. Intriguingly, memorization prevention mechanisms transfer robustly across different text domains, while memorization induction appears more context-dependent.

Strong equivalence between knowledge bases ensures the possibility of replacing one with the other without affecting reasoning outcomes, in any given context. This makes it a crucial property in nonmonotonic formalisms. In particular, the fields of logic programming and abstract argumentation provide primary examples in which this property has been subject to vast investigations. However, while (classes of) logic programs and abstract argumentation frameworks are known to be semantically equivalent in static settings, this alignment breaks in dynamic contexts due to differing notions of update. As a result, strong equivalence does not always carry over from one formalism to the other. In this paper, we carefully investigate this discrepancy and introduce a new notion of strong equivalence for logic programs. Our approach preserves strong equivalence under translation between certain classes of logic programs and both Dung-style and claim-augmented argumentation frameworks, thus restoring compatibility across these formalisms.

In the study of logic programming, notions of equivalence play a significant role. This is due to the fact that under common no semantics, like answer-set programming, two programs sharing the same models (answer sets) does not necessarily yield that they are equivalent in all contexts. Whether this context concerns other program modules or just different data, distinguishes strong from uniform equivalence. We introduce a new notion of equivalence for logic programs under the answer-set semantics that allows to precisely compare and simplify programs that receive input from different sources (i.e., over different alphabets); a setting that previous equivalence notions have not considered, but has some interesting use cases, like data integration or belief merging. Our notion further generalizes relativized equivalence, where equivalence is only required over a parameterized context, and has the core concepts of strong and uniform equivalence as corner cases. We provide a model-theoretic characterization in the spirit of SE-models and establish some theoretical properties including a thorough complexity analysis. Furthermore, using our notion, we can pinpoint the known complexity gap between strong and uniform equivalence, giving insight into why the latter is harder than the former.

Abstract argumentation frameworks (AFs) are a popular formalism for modeling argumentation processes. Thus, various solvers have been developed that can be used to answer decision problems on such frameworks and that regularly compete within the context of competitions. For positive results, these solvers typically provide some sort of model or extension, making it easy to verify their results. However, negative results cannot be easily verified in such a way, creating a need for some sort of certificate to be able to check these results as well. While, for instance, SAT solvers commonly support inconsistency proofs, this is not the case for abstract argumentation solvers yet. In this work, we provide a formal definition of such a certificate for SETAFs, a generalization of Dung AFs, and provide a prototype implementation of a genuine CDCL-based solver for SETAFs that can produce such inconsistency proofs as well as a tool for verifying these proofs.

Answer Set Programming (ASP) is a prominent rule-based language for knowledge representation and reasoning with roots in logic programming and non-monotonic reasoning. The aim to capture the essence of removing (ir)relevant details in ASP programs led to the investigation of different notions, from strong persistence (SP) forgetting, to faithful abstractions, and, recently, strong simplifications, where the latter two can be seen as relaxed and strengthened notions of forgetting, respectively. Although it was observed that these notions are related, especially given that they have characterizations through the semantics for strong equivalence, it remained unclear whether they can be brought together. In this work, we bridge this gap by introducing a novel relativized equivalence notion, which is a relaxation of the recent simplification notion, that is able to capture all related notions from the literature. We provide necessary and sufficient conditions for relativized simplifiability, which shows that the challenging part is for when the context programs do not contain all the atoms to remove. We then introduce an operator that combines projection and a relaxation of (SP)-forgetting to obtain the relativized simplifications. We furthermore present complexity results that complete the overall picture.

Assumption-based argumentation (ABA) is a powerful defeasible reasoning formalism which is based on the interplay of assumptions, their contraries, and inference rules. ABA with preferences (ABA+) generalizes the basic model by allowing qualitative comparison between assumptions. The integration of preferences however comes with a cost. In ABA+, the evaluation under two central and well-established semantics---grounded and complete semantics---is not guaranteed to yield an outcome. Moreover, while ABA frameworks without preferences allow for a graph-based representation in Dung-style frameworks, an according instantiation for general ABA+ frameworks has not been established so far. In this work, we tackle both issues: First, we develop a novel abstract argumentation formalism based on set-to-set attacks. We show that our so-called Hyper Argumentation Frameworks (HYPAFs) capture ABA+. Second, we propose relaxed variants of complete and grounded semantics for HYPAFs that yield an extension for all frameworks by design, while still faithfully generalizing the established semantics of Dung-style Argumentation Frameworks. We exploit the newly established correspondence between ABA+ and HYPAFs to obtain variants for grounded and complete ABA+ semantics that are guaranteed to yield an outcome. Finally, we discuss basic properties and provide a complexity analysis. Along the way, we settle the computational complexity of several ABA+ semantics.

The visualization of argumentation frameworks (AFs) is crucial for enabling a wide applicability of argumentative tools. However, their visualization is often considered only as an accompanying part of tools for computing semantics and standard graphical representations are used. We introduce a new visualization technique that draws an AF, together with an extension (as part of the input), as a 3-layer graph layout. Our technique supports the user to more easily explore the visualized AF, better understand extensions, and verify algorithms for computing semantics. To optimize the visual clarity and aesthetics of this layout, we propose to minimize edge crossings in our 3-layer drawing. We do so by an exact ILP-based approach, but also propose a fast heuristic pipeline. Via a quantitative evaluation, we show that the heuristic is feasible even for large instances, while producing at most twice as many crossings as an optimal drawing in most cases.

Answer Set Programming (ASP) is a prominent problem-modeling and solving framework, whose solutions are called answer sets. Epistemic logic programs (ELP) extend ASP to reason about all or some answer sets. Solutions to an ELP can be seen as consequences over multiple collections of answer sets, known as world views. While the complexity of propositional programs is well studied, the non-ground case remains open. This paper establishes the complexity of non-ground ELPs. We provide a comprehensive picture for well-known program fragments, which turns out to be complete for the class NEXPTIME with access to oracles up to SigmaP2. In the quantitative setting, we establish complexity results for counting complexity beyond #EXP. To mitigate high complexity, we establish results in case of bounded predicate arity, reaching up to the fourth level of the polynomial hierarchy. Finally, we provide ETH-tight runtime results for the parameter treewidth, which has applications in quantitative reasoning, where we reason on (marginal) probabilities of epistemic literals.

Online discussion platforms are a vital part of the public discourse in a deliberative democracy. However, how to interpret the outcomes of the discussions on these platforms is often unclear. In this paper, we propose a novel and explainable method for selecting a set of most representative, consistent points of view by combining methods from computational social choice and abstract argumentation. Specifically, we model online discussions as abstract argumentation frameworks combined with information regarding which arguments voters approve of. Based on ideas from approval-based multiwinner voting, we introduce several voting rules for selecting a set of preferred extensions that represents voters' points of view. We compare the proposed methods across several dimensions, theoretically and in numerical simulations, and give clear suggestions on which methods to use depending on the specific situation.