Combining Stochastic Constraint Optimization and Probabilistic Programming: From Knowledge Compilation to Constraint Solving
Award ID(s):
NSF-PAR ID:
10053971
Author(s) / Creator(s):
; ; ; ; ;
Date Published:
Journal Name:
Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP)
Format(s):
Medium: X
Interpretations of logical formulas over semirings (other than the Boolean semiring) have applications in various areas of computer science including logic, AI, databases, and security. Such interpretations provide richer information beyond the truth or falsity of a statement. Examples of such semirings include Viterbi semiring, min-max or access control semiring, tropical semiring, and fuzzy semiring. The present work investigates the complexity of constraint optimization problems over semirings. The generic optimization problem we study is the following: Given a propositional formula $\varphi$ over $n$ variable and a semiring $(K,+,\cdot,0,1)$, find the maximum value over all possible interpretations of $\varphi$ over $K$. This can be seen as a generalization of the well-known satisfiability problem (a propositional formula is satisfiable if and only if the maximum value over all interpretations/assignments over the Boolean semiring is 1). A related problem is to find an interpretation that achieves the maximum value. In this work, we first focus on these optimization problems over the Viterbi semiring, which we call \optrustval\ and \optrust. We first show that for general propositional formulas in negation normal form, \optrustval\ and {\optrust} are in ${\mathrm{FP}}^{\mathrm{NP}}$. We then investigate {\optrust} when the input formula $\varphi$ is represented in the conjunctive normal form. For CNF formulae, we first derive an upper bound on the value of {\optrust} as a function of the number of maximum satisfiable clauses. In particular, we show that if $r$ is the maximum number of satisfiable clauses in a CNF formula with $m$ clauses, then its $\optrust$ value is at most $1/4^{m-r}$. Building on this we establish that {\optrust} for CNF formulae is hard for the complexity class ${\mathrm{FP}}^{\mathrm{NP}[\log]}$. We also design polynomial-time approximation algorithms and establish an inapproximability for {\optrustval}. We establish similar complexity results for these optimization problems over other semirings including tropical, fuzzy, and access control semirings.