Integrating diverse formalisms into modular knowledge representation systems offers increased expressivity, modeling convenience and computational benefits. We introduce concepts of abstract modules and abstract modular systems to study general principles behind the design and analysis of model-finding programs, or solvers, for integrated heterogeneous multi-logic systems. We show how abstract modules and abstract modular systems give rise to transition systems, which are a natural and convenient representation of solvers pioneered by the SAT community. We illustrate our approach by showing how it applies to answer set programming and propositional logic, and to multi-logic systems based on these two formalisms.
Intelligent Systems Department（智能系统部）；Computer Science Institute（计算机科学研究所）；Leipzig University（莱比锡大学）
MatrixX is a solver for Abstract Argumentation Frameworks. Offensive and defensive properties of an Argumentation Framework are notated in a matrix style. Rows and columns of this matrix are systematically reduced by the solver. This procedure is implemented through the use of hash maps in order to accelerate calculation time. MatrixX works for stable and complete semantics and was designed for the ICCMA 2021 competition.
Vector Symbolic Algebras for the Abstraction and Reasoning Corpus
Centre for Theoretical Neuroscience（理论神经科学中心）；David R. Cheriton School of Computer Science（大卫·R·切里顿计算机科学学院）；University of Waterloo（滑铁库大学）；Department of Philosophy（哲学系）；Department of Systems Design Engineering（系统设计工程系）
University of Koblenz-Landau（科布伦茨-兰道大学）；University of Brescia（布雷西亚大学）；University of Huddersfield（哈德斯菲尔德大学）
We present Fudge, an abstract argumentation solver that tightly integrates satisfiability solving technology to solve a series of abstract argumentation problems. While most of the encodings used by Fudge derive from standard translation approaches, Fudge makes use of completely novel encodings to solve the skeptical reasoning problem wrt. preferred semantics and problems wrt. ideal semantics.
Computer programs, so-called solvers, for solving the well-known Boolean satisfiability problem (Sat) have been improving for decades. Among the reasons, why these solvers are so fast, is the implicit usage of the formula's structural properties during solving. One of such structural indicators is the so-called treewidth, which tries to measure how close a formula instance is to being easy (tree-like). This work focuses on logic-based problems and treewidth-based methods and tools for solving them. Many of these problems are also relevant for knowledge representation and reasoning (KR) as well…
University of Angers（昂热大学）；University of Nantes（南特大学）
Cooperation among constraint solvers is difficult because different solving paradigms have different theoretical foundations. Recent works have shown that abstract interpretation can provide a unifying theory for various constraint solvers. In particular, it relies on abstract domains which capture constraint languages as ordered structures. The key insight of this paper is viewing cooperation schemes as abstract domains combinations. We propose a modular framework in which solvers and cooperation schemes can be seamlessly added and combined. This differs from existing approaches such as SMT w…
Counterexample guided abstraction refinement (CEGAR) represents a powerful symbolic technique for various tasks such as model checking and reachability analysis. Recently, CEGAR combined with Boolean satisfiability (SAT) has been applied for multi-agent path finding (MAPF), a problem where the task is to navigate agents from their start positions to given individual goal positions so that the agents do not collide with each other. The recent CEGAR approach used the initial abstraction of the MAPF problem where collisions between agents were omitted and were eliminated in subsequent abstraction…
University of the Chinese Academy of Sciences（中国科学院大学）；Huazhong University of Science and Technology（华中科技大学）；National University of Singapore（新加坡国立大学）
Abstract visual reasoning connects mental abilities to the physical world, which is a crucial factor in cognitive development. Most toddlers display sensitivity to this skill, but it is not easy for machines. Aimed at it, we focus on the Raven Progressive Matrices Test, designed to measure cognitive reasoning. Recent work designed some black-boxes to solve it in an end-to-end fashion, but they are incredibly complicated and difficult to explain. Inspired by cognitive studies, we propose a Multi-Granularity Modularized Network (MMoN) to bridge the gap between the processing of raw sensory infor…
Integer programming problems (IPs) are challenging to be solved efficiently due to the NP-hardness, especially for large-scale IPs. To solve this type of IPs, Large neighborhood search (LNS) uses an initial feasible solution and iteratively improves it by searching a large neighborhood around the current solution. However, LNS easily steps into local optima and ignores the correlation between variables to be optimized, leading to compromised performance. This paper presents a general adaptive constraint partition-based optimization framework (ACP) for large-scale IPs that can efficiently use a…
Intelligent robots need to achieve abstract objectives using concrete, spatiotemporally complex sensory information and motor control. Tabula rasa deep reinforcement learning (RL) has tackled demanding tasks in terms of either visual, abstract, or physical reasoning, but solving these jointly remains a formidable challenge. One recent, unsolved benchmark task that integrates these challenges is Mujoban, where a robot needs to arrange 3D warehouses generated from 2D Sokoban puzzles. We explore whether integrated tasks like Mujoban can be solved by composing RL modules together in a sense-plan-a…
