Semiring-induced propositional logic: Definition and basic algorithms

Abstract

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 to incorporate the three features that are common in all modern SAT solvers: backjumping, learning and restarts. As a result, we obtain an extremely simple algorithm that captures, unifies and extends in a well-defined logical language several techniques that are valid for arbitrary semirings. © 2010 Springer-Verlag.