Interpretations of logical formulas over semirings 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 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 optConfVal and optConf. We show that for general propositional formulas in negation normal form, optConfVal and optConf are in ${\mathrm{FP}}^{\mathrm{NP}}$. We investigate optConf when the input formula $\varphi$ is represented as a CNF. For CNF formulae, we first derive an upper bound on optConfVal 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 optConfVal is at most $1/4^{m-r}$. Building on this we establish that optConfVal 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 optConfVal. We establish similar complexity results for these optimization problems over other semirings including tropical, fuzzy, and access control semirings.

翻译：在幺半群上对逻辑公式的解释在计算机科学的多个领域具有应用，包括逻辑学、人工智能、数据库和安全领域。这种解释提供了超越语句真伪的丰富信息。此类幺半群的例子包括Viterbi幺半群、最小-最大或访问控制幺半群、热带幺半群和模糊幺半群。本文研究了幺半群上约束优化问题的复杂性。我们研究的通用优化问题如下：给定一个包含n个变量的命题公式$\varphi$和一个幺半群$(K,+,\cdot,0,1)$，求$\varphi$在$K$上所有可能解释中的最大值。这可以看作经典可满足性问题的一种推广。一个相关问题是寻找达到该最大值的解释。本文首先关注这些在Viterbi幺半群上的优化问题，我们将其称为optConfVal和optConf。我们证明，对于否定范式中的一般命题公式，optConfVal和optConf属于${\mathrm{FP}}^{\mathrm{NP}}$类。当输入公式$\varphi$表示为CNF时，我们研究了optConf。对于CNF公式，我们首先推导出optConfVal的一个上界，该上界是最大可满足子句数量的函数。特别地，我们证明：如果一个包含m个子句的CNF公式中最大可满足子句数为r，则其optConfVal至多为$1/4^{m-r}$。基于此，我们证明CNF公式的optConfVal对于复杂度类${\mathrm{FP}}^{\mathrm{NP}[\log]}$是难的。我们还设计了多项式时间近似算法，并证明了optConfVal的不可近似性。对于其他幺半群（包括热带幺半群、模糊幺半群和访问控制幺半群）上的这些优化问题，我们建立了类似的复杂性结果。