An Abstract View on Optimizations in Propositional Frameworks

TL;DR

This paper introduces a unifying framework called weight systems that consolidates various optimization paradigms in automated reasoning, simplifying analysis and fostering interoperability among different approaches.

Contribution

It proposes a novel unifying framework for optimization statements in automated reasoning, bridging diverse paradigms and aiding formal analysis and solver development.

Findings

Eliminates syntactic distinctions between optimization paradigms

Highlights essential similarities and differences among frameworks

Facilitates development of translational solvers

Abstract

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