An Abstract View on Optimizations in Propositional Frameworks
This work addresses the challenge of fragmented optimization approaches in automated reasoning and knowledge representation for researchers, providing a tool for formal analysis and bridging frameworks, though it is incremental in nature.
The authors tackled the problem of diverse optimization statements in automated reasoning paradigms by proposing a unifying framework called weight systems, which eliminates syntactic distinctions and reveals essential similarities and differences, offering simplifying and explanatory potential for studies in optimization and modularity.
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.