Unifying Framework for Optimizations in non-boolean Formalisms

TL;DR

This paper introduces a unifying framework called extended weight systems that standardizes the expression of optimization problems across various automated reasoning paradigms, revealing their core similarities and differences.

Contribution

It proposes a formal, unified framework for diverse optimization languages in automated reasoning, enabling better comparison and understanding of their properties.

Findings

Unified framework clarifies relationships between paradigms

Formal properties of systems are derived and analyzed

Framework supports multiple reasoning languages within a single formalism

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 towards 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. Recall integer linear programming, MaxSAT, optimization satisfiability modulo theory, and (constraint) answer set programming. These paradigms vary significantly in their languages in ways they express quality conditions on computed solutions. Here we propose a unifying framework of so called extended weight systems that eliminates syntactic distinctions between paradigms. They allow us to see essential similarities and differences between optimization statements provided by distinct automated reasoning languages. We also study formal properties of the proposed systems that immediately translate into formal properties of paradigms that can be captured within our framework. Under consideration in Theory and Practice of Logic Programming (TPLP).