Constraint Optimization over Semirings
A. Pavan, Kuldeep S. Meel, N. V. Vinodchandran, Arnab, Bhattacharyya

TL;DR
This paper studies the complexity of constraint optimization problems over various semirings, generalizing satisfiability, and provides complexity bounds, algorithms, and inapproximability results for different semiring-based formulas.
Contribution
It introduces the first complexity analysis of constraint optimization over semirings, including bounds, algorithms, and hardness results for various semiring interpretations.
Findings
optConfVal and optConf are in FP^NP for propositional formulas in negation normal form.
For CNF formulas, optConfVal is at most 1/4^{m-r}, where r is the maximum satisfiable clauses.
optConfVal for CNF formulas is hard for FP^NP[log], with polynomial-time approximation algorithms and inapproximability results.
Abstract
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 over variable and a semiring , find the maximum value over all possible interpretations of over . 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
Constrained Optimization Over Semirings· youtube
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Formal Methods in Verification
Constraint Optimization over Semirings††thanks: The authors decided to forgo the old convention
of alphabetical ordering of authors in favor of a randomized ordering, denoted by ⓡ. The publicly verifiable record of the randomization is available at https://www.aeaweb.org/journals/policies/ random-author-order/search. An abridged version of the paper appeared in AAAI 2023.
A. Pavan ⓡ
Iowa State Univerity
Kuldeep S. Meel ⓡ
National University of Singapore, Singapore
N. V. Vinodchandran ⓡ
University of Nebraska-Lincoln
Arnab Bhattacharyya
National University of Singapore, Singapore
Abstract
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 over variable and a semiring , find the maximum value over all possible interpretations of over . 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 and .
We first show that for general propositional formulas in negation normal form, and are in . We then investigate when the input formula is represented in the conjunctive normal form. For CNF formulae, we first derive an upper bound on the value of as a function of the number of maximum satisfiable clauses. In particular, we show that if is the maximum number of satisfiable clauses in a CNF formula with clauses, then its value is at most . Building on this we establish that for CNF formulae is hard for the complexity class . We also design polynomial-time approximation algorithms and establish an inapproximability for . We establish similar complexity results for these optimization problems over other semirings including tropical, fuzzy, and access control semirings.
1 Introduction
Classically, propositional formulae are interpreted over the Boolean semiring which is the standard semantics for the logical truth. In this setting, the variables take one of the two values T (true) or F (false). However, it is natural to extend the semantics to other semirings. Here, the idea is to interpret logical formulae when the variables take values over a semiring . Such interpretations provide richer information beyond the truth or falsity of a statement and have applications in several areas such as databases, AI, logic, and security (see [ILJ89, FR97, Zim97, CWW00, Cui02, GT20] and references therein). In particular, semiring provenance analysis has been successfully applied in several software systems, such as Orchestra and Propolis (see, e.g., [ADT11, DMRT14, FGT08, Gre11, Tan13]).
Examples of semirings that are studied in the literature include Viterbi semiring, fuzzy semiring, min-max or access control semiring, and tropical semiring. Semantics over the Viterbi semiring has applications in database provenance, where is interpreted as a confidence score [GT20, GKT07, Tan17, GM21], in probabilistic parsing, in probabilistic CSPs, and in Hidden Markov Models [Vit67, KM03, BMR95]. The access control semiring can be used as a tool in security specifications [GT20]. Other semirings of interest include the tropical semiring, used in cost analysis and algebraic formulation for shortest path algorithms [Moh02], and fuzzy semirings used in the context of fuzzy CSPs [BMR95].
Optimization problems over Boolean interpretations have been central in many application as well as foundation areas. Indeed, the classical satisfiability problem is determining whether a formula has an interpretation/assignment over the Boolean semiring that evaluates to True. Even though semiring semantics naturally appear in a variety of applications, the optimization problems over semirings, other than the Boolean semiring, have not received much attention.
In this work, we introduce and investigate the complexity of optimization problems over semiring semantics. Let be a semiring with a total order over and be a propositional formula over a set of variables. A -interpretation is a function from to . Such an interpretation can be naturally extended to formula , which we denote by . We study the following computational problem: Given a propositional formula in negation normal form over a set of variables, compute the maximum value of over all possible interpretations . We call this problem . A related problem, denoted , is to compute an interpretation that maximizes . Refer to Section 2 for a precise formulation of these problems.
There has been a rich history of work which formulated the notion of CSP over semirings and investigated local consistency algorithms in the general framework [Bis04, BG06, BMR95, BMR97, BMR*+*99, MRS06]. These works did not involve interpretations and did not focus on the computational complexity of the above-defined problems. Relatedly, the computational complexity of sum-of-product problems over semirings has been studied recently [EK21]. However, the problems they study are different from ours. To the best of our knowledge, optimization problems and that we consider over semirings have not been studied earlier and there are no characterizations of their computational complexity.
1.1 Our Results
We comprehensively study the computational complexity of and the related problem over various semirings such as Viterbi semiring, tropical semiring, access control semiring and fuzzy semiring, from both an algorithmic and a complexity-theoretic viewpoint. When the underlying semiring is the Viterbi semiring, we call these problems and . Our results can be summarized as follows:
We establish that both and are in the complexity class . The crucial underlying observation is that even though maps to real values in the range ; the solution to can be represented using polynomially many bits. We then draw upon connections to Farey sequences to derive an algorithm with polynomially many calls (Theorem 3.2). 2. 2.
For CNF formulas, we establish an upper bound on as a function of the number of maximum satisfiable clauses (Theorem 3.7). 3. 3.
We also establish a lower bound on the complexity of and . In particular, we show that both the problems are hard for the complexity class . To this end, we demonstrate a reduction from MaxSATVal to ; this reduction crucially relies on the above-mentioned upper bound on in terms of the number of maximum satisfiable clauses (Theorem 3.9). 4. 4.
We design a polynomial-time approximation algorithm for and establish an inapproximability result. In particular, for 3-CNF formulas with clauses, we design a -approximation algorithm and show that the approximation factor can not be improved to unless P = NP (Theorems 4.3 and 4.5). 5. 5.
Finally, we show that for the access control semiring, the complexity of these optimization problems is equivalent to the corresponding problems over Boolean semiring (Theorem 5.3).
Remark 1**.**
Since Viterbi semiring and tropical semiring are isomorphic via the mapping , results established for Viterbi semiring also hold for the tropical semiring. Fuzzy semiring can be seen as an “infinite refinement” of access control semiring with the same algebraic structure, results that we establish for access control semiring also hold for fuzzy semiring.
Organization. The rest of the paper is organized as follows. We give the necessary notation and definitions in Section 2. Section 3 details our results on the computational complexity of and . Section 4 deals with approximate algorithms and the hardness of approximation of . In Section 5, we give complexity results for optimization problems for the access control semiring. Finally, we conclude in Section 6.
2 Preliminaries
We assume that the reader is familiar with definition of a semiring. We denote a generic semiring by where is the underlying set. For interpreting formulas over , we will add a “negation” function \mbox{\daleth}:K\rightarrow K. We assume is a bijection so that \mbox{\daleth}(\mbox{\daleth}(x))=x, and \mbox{\daleth}(0)=1. For ease of presentation, we use the most natural negation function (depending on the semiring). However, many of our results hold for very general interpretations of negation. Finally, as our focus is on optimization problems, we will also assume a (natural) total order on the elements of .
For a set of variables, we associate the set . We call the literals and formulas we consider are propositional formulas over in negation normal form. We also view a propositional formula in negation normal form as a rooted directed tree wherein each leaf node is labeled with a literal, 1, or 0 and each internal node is labeled with conjunction or disjunction . Note that viewing as a tree ensures a similar size as its string representation. We call the tree representing the formula as formula tree and denote it with . For a propositional formula , in negation normal form we use to denote the size of the formula, i.e. the total number of occurrences of each variable and its negation. When is in CNF form, denotes the number of clauses. We interpret a propositional formula over a semiring by mapping the variables to and naturally extending it. Formally, a -interpretation is a function . We extend to an arbitrary propositional formula in negation normal form, which is denoted by ( stands for ‘semantics’), as follows.
2. -
\mathsf{Sem}(\neg x,\pi)=\mbox{\daleth}(\pi(x)) 3. -
4. -
2.1 Optimization Problems and Complexity Classes
For a formula , we define as
[TABLE]
where is taken over all possible -interpretations from to .
Definition 2.1** ( and ).**
Given a propositional formula in negation normal form, the problem is to compute . The problem is to compute a -interpretation that achieves , i.e, output so that .
Notice that when is the Boolean semiring (with ordering and standard negation interpretation), is the well-known satisfiability problem: the formula is satisfiable if and only if . Also, the problem is to output a satisfying assignment if the formula is satisfiable.
In this work, we consider the following semirings.
Viterbi semiring . As mentioned, the Viterbi semiring has applications in database provenance, where is interpreted as confidence scores, in probabilistic parsing, in probabilistic CSPs, and in Hidden Markov Models. 2. 2.
The tropical semiring .
The tropical semiring is isomorphic to the Viterbi semiring via the mapping . 3. 3.
The fuzzy semiring . 4. 4.
Access control semiring . Intuitively, each is associated with an access control level with natural ordering. Here 0 corresponds to public access and corresponds to no access at all. is the set .
Most of our focus will be on complexity of and problems over the Viterbi semiring. We call the corresponding computational problems and respectively. We call the extended interpretation function as in this case.
Definition 2.2** ( and ).**
Given a propositional formula in CNF form, the problem is to compute an assignment of that satisfies the maximum number of clauses. Given a propositional formula in CNF form, the problem is to compute the maximum number of clauses of that can be satisfied.
We need a notion of reductions between functional problems. We use the notion of metric reductions introduced by Krentel [Kre88].
Definition 2.3** (Metric Reduction).**
For two functions , we say that metric reduces to if there are polynomial-time computable functions and where (the reduction function) and so that for any , .
Definition 2.4**.**
For a function , denotes the class of functions that can be solved in polynomial-time with queries to an oracle where is the size of the input. When is some polynomial, we denote the class by .
Metric reductions are used to define notions of completeness and hardness for function classes and . The following result due to Krentel [Kre88] characterizes the complexity of the problem.
Theorem 2.5** ([Kre88]).**
* is complete for under metric reductions.*
The following proposition is a basic ingredient in our results. It can be proved using basic calculus.
Proposition 1**.**
Let where are non-negative integers, the maximum value of over the domain is attained when . The maximum value of the function is .
3 Computational Complexity of Confidence Maximization
For semantics over Viterbi semiring we assume the standard closed world semantics and use the negation function \mbox{\daleth}(x)=1-x. Thus we have . However, our upper bound proofs go through for any reasonable negation function. We discuss this in Remark 2.
Since can be computed in polynomial time, is at least as hard as . The following observation states that computing and are -hard.
Observation 3.1**.**
For a formula , if and only if satisfiable. Hence both and are NP-hard.
While both and are -hard, we would like to understand their relation to other maximization problems. In the study of optimization problems, the complexity classes and play a key role. In this section, we investigate both upper and lower bounds for these problems in relation to the classes and .
An Illustrative Example.
We first provide an illustrative example that gives an idea behind the upper bound. Consider the formula . Clearly, the formula is not satisfiable. Over the Viterbi semiring the value of the by distributivity. This is maximized when (by Proposition 1) and or and , leading to an optimum value of . In the following section, we show that the computation of reduces to maximization over a set of polynomial terms wherein each polynomial term corresponds to a proof tree, which we define. While the number of polynomial terms could be exponential, we use an NP oracle to binary search for the term that gives the maximum value.
3.1 An Upper Bound for General Formulae
We show that and can be computed in polynomial-time with oracle queries to an language.
Theorem 3.2**.**
* for formulas in negation normal form is in .*
Proof Idea: In order to show that is in , we use a binary search strategy using a language in . One of the challenges is that the confidence value could potentially be any real number in and thus apriori we may not be able to bound the number of binary search queries. However, we first argue that for any formula on variables and with size , is a fraction of the form where . Ordered fractions of such form are known as Farey sequence of order (denoted as ). Thus our task is to do a binary search over with time complexity . However, in general binary search for an unknown element in the Farey sequence with time complexity appears to be unknown. We overcome this difficulty by using an oracle to aid the binary search. We will give the details now.
Definition 3.3**.**
Let be a propositional formula in negation normal form with size . Let be its formula tree. A proof tree of is a subtree obtained by the following process: for every OR node , choose one of the sub-trees of . For every AND node , keep all the subtrees.
Note that in a proof tree every OR node has only one child.
Definition 3.4**.**
Let be a propositional formula in negation normal form and let be a proof tree. We define the proof tree polynomial by inductively defining a polynomial for the subtree at every node (denoted by ): If the node is a variable , the polynoimal is and if it is , the polynomial is . If is an AND node with children , then . If is an OR node with a child , then .
Claim 3.4.1**.**
Let be a propositional formula in negation normal form and let be a proof tree of .
The proof tree polynomial is of the form
[TABLE]
where 2. 2.
For a -interpretation ,
[TABLE] 3. 3.
Both and can be computed in polynomial-time. 4. 4.
**
Proof.
Item (1) follows from the definition of the proof tree polynomial and a routine induction and the fact that the size of the formula is . Item (2) follows from the definitions.
Note that the polynomial can be maximized by maximizing each of the individual terms . By Proposition 1, the maximum value for a polynomial of this form is achieved at . Thus the interpretation is an optimal -interpretation that can be computed in polynomial-time. Since , also can be computed in polynomial-time. Item (4) follows from Item (3), by substituting the values for in the polynomial . ∎
The next claim relates of the formula to of its proof trees. The proof of this claim follows from the definition of proof tree and standard induction.
Claim 3.4.2**.**
For a formula ,
[TABLE]
where maximum is taken over all proof trees of . If is the proof tree for which is maximized, then .
The above claim states that can be computed by cycling through all proof trees of and computing . Since there could be exponentially many proof trees, this process would take exponential time. Our task is to show that this process can be done in . To do this we establish a claim that restricts values that can take. We need the notion of Farey sequence.
Definition 3.5**.**
For any positive integer , the Farey sequence of order , denoted by , is the set of all irreducible fractions with arranged in increasing order.
Claim 3.5.1**.**
For a propositional formula , belongs to the Farey sequence . 2. 2.
For any two fractions and from ,
Proof.
By Claim 3.4.2, equals , for some proof tree . By Item (4) of Claim 3.4.1 this value is a product of fractions, where the denominator of each fraction is of the form where and are non-negative integers. Since , each denominator is at most , and thus the denominator of the product is bounded by . Since the numerator is at most the denominator, the claim follows.
For the proof of the second part, let and , . Now . Since , we have . Since , are all integers, . Thus .
∎
Consider the following language
[TABLE]
Claim 3.5.2**.**
* is in .*
Proof.
Consider the following non-deterministic machine . On input , guesses a proof tree of : for every OR node, non-deterministically pick one of the subtrees. For , compute and accept if . This can be done in polynomial-time using Item (3) of Claim 3.4.1. The correctness of this algorithm follows from Claim 3.4.2. ∎
We need a method that given two fractions and and an integer , outputs a fraction , and . We give an algorithm that makes queries to the oracle to achieve this. We first define the language . For this we fix any standard encoding of fraction using the binary alphabet. Such an encoding will have bit representation for any fraction in .
[TABLE]
The following claim is easy to see.
Claim 3.5.3**.**
.
Now we are ready to prove the Theorem 3.2.
Proof.
(of Theorem 3.2). The algorithm performs a binary search over the range by making adaptive queries to the language starting with . At any iteration of the binary search, we have an interval and with the invariant . The binary search stops when the size of the interval . Since each iteration of the binary search reduces the size of the interval by a factor of 2, the search stops after making queries to . The invariant ensures that is in this interval. Moreover, (by item (1) of Claim 3.5.1) and there are no other fractions from in this interval (by item (2) of Claim 3.5.1). Now, by making queries to with , , , we can construct the binary representation of the unique fraction in that lies between and which is . ∎
Next we show the optimal -interpretation can also be computed in polynomial time with queries to an NP oracle.
Theorem 3.6**.**
* for formulas in negation normal form can be computed in .*
Proof.
Let be a propositional formula in negation normal form. We use a prefix search over the encoding of proof trees of using an language to isolate a proof tree such that . For this, we fix an encoding of proof trees of . Consider the following language :
[TABLE]
Claim 3.6.1**.**
* is in * NP*.*
Proof.
Consider a non-deterministic machine that guesses a , verifies that encodes a proof tree of , and accepts if . By item (3) of Claim 3.4.1, can be computed in polynomial time. ∎
To complete the proof Theorem 3.6, given a propositional formula , we first use algorithm from Theorem 3.2 to compute . Now we can construct a proof tree of so that by a prefix search using language . Now by Claim 3.4.1, we can compute a -interpretation so that . Thus is an optimal -interpretation for , by Claim 3.4.2. ∎
Remark 2**.**
We revisit the semantics of negation. As stated earlier, by assuming the closed world semantics, we have \mbox{\daleth}(x)=1-x. We note that this assumption is not strictly necessary for the above proof to go through. Recall that Item (1) of Claim 3.4.1 states that the proof tree polynomial is of the form . For a general negation function , the proof tree polynomial is of the form \prod x_{i}^{a_{i}}(\mbox{\daleth}(x_{i}))^{b_{i}}. Now if the maximum value of a term x^{a}(\mbox{\daleth}(x))^{b} can be found, for example when is an explicit differentiable function, the result will hold.
3.2 Relation to for CNF Formulae
In this section we study the problem for CNF formulae and establish its relation to the problem. We first exhibit an upperbound on the using the maximum number of satisfiable clauses. Building on this result, in Section 3.3 we show that for CNF formulae is hard for the complexity class .
We first define some notation that will be used in this and next subsections. Let be a CNF formula and let be an optimal -interpretation. For each clause from , let be the value achieved by this interpretation, i.e . Observe that since is a disjunction of literals, . For a clause , let
[TABLE]
In the above, if there are multiple maximums, we take the smallest literal as (By assuming an order . Observe that, since we are working over the Viterbi semiring, . A literal is maximizing literal for a clause , if .
Since is a CNF formula, for any -interpretation is of the form . Given a collection of clauses from , the contribution of to is defined as .
The following theorem provides an upperbound on using . This is the main result of this section.
Theorem 3.7**.**
Let be a CNF formula with clauses. Let be the maximum number of clauses that can be satisfied. Then .
Proof.
Let be an optimal -interpretation for . A clause is called low-clause if , is called a high-clause of , and is a neutral-clause if . Let , , and respectively denote the number of low, high, and neutral clauses.
We start with the following claim that relates the number of neutral clauses and the number of high-clauses to .
Claim 3.7.1**.**
**
Proof.
Suppose that the number of low-clauses is strictly less than , thus number of high-clauses is more than .
For a variable , let
[TABLE]
and
[TABLE]
That is is the number of neutral clauses for which is the maximizing literal and is the number of neutral clauses for which is the maximizing literal.
Consider the truth assignment that is constructed based on the following three rules: (1) For every high-clause , set to True and to False, 2) For every variable , if one of or is not zero, then if , then set to True, otherwise set to False. (3) All remaining variables are consistently assigned arbitrary to True/False values.
We argue that this is a consistent assignment: I.e, for every literal , both and are not assigned the same truth value. Consider a literal . If there is a high clause such that , then this literal is assigned truth value True and is assigned False. In this case, since , . Thus can not be maximizing literal for any high-clause and thus Rule (1) does not assign True to . Again, since , there is no neutral-clause such that or . Thus Rule (2) does not assign a truth value to either of or . Since and are assigned truth values, Rule (3) does not assign a truth value to or .
Consider a variable where at least one of or is not zero. In this case or is maximizing literal for a neutral clause. Thus and neither nor is maximizing literal for a high-clause. Thus Rule (1) does not assign a truth value to or . Now is True if and only if , thus the truth value assigned to (and ) is consistent. Since Rule (3) consistently assigns truth values of literals that are not covered by Rules (1) and (2), the constructed assignment is a consistent assignment.
For every high clause , literal is set to true. Thus the assignment satisfies all the high-clauses. Consider a variable and let be the (non-empty) collection of neutral clauses for which either or is a maximizing literal. As is assigned True if and only if , at least half the clauses from are satisfied. Thus this assignment satisfies at least clauses. Since is the maximum number of satisfiable clauses, the claim follows. ∎
For a literal , let be the number of low-clauses for which is a maximizing literal, i.e,
[TABLE]
and
[TABLE]
We show the following relation between and .
Claim 3.7.2**.**
For every literal , .
Proof.
[TABLE]
Now suppose that for some literal . Let be the variable corresponding to the literal . Note that
[TABLE]
where . Consider a new interpretation where , and for all other literals the value of is the same as the value of . Now
[TABLE]
The last inequality follows because and the assumption that . Since for every , combining the above inequality with Equation 1, we obtain that and thus is not an optimal -interpretation. This is a contradiction. Thus ∎
We next bound the contribution of neutral and low clauses to . For every neutral clause , , thus we have the following observation.
Observation 3.8**.**
The contribution of neutral clauses to is exactly .
We establish the following claim.
Claim 3.8.1**.**
[TABLE]
Proof.
By Observation 3.8, the contribution of neutral clauses to is . Next we show that the contribution of all high and low clauses is exactly.
[TABLE]
For this we first claim that exactly one of or contribute to the above product. For this it suffices to prove that for every literal exactly one of ( resp.) or () is zero. Suppose , in this case can not be maximizing literal for any low clause. Thus . Suppose that , then is a maximizing literal for a high clause and thus , and . If , then must be a maximizing literal for a high-clause, and this is not possible as . Thus .
Let be the collection of literals for which . Now that quantity captures the contribution of all low clauses and many high-clauses. For all remaining high-clauses, there exist a literal such that and . The contribution of all the remaining high- clauses is . This quantity equals as for . ∎
Finally, we are ready to complete the proof of Theorem 3.7. For every literal , By Claim 3.7.2, . Let , . Consider the following inequalities.
[TABLE]
In the above, equality at line 2 is due to Claim 3.8.1. The inequality at line 4 follows because . The last inequality follows because is maximized at . The last equality follows as . Note that the number of clauses and by Claim 3.7.1 . It follows that . Thus . ∎
3.3 - Hardness
In this subsection, we show that is hard for the class . We show this by reducing to . Since is complete for , the result follows. We also show that the same reduction can be used to compute a assignment from an optimal -interpretation.
Theorem 3.9**.**
* metric reduces to for CNF formulae. Hence is hard for for CNF formulae.*
Proof.
Let be a formula with clauses on variables . Consider the formula with additional variables constructed as follows: For each clause of , add the clause in . Also add unit clauses . That is
[TABLE]
Claim 3.9.1**.**
* where is the maximum number of clauses that can be satisfied in .*
Proof.
We show this claim by first showing that and exhibiting an interpretation so that . We claim that if is the maximum number of clauses that can be satisfied in , then is the maximum number of clauses that can be satisfied in . We will argue this by contradiction. Let be an assignment that satisfies clause in . Let be the number of s that are set to False. This assignment will satisfy clauses of the form . However the total number of clauses of the form that are satisfied is . Thus there are clauses of the form that are satisfied where is set to False. This assignment when restricted to s will satisfy more than clauses of . Hence the contradiction.
Thus from Theorem 3.7, it follows that . Now we exhibit an interpretation so that . Consider an assignment for that satisfies clauses. Consider the following interpretation over the variable of : if and if . if and only if is satisfied by . Else . For every satisfiable clause , and . For all other clauses in , . Since there are clauses that are satisfied, the number of clauses for which is . Hence the . Thus . ∎
Since , for can be computed by knowing the . ∎
While the above theorem shows that can be computed from , the next theorem shows that a maxsat assignment can be computed from an optimal -interpretation.
Theorem 3.10**.**
* metric reduces to .*
Proof.
Consider the same reduction as from the previous theorem. Our task is to construct a assignment for , given an optimal -interpretation for . By the earlier theorem, , where is the maximum number of satisfiable clauses of .
We next establish a series of claims on the values takes by and .
Claim 3.10.1**.**
For all ; .
Proof.
Consider a clause for which . Now the contribution of and the clause to is . Since there is no clause for which , the above value is maximized when . Now consider a clause , for which . Contribution of and the clause to is . Since, , and there is no other clause in which or appear, the above expression is maximized when and thus . ∎
Claim 3.10.2**.**
For every , if is not maximizing literal for clause , then .
Proof.
Let be a clause for which is not maximizing literal. Say is the maximizing literal. We first consider the case . By previous claim, , and if , then can not be maximizing literal for clause . Thus . Now consider the case . Suppose that . Now the contribution of the clauses and to is . However, if we change , then the contribution of these clauses would become and this would contradict the optimality of . Thus by Claim 3.10.1, . ∎
Claim 3.10.3**.**
For all , if or is a maximizing literal, then
Proof.
We argue for the case when is a maximizing literal. The case when is a maximizing literal follows by similar arguments. Suppose that is a maximizing literal and and is neither 0 nor 1. It must be the case that is also a maximizing literal, otherwise making will increase the trust value. Suppose is a maximizing literal for many clauses and is a maximizing literal for many clauses. If , then we can obtain a -interpretation, by swapping with . If equals , then must be equal to as is maximized for . Thus . For every clause for which or is the maximizing literal, it must be the case that , by Claim 3.10.2. Let be the collection of all clauses together with , where either or is maximizing literal. The contribution of these clauses to is .
We now construct a new -interpretation that will contradict the optimality of . For every clause in which is the maximizing literal, and . Now the contribution of clauses from to is
Since (when ),
[TABLE]
Thus which is a contradiction. Thus if , then , a similar argument shows that if , then . ∎
Claim 3.10.4**.**
For every with , and are maximizing literals for exactly the same number of clauses.
Proof.
Let be the collection of clauses for which either or is maximizing literal. Suppose that is maximizing literal for clauses and is maximizing literal for clauses. If , and this contradicts Claim 3.10.3. ∎
We will show how to construct a assignment from : If , set the truth value of to False, else set the truth value of to True.
By Claim 3.10.3, . Let be the number of clauses for which maximizing literal is a -variable and . Note that the above truth assignment will satisfy all the clauses. Let be number of clauses for which maximizing literal is a -variable and . By Claim 3.10.4, in exactly clauses a positive literal is maximizing, and thus all these clauses are satisfied by our truth assignment. Thus the total number of clauses satisfied by the truth assignment is . Let the number of clauses in which is maximizing literal. By Claim 3.10.1, when is maximizing literal. Thus
[TABLE]
The last equality follows from Claim 3.9.1. Thus , combining this with , we obtain that . Thus the truth assignment constructed will satisfy clauses and is thus a assignment. ∎
4 Approximating
We study the problem of approximating efficiently. Below, a -SAT formula is a CNF formula with exactly distinct variables in any clause. We start with the following proposition.
Lemma 4.1**.**
Let be an assignment, that satisfies clauses of a CNF formula . There is an interpretation so that is
Proof.
If , set and if , then set . For every clause that is satisfied, we obtain a max value of and for every clause that is not satisfied, the max value is . Thus the obtained by this assignment is , and this is maximized when by Proposition 1. ∎
Hence, for example, if is a 3-SAT formula, since a random assignment satisfies fraction of the clauses in expectation, for a random assignment , and by Lemma 4.1, . The following lemma shows that one can get a better lower bound on in terms of the clause sizes for CNF formulae.
Lemma 4.2**.**
For every CNF formula , where is the arity of the ’th clause in .
Proof.
Consider the interpretation that assigns every variable a uniformly chosen value in the interval . Let the clauses in be . Then:
[TABLE]
Hence, there exists a choice of achieving this trust value. ∎
This yields a probabilistic algorithm. For example, if is a -SAT formula, and thus improving on the result of Lemma 4.1. In fact, we can design a deterministic polynomial time algorithm that finds an interpretation achieving the trust value guaranteed by Lemma 4.2, using the well-known ‘method of conditional expectation’ to derandomize the construction in the proof (For example, see [AS08, GW94]).
Theorem 4.3**.**
There is a polynomial-time, -approximation algorithm for , when the input formulas are -CNF formulas with -clauses.
Proof.
Arbitrarily ordering the variables , the idea is to sequentially set ensuring that for every :
[TABLE]
Assuming have already been fixed, we show how to choose satisfying the above. We use to denote . For a clause , let , and suppose . Then:
[TABLE]
where is the number of literals in the clause involving variables . One can similarly evaluate the conditional expectation in the cases and .
Summing up over all the clauses , we get that
[TABLE]
is a continuous function of that is a piecewise polynomial in at most intervals. In polynomial time111For simplicity, we ignore issues of precision here, but the error can be made inversely polynomial in ., we can find a value of that maximizes this function. By induction on , the maximum value of this function is at least , and hence (*) is satisfied. This completes the description of the algorithm.
∎
Next, we show that the approximation factor can not be significantly improved.
We use the following result on hardness of approximating established by Hastad [Hås01].
Theorem 4.4** ([Hås01]).**
For any and any it is NP-hard to distinguish satisfiable -SAT formulas from -SAT formulae satisfiable clauses.
We are now ready to show the following.
Theorem 4.5**.**
There is no polynomial-time -approximation algorithm for for -SAT formulae, unless .
Proof.
Assuming such an approximation algorithm exists, we contradict Hastad’s Theorem (Theorem 4.4). Consider the following algorithm that on input a -SAT formula , runs . If outputs a value that is , then outputs YES otherwise outputs NO. Suppose is satisfiable, then . Hence will output a value . Thus output YES. Suppose maximum number of satisfiable clauses for is . By Theorem 3.7,
[TABLE]
Hence output of is and hence will output NO.
Thus contradicts Theorem 4.4, unless . ∎
Thus, for example for -SAT formulas, while we have a polynomial-time, -approximation algorithm (by Theorem 4.3), we cannot expect an efficient -approximation algorithm by the above result unless equals . It remains an interesting open problem to determine the optimal approximation ratio for this problem achievable by a polynomial time algorithm.
5 Complexity of Access Maximization
In this section, we study the optimization problems for the access control semiring . We refer to the corresponding computational problems as and . For this section we first assume the negation function is the additive inverse modulo . That is \mbox{\daleth}(a)=b such that .
Theorem 5.1**.**
Let be a propositional formula in negation normal form and . The following statement holds.
- •
If is satisfiable, then .
- •
If is not satisfiable, then .
Proof.
We will first prove it for the case when is in the CNF form, i.e . Suppose that the formula is satisfiable and is a satisfying assignment to the variables . Consider the interpretation defined as follows: If is true, then , else \pi(x_{i})=\mbox{\daleth}(k). Consider a clause , since the formula is satisfiable, there exists a literal (either or for some ) in such that is set to true. If , then and . If , then \pi((x_{i})=\mbox{\daleth}(k)=0 and \mathsf{Sem}(\neg x_{i},\pi)=\mbox{\daleth}(0)=k. Since is a disjunction . Thus for every clause , . Since is a conjunction of , it follows that .
For the proof of the second item, first assume that is even, the proof when is odd is very similar. Note that in this case, \mbox{\daleth}(k/2)=k/2. Let be an unsatisfiable formula. Consider an interpretation where for every . Clearly, for this interpretation, . Suppose that be an interpretation . Consider the following satisfying assignment: is true if , else is false. Observe that this is a consistent assignment. We will establish that this assignment satisfies . This establishes that .
Note that for every clause , , . Fix a clause , since , there exists a literal in such that . If , then which implies that . Thus is true and the clause is satisfied by the assignment. If , then . Thus \mbox{\daleth}(\pi^{\prime}(x_{i}))>k/2. By the definition of , we have . Thus is set to false. Thus the clause is satisfiable. This proves that the assignment satisfies the formula .
The case where the general formula is in the negation normal form follows by similar ideas using the notion of proof trees as in the case of Viterbi semiring. ∎
For a general negation function, we can establish an analogous theorem. For this, we define the notion of the index of negation. Given a negation function , its index denoted by {\it Index}(\mbox{\daleth}) is the largest for which there exists , such that both and \mbox{\daleth}(a) are at least .
Theorem 5.2**.**
Let be a propositional formula in negation normal form and . The following statement holds.
- •
If is satisfiable, then .
- •
If is not satisfiable, then \mathsf{optAccessVal}(\varphi)=Index(\mbox{\daleth}).
The following is a corollary to the above result and its proof which states that the complexity of optimization problems over access control semiring is equivalent to their complexity over the Boolean semiring.
Theorem 5.3**.**
The problem and are equivalent under metric reductions. Similarly, the problem and the problem of computing a satisfying assignment of a given Boolean formula are equivalent under metric reductions.
6 Conclusion
In this work, we provided a comprehensive study of the computational complexity of and the related problem over various semirings such as Viterbi semiring, tropical semiring, access control semiring and fuzzy semiring, from both an algorithmic and a complexity-theoretic viewpoint. An exciting recent development in the field of CSP/SAT solving has been the development of solvers for , which seeks to find the smallest lexicographic satisfying assignment of a formula [MSAGL11]. In this regard, Theorem 3.2 opens up exciting directions of future work to develop efficient techniques for .
7 Acknowledgements
We thank Val Tannen for introducing us to the world of semiring semantics and for helpful conversations during the nascent stages of the project. We thank the anonymous reviewers of AAAI-23 for valuable comments. This research is supported by the National Research Foundation under the NRF Fellowship Programme [NRF-NRFFAI1-2019-0004] and Campus for Research Excellence and Technological Enterprise (CREATE) program. Bhattacharyya was supported in part by the NRF Fellowship Programme [NRF-NRFFAI1-2019-0002] and an Amazon Research Award. Vinod was supported in part by NSF CCF-2130608 and NSF HDR:TRIPODS-1934884 awards. Pavan was supported in part by NSF CCF-2130536, and NSF HDR:TRIPODS-1934884 awards.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[ADT 11] Yael Amsterdamer, Daniel Deutch, and Val Tannen. Provenance for aggregate queries. In Proc. of PODS , pages 153–164, 2011.
- 2[AS 08] Noga Alon and Joel H. Spencer. The Probabilistic Method, Third Edition . Wiley-Interscience series in discrete mathematics and optimization. Wiley, 2008.
- 3[BG 06] Stefano Bistarelli and Fabio Gadducci. Enhancing constraints manipulation in semiring-based formalisms. In ECAI , volume 141, pages 63–67, 2006.
- 4[Bis 04] Stefano Bistarelli. Semirings for soft constraint solving and programming , volume 2962. Springer Science & Business Media, 2004.
- 5[BMR 95] Stefano Bistarelli, Ugo Montanari, and Francesca Rossi. Constraint solving over semirings. In IJCAI (1) , pages 624–630. Citeseer, 1995.
- 6[BMR 97] Stefano Bistarelli, Ugo Montanari, and Francesca Rossi. Semiring-based constraint satisfaction and optimization. J. ACM , 44(2):201–236, 1997.
- 7[BMR + 99] Stefano Bistarelli, Ugo Montanari, Francesca Rossi, Thomas Schiex, Gérard Verfaillie, and Hélene Fargier. Semiring-based csps and valued csps: Frameworks, properties, and comparison. Constraints , 4(3):199–240, 1999.
- 8[Cui 02] Yingwei Cui. Lineage tracing in data warehouses . Ph D thesis, Stanford University, 2002.
