Semiring-Induced Propositional Logic: Definition and Basic Algorithms

In this paper we introduce an extension of propositional logic that allows clauses to be weighted with values from a generic semiring. The main interest of this extension is that different instantiations of the semiring model different interesting computational problems such as finding a model, counting the number of models, finding the best model with respect to an objective function, finding the best model with respect to several independent objective functions, or finding the set of pareto-optimal models with respect to several objective functions. Then we show that this framework unifies several solving techniques and, even more importantly, rephrases them from an algorithmic language to a logical language. As a result, several solving techniques can be trivially and elegantly transferred from one computational problem to another. As an example, we extend the basic DPLL algorithm to our framework producing an algorithm that we call SDPLL. Then we enhance the basic SDPLL in order t...

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Javier Larrosa, Albert Oliveras, Enric Rodríguez-Carbonell
• Keywords: Automated Reasoning, Independent Objective Functions, Logical Language, LPAR 2010, Objective Functions