Semiring-valued satisfiability

Abstract

In this paper we show that a certain type of satisfiability problem for a set of propositional sentences with a many-valued semantics can be transformed into an equivalent commutative semiring-based constraint satisfaction problem (CSP). This is in analogy to the classical satisfiability problem (SAT) being an instance of a CSP. The characteristic matrix of the logic is a De Morgan lattice, seen as a commutative semiring. The levels of satisfiability is determined by the natural partial order on the semiring. The aim of a many-valued satisfiability problem may be to maximize the level of satisfaction, or to find a state in which a predetermined minimum level of satisfaction is attained. These aims can both be formulated as constraint problems. Many-valued satisfiability problems occur naturally in an epistemic context of knowledge and beliefs about the state of a system S. The possible states of S are determined by the ontological constraints on S. The states are partially ordered by the beliefs of an agent observing the system, and trying to determine its current state. Unlike the ontological constraints on S, which are not defeasible, epistemic constraints are assigned degrees of plausibility, reflecting the reliability of the source or observation. The aim of the agent may be to find a possible state in which the degree of plausibility of the combination of its epistemic constraints is maximized, or to find a sufficiently plausible state. Such a state represents a best approximation of the current state of the system.