Fine-grained Complexity of Partial Minimum Satisfiability

1 Introduction

For many computationally hard problems, the best way to cope with their intractability in practice is to reduce them to SAT or MAX-SAT and then run a SAT/MAX-SAT solver. The main reason for this is the existence of the whole industry studying exactly these problems. There are annual conferences and competitions solely dedicated to these problems, like SAT 1 , MSE (MaxSAT Evaluation 2 ), and others. At AAAI-2011, Li et al. [2011] proposed an alternative to this approach and suggested reducing NP-hard problems to the following PARTIAL MIN-SAT problem.

1 http://satisfiability.org/SAT22/

2 https://maxsat-evaluations.github.io/2021/

In the same paper, Li et al. [2011] developed the MinSatz solver and showed that reducing to PARTIAL MIN-SAT and solving with MinSatz is in some cases more efficient than a reduction to SAT or MAX-SAT. We also observe that the language of the PARTIAL MIN-SAT problem allows to succinctly encode a number of classical problems such as VERTEX COVER, SET COVER, INDEPENDENT SET, HITTING SET, and many others.

Since the introduction of the problem, many results relating to PARTIAL MIN-SAT were published [Ignatiev et al., 2016; Zhu et al., 2012; Li and Manya, 2015; Li et al., 2012; Abram´e and Habet, 2015; Hers et al., 2012; Ignatiev et al., 2014; Avidor and Zwick, 2005; Escoffier and Paschos, 2007]. Note that some approximation results were known for PARTIAL MIN-SAT even before [Li et al., 2011], for example [Marathe and Ravi, 1996; Kohli et al., 1994]. However, to the best of our knowledge, the general case of PARTIAL MIN-SAT was not studied up to these days from the worst-case complexity point of view. This is drastically different from the case of SAT and MAX-SAT: for those problems there is a chain of non-trivial algorithms with improving bounds on the worstcase complexity. In Tables 1 and 2 we list the algorithms whose running time depends on the overall number of clauses in the input formula. Note that the last results were presented quite recently at AAAI-2021 and IJCAI-2019 after 15 years of no progress.

While the search for the best worst-case guarantee of an algorithm for SAT and its variants poses an intriguing theoretical question, it is also well-motivated from the practical perspective. Tools and reduction/branching rules used in algorithms for the worst case have been consistently reused in the implementations of practical solvers. In the case of SAT, the most well-known such rules are pure literal elimination, resolution, and unit propagation. The main motivation of our study is to extend this perspective to the more expressive PARTIAL MIN-SAT problem.

In particular, we are interested in running time bounds in terms of m, where m is the overall number of clauses. One may expect that the behavior of PARTIAL MIN-SAT is similar to that of SAT and MAX-SAT since the problems are tightly related, and from [K¨ugel, 2012] we know a natural transformation from PARTIAL MIN-SAT to PARTIAL MAXSAT and vice versa. Quite surprisingly the situation turns out to be significantly different. It is easy to see that pure literal elimination does not work for PARTIAL MIN-SAT, as assigning a pure literal to true can undesirably satisfy soft clauses. Also, SET COVER can be reduced to PARTIAL MIN-SAT and all literals will be positive. Hence, PARTIAL MIN-SAT is NP-hard even if all literals are positive. Unfortunately, the usage of the resolution rule is also restricted even if the variable appears only once positively and once negatively, since INDEPENDENT SET can be reduced to this special case of PARTIAL MIN-SAT. Hence, PARTIAL MIN-SAT is NP-hard even if each variable appears once as a positive literal and once as a negative literal.

While these observations leave a possibility that a betterthan-trivial algorithm for PARTIAL MIN-SAT might be obtained by using a more sophisticated approach, in Theorem 1 we show that this is most likely not the case. We prove that there is no algorithm for PARTIAL MIN-SAT with running time O∗ ((2 - ϵ)m) for any ϵ > 0, unless the Strong Exponential Time Hypothesis (SETH) fails. Recall that SETH is a complexity hypothesis that implies that there is no O∗ ((2-ϵ)n ) algorithm for SAT for any ϵ > 0, where n is the number of variables. Thus, PARTIAL MIN-SAT does not have algorithms with non-trivial running time both in terms of n and m if SETH is true. (O∗ (2n ) and O∗ (2m) running time algorithms for PARTIAL MIN-SAT are straightforward.)

On the positive side, we present several non-trivial algorithms that are characterized by a broader range of natural parameters such as n (number of variables), s (number of soft clauses), h (number of hard clauses), q (size of the largest hard clause), ts (number of variables that have positive and negative literals inside soft clauses). On instances where each clause has length at most two, PARTIAL MINSAT can be solved in O∗ (2ωn/3 ) time (here ω is the matrix multiplication exponent). If q ≤ 2 then PARTIAL MINSAT can be solved in time O∗ (csvc ) where cvc is the lowest constant such that VERTEX COVER admit O∗ (cn′ vc ) running time algorithm on graphs with n′ vertices. (The currently best bound of cvc = 1.1996 is given by [Xiao and Nagamochi, 2017]). Moreover, PARTIAL MIN-SAT can be solved in O∗ (2min{n,k,ts} · (2 - 1q )n-min{n,k,ts} ) time and if q ≥ 3 then there is a O∗ (1.6181h ·(2- 1q )s ) running time algorithm for PARTIAL MIN-SAT. Finally for the general case we present an algorithm with the running time O∗ (1.755 m+n 2 ).

The rest of the paper is organized as follows. In Section 2 we establish a connection between PARTIAL MIN-SAT and a certain set union problem that is crucial in the proof of Theorem 1. In Section 3 we show Theorem 1 and other parameterized complexity lower bounds. Finally, in Section 4 we present our algorithmic results. Proofs of the statements marked by ⋆ are omitted due to space constraints.

Throughout the paper we use standard notions and definitions from graph theory [Diestel, 2010], parameterized complexity [Cygan et al., 2015], exact exponential algorithms [Fomin and Kratsch, 2010], and satisfiability theory [Marek, 2009]. Due to space constraints, we are not able to formally present all the definitions in the main body; we refer the reader the standard textbooks cited above.

2 MinimumUnion

In this section, we show that PARTIAL MIN-SAT is closely related to a natural set problem, MINIMUM UNION, which asks to find a collection of k sets with minimum union size. This problem was recently studied in [Agrawal and Maity, 2021] from the parameterized point of view. We shall also use this connection to show parameterized lower bounds for PARTIAL MIN-SAT. Throughout the paper, we stick to the following multicolored version of MINIMUM UNION.

MULTICOLORED MINIMUM UNION

Input: An integer n, k collections of subsets of [n]

F1, F2, . . . , Fk ⊆ 2[n] , and an integer ℓ.

Question: Does there exist a choice of S1, S2, . . . , Sk such that Si ∈ Fi and | ⋃ Si| ≤ ℓ?

Lemma 1. MULTICOLORED MINIMUM UNION is equivalent to the special case of PARTIAL MIN-SAT when all variables appear positively in the input formula. Moreover, in the corresponding PARTIAL MIN-SAT instance the number of hard clauses equals k, the number of soft clauses equals n, the number ℓ is the number of satisfied soft clauses and the variables correspond to the sets in the instance of MULTICOLORED MINIMUM UNION.

Proof. To construct an instance of PARTIAL MIN-SAT from an instance of MULTICOLORED MINIMUM UNION, it is enough to associate a soft clause with each element of the universe [n]. Each of the k color groups is associated with a hard clause. With each unique universe subset in the instance, a unique variable is associated. Hence, the number of variables of the constructed instance equals the number of unique subsets, the number of soft clauses equals n and the number of hard clauses equals k. Then ith hard clause is a disjunction of the variables corresponding to the subsets in Fi. While j th soft clause is a disjunction of all variables corresponding to the subsets containing element j of the universe.

It is then asked to satisfy all hard clauses but at most ℓ soft clauses simultaneously. The value of a variable in an assignment corresponds to whether we should take the corresponding subset in the solution or not. Hard clauses ensure that at least one set is picked from each Fi, while each soft clause evaluates whether the corresponding element is covered by the chosen subsets. Thus, the constructed instance of PARTIAL MIN-SAT is equivalent to the initial instance of MULTICOLORED MINIMUM UNION.

To construct an instance of MULTICOLORED MINIMUM UNION from an instance of PARTIAL MIN-SAT with allpositive literals, one need to proceed in a similar fashion as above, but in the opposite direction: associate a universe element with each soft clause; associate a subset with each variable that consists exactly elements corresponding to soft clauses containing this variable; finally associate with each hard clause a subset family containing subsets corresponding to the variables comprising this hard clause.

Below, we provide an example of reduction from PARTIAL MIN-SAT with all-positive literals to MULTICOLORED MINIMUM UNION. Assume, we have the following instance of PARTIAL MIN-SAT:

hard clauses: x ∨ y, y ∨ z

soft clauses: x ∨ y ∨ t, t ∨ z, y ∨ z ∨ t.

An equivalent instance of MULTICOLORED MINIMUM UNION has n = 3 as the number of soft clauses is three, k = 2 as the number of hard clauses is two. F1 = {{1}, {1, 3}} as a literal x from a hard clause x ∨ y appears only in the first soft clause and a literal y appears in the first and the third soft clauses. Similarly, F2 = {{1, 3}, {2, 3}} as a literal z from a hard clause y ∨ z appears in the second and the third soft clauses.

While MULTICOLORED MINIMUM UNION is thus a special case of PARTIAL MIN-SAT, PARTIAL MIN-SAT still can be reduced to MULTICOLORED MINIMUM UNION in FPT time.

Lemma 2 (⋆). PARTIAL MIN-SAT parameterized by k + h admits a parameterized reduction to MULTICOLORED MINIMUM UNION parameterized by ℓ + k.

3 Lower Bounds

We start with the lower bounds for PARTIAL MIN-SAT, disproving faster-than-brute-force algorithms in terms of number of variables or number of clauses under SETH. The starting point of the reduction is the following result of [Cygan et al., 2016] on the complexity of a variant of the HITTING SET problem.

Proposition 1. Let δ ∈ (0, 1) be an arbitrary real number. Unless SETH fails, there exists c > 0 such that c-SPARSEHITTING-SET cannot be solved in O(2δn ) running time.

Theorem 1. Unless SETH fails, PARTIAL MIN-SAT cannot be solved in O∗ ((2 - ϵ)n ) or O∗ ((2 - ϵ)m) running time for any ϵ > 0.

Proof. Since PARTIAL MIN-SAT with zero soft clauses is equivalent to SAT, the first part of this theorem is trivial.

To show the second part, we require sophisticated reductions. We provide a polynomial reduction from c-SPARSEHITTING SET over n elements to PARTIAL MIN-SAT where the number of clauses is bounded by c′n for some constant c′ > 1 that can be as close as needed to 1 in trade for running time. We then will show how from this reduction and a O((2 - ϵ)m) algorithm for PARTIAL MIN-SAT it follows that SETH fails through Proposition 1. Observe also that any O∗ ((2 - ϵ)m)-time algorithm has a O((2 - ϵ′ )m) runtime bound for any ϵ′ > ϵ.

Let (n, S1, S2, . . . , Sm, ℓ) be the given instance of cSPARSE-HITTING SET. We construct an equivalent instance of MULTICOLORED MINIMUM UNION using a fixed integer p that is to be chosen later. The universe for instance of MULTICOLORED MINIMUM UNION is equivalent to the universe of the given instance. To construct the subset groups, split the m sets of the input instance into ⌈m/p⌉ groups, each containing p sets, except possibly for the last one that can contain less than p sets.

Each group forms an instance of HITTING SET. To construct the family Fi, take the ith group and enumerate all inclusion-wise minimal hitting sets of the group. Clearly, the size of Fi is bounded by np , while the time required to construct it is bounded by nO(p) . Thus, the instance of MULTICOLORED MINIMUM UNION consists of ⌈m/p⌉ collections of sets. We finally ask to find ⌈m/p⌉ sets from these collections such that their union is of size at most ℓ.

We claim that the constructed instance (n, ⌈m/p⌉,F1, . . . ,F⌈m/p⌉, ℓ) is a yes-instance if and only if (n, S1, S2, . . . , Sm, ℓ) is a yes-instance. This equivalence is clear from the fact that any optimal hitting set of S1, S2, . . . , Sm is a union of inclusion-wise minimal hitting sets for each of the ⌈m/p⌉ groups.

Using Lemma 1, we finally construct an instance of PARTIAL MIN-SAT from the instance of MULTICOLORED MINIMUM UNION. The number of variables is bounded by np , while the total number of clauses equals n + ⌈m/p⌉ ≤ n+cn/p+1 ≤ n+cn/p+n/p, as we reduce from c-SPARSEHITTING SET. Hence, the number of clauses in the instance of PARTIAL MIN-SAT is bounded by (1 + (c + 1)/p)n.

Assume that the SETH holds and there exists a O(2δ′m′ )- time algorithm for PARTIAL MIN-SAT for some δ′ < 1, where m′ is the number of clauses in the input formula. Take δ := δ′ +(1-δ′ )/2 < 1. By Proposition 1 there exists a constant c such that no O(2δn ) algorithm exists for c-SPARSEHITTING SET.

Then take p := ⌈2δ′ (c + 1)/(1 - δ′ )⌉ and construct an algorithm for c-SPARSE-HITTING SET using the reduction from HITTING SET to PARTIAL MIN-SAT and the O(2δ′m′ )algorithm for PARTIAL MIN-SAT. The number of clauses m′ is bounded by (1 + (c + 1)/p)n ≤ (1 + (1 - δ′ )/2δ′ )n. The running time of the constructed algorithm is bounded by O(2(δ′+(1-δ′ )/2)n ), which is O(2δn ), and this contradicts Proposition 1. The proof is complete.

Observe that for both SAT and MIN-SAT there exists an algorithm that is single-exponential in the number of satisfied clauses i.e. in h + k: for SAT it is the straightforward O∗ (2m) = O∗ (2h ) algorithm, and for MIN-SAT such an algorithm follows from the reduction to VERTEX COVER [Marathe and Ravi, 1996]. It is thus natural to ask whether a similar algorithm exists for PARTIAL MIN-SAT, or at least one with running time f(h + k) · nO(1) for some function f of h + k, the total number of satisfied clauses. The following theorem resolves the last question negatively, up to the standard parameterized complexity assumption that W[1] ̸= FPT.

Theorem 2 (⋆). PARTIAL MIN-SAT is W[1]-hard with respect to parameter h+k, i.e. the number of clauses to satisfy. Unless ETH fails, PARTIAL MIN-SAT does not admit an algorithm with running time f(h+k) · (n+m)o(√h+k) for any computable function f.

4 Algorithms

Having established the main intractability result for PARTIAL MIN-SAT (Theorem 1), we turn our attention to special cases where algorithms with non-trivial running times exist. One notable "easy" case of SAT that is still fairly expressive is 2-SAT, which is well-known to be solvable in polynomial time. For PARTIAL MIN-SAT however, there is little hope for a polynomial algorithm in this case, as even 2-MIN-SAT is known to be NP-complete [Kohli et al., 1994]. On the positive side, MIN-SAT with arbitrary clause length allows an efficient reduction to VERTEX COVER [Marathe and Ravi, 1996], where the number of clauses in the formula is exactly transferred to the number of vertices in the graph. In particular, any algorithm that solves VERTEX COVER in time O∗ (cn′ ), where n′ is the number of vertices in the graph, immediately gives an algorithm for MIN-SAT with running time O∗ (cm). A similar situation occurs with another closely related problem. In 2-MIN-ONES-SAT, the input is a 2CNF formula φ and an integer k, and the task is to determine whether φ can be satisfied by an assignment that sets at most k variables to true. [Misra et al., 2013] showed a reduction from 2-MIN-ONES-SAT to VERTEX COVER that transfers the number of variables in φ exactly to the number of vertices in the graph. Observe that MIN-ONES-SAT is a special case of PARTIAL MIN-SAT where soft clauses are simply variables of the formula. Since PARTIAL MIN-SAT with hard clauses of length at most 2 generalizes both MIN-SAT and 2-MIN-ONES-SAT, a natural question is whether a similar reduction to VERTEX COVER can be derived. In the next theorem, we show that this is indeed the case.

Theorem 3 (⋆). PARTIAL MIN-SAT with hard clause length bounded by 2 can be reduced to an instance (G, k) of VERTEX COVER with |V (G)| = s in polynomial time, if all hard clauses can be satisfied simultaneously. Moreover, there is a one-to-one correspondence between vertices of G and soft clauses. Any set of vertices in G is independent if and only if the corresponding set of clauses can be unsatisfied simultaneously in the initial instance. The target graph Gmay contain loops.

To give an intuition, the reduction populates the target graph G with two kinds of edges: some pairs of soft clauses cannot be unsatisfied simultaneously because of a hard clause that prevents this (in fact, any clause in the transitive closure of the set of hard clauses, similar to [Misra et al., 2013]), and some because there is a variable that appears positively in one clause and negatively in the other. It is then left to show that forbidding these pairs is both necessary and sufficient for a PARTIAL MIN-SAT solution.

Composing our reduction with the best-known exact algorithm for VERTEX COVER [Xiao and Nagamochi, 2017], we obtain the following.

Corollary 1. PARTIAL MIN-SAT with hard clause length bounded by 2 is solvable in time O∗ (1.1996s ).

Restricting clauses to length 2 allows us to break the barrier of Theorem 1 in terms of the number of variables as well. The following algorithm stems from the matrix-multiplicationbased MAXIMUM CUT algorithm with the same running time due to [Williams, 2007].

Theorem 4 (⋆). There is a O∗ (2ωn/3 ) running-time algorithm for PARTIAL MIN-SAT restricted to formulas in 2CNF.

We now move to a more general case where the hard clause length is bounded by a parameter q.

Lemma 3. When soft clauses contain only positive literals, PARTIAL MIN-SAT can be solved in O∗ ((2 - 1q )n ) time.

Proof. To approach this case of PARTIAL MIN-SAT, we first refer to the Φ-SUBSET problem, which is the central problem of the work of Fomin et al [2019]. Their results hold in the general model where a predefined mapping Φ constructs the instance from an encoding in the form of a binary string. However, in our case the encoding is straightforward, so we restate Φ-SUBSET in the following way. Here, an implicit set family F should be understood as defined by the algorithm that checks whether an arbitrary set belongs to F, instead of listing the sets in the family explicitly in the input.

Φ-SUBSET parameterized by n

Input: An implicit subset family F over an nelement universe U, such that S ?∈ F can be checked in polynomial time for a given S ⊆ U.

Question: Find any element of F.

Another crucial problem in the work is the Φ-EXTENSION problem.

The central result of [Fomin et al., 2019] is that a qk′ ·nO(1) algorithm for Φ-EXTENSION for some family F yields a (2- 1q )n ·nO(1) algorithm for Φ-SUBSET for the same family. Thus, our approach to PARTIAL MIN-SAT with all-positive soft clauses is to reduce it to Φ-SUBSET, where universe is a set of variables, and show a Φ-EXTENSION algorithm running in qk′ · nO(1) time.

Let (φ, k) be the given instance of PARTIAL MIN-SAT. We start the reduction to Φ-SUBSET by identifying the universe of Φ-SUBSET with the set of variables of φ. The set family F is then defined as follows. A set S of variables of φ is in F if and only if assigning all variables of S to one (and all other variables to zero) satisfies all hard clauses and at most k soft

clauses. Clearly, S ?∈ F can be checked in polynomial time. Moreover, solving Φ-SUBSET for F is equivalent to solving (φ, k).

To finish the proof, we describe the algorithm for ΦEXTENSION. Given a set S of variables that are assigned to one, we need to assign at most k′ more variables to one so at most k soft clauses are satisfied while all hard clauses are satisfied. If the assignment of the variables of S already satisfies at least k + 1 soft clauses, then no X exists for ΦEXTENSION, since we cannot "unsatisfy" any soft clause by assigning more variables to one. The same holds if there is a hard clause with all negative literals that all evaluate to false because of S. In these two cases, the algorithm reports that no X exists and stops.

Otherwise, at most k soft clauses are satisfied. If all hard clauses are satisfied as well, the algorithm reports empty X and stops, as S ∈ F already. We consider that at least one hard clause is not satisfied by the assignment. In this case, a branching can always be performed. There are at most q literals in this clause with variables outside S. Since the clause is not satisfied, all these literals are positive (while literals with variables in S are negative). As negative literals can no more be satisfied, the only option to satisfy the clause is to satisfy at least one its positive literal. This clearly yields at most q branches, where in each branch we add a variable to S and decrease k′ by one.

Clearly, the obtained algorithm for Φ-EXTENSION runs in qk′ · (n+m)O(1) time. Finally, the central result of Fomin et al. gives the running time (2 - 1q )n · (n + m)O(1) for ΦEXTENSION, hence the algorithm for PARTIAL MIN-SAT with soft clauses containing only positive literals.

We say that a variable is non-trivial (with respect to the set of clauses) if it appears both negatively and positively (in the clauses of this set). The following algorithm generalizes Lemma 3, as well as the best-known algorithm for MIN-ONES q-SAT.

Theorem 5. There is an algorithm for PARTIAL MIN-SAT with running time O∗ (2min{k,ts} · (2- 1q )n-min{k,ts} ), where ts is the number of non-trivial variables with respect to soft clauses.

Proof. The approach is to reduce to the case of all-positive soft clauses using the two following rules. When neither is applicable, Lemma 3 is applied.

Reduction rule 1. If there is a variable that appears in soft clauses only as negative literals, revert all literals containing this variable in all clauses of φ.

Branching rule 1. If there is a variable that appears in soft clauses as both positive and negative literals, branch on this variable set to true or false.

It is trivial to see that the rules are safe. Note that Branching rule 1 increases the number of satisfied soft clauses by at least one in each branch, so the depth of the corresponding recursion tree is at most k. Since it also reduces the number of non-trivial variables with respect to soft clauses by at least one, the depth of this tree is also at most ts. Observe that each application of Branching rule 1 also reduces the number of variables by at least one.

In each leaf of the recursion tree produced by the rules, we have an instance of PARTIAL MIN-SAT suitable for application of Lemma 3. For an instance that corresponds to a leaf of depth d, the running time of the algorithm of Lemma 3 is at most O∗ ((2 - 1q )n-d ). The recursion tree is a complete binary tree, so the worst case is when all leaves have maximum depth min{k, ts} and there are 2min{k,ts} leaves in total. Thus, the running time bound of our algorithm is O∗ (2min{k,ts} · (2 - 1q )n-min{k,ts} ).

The absense of non-trivial variables helps also in hard clauses.

Lemma 4 (⋆). When there are no non-trivial variables with respect to hard clauses, the PARTIAL MIN-SAT is solvable in O∗ ((2 - 1q )s ) time.

With addition of simple branching on non-trivial variables w.r.t. hard clauses gives us the following.

Corollary 2. There is an algorithm for PARTIAL MIN-SAT running in O∗ (2th · (2- 1q )s ) time, where th is the number of non-trivial variables with respect to hard clauses.

Our final goal is to obtain a faster-than-2m algorithm for PARTIAL MIN-SAT when length of hard clauses is bounded. We obtain this by combining simple branching rules with the algorithm above, while also using another novel technique to get rid of non-trivial variables when a suitable branching is not possible.

Theorem 6. There is an algorithm for PARTIAL MIN-SAT running in time O∗ (1.6181h · (2 - 1q )s ) for q ≥ 3.

Proof. The algorithm starts with the following simple branching rule and simple reduction rule.

Branching rule 2. If there is a non-trivial (w.r.t. hard clauses) variable that appears at least three times (in total in φ), branch on the value of this variable.

Reduction rule 2. If Branching rule 2 cannot be applied and there are two non-trivial variables that appear in the same pair of hard clauses, assign these variables a value so both these clauses are satisfied.

Branching rule 2 leaves us with the case when each nontrivial variable appears exactly two times in hard clauses, while it does not appear in soft clauses at all. We still want to reduce this case to when no variable is non-trivial w.r.t. hard clauses. While there are 2th possible assignments of non-trivial variables, none of them satisfies any soft clause. Thus, we are not interested in each assignment itself, but we are rather interested in the set of hard clauses it satisfies. This idea leaves us with the following branching rule.

Branching rule 3. If there is a hard clause containing p ≥ 1 non-trivial variables, consider p + 1 branches:

• either this clause is not satisfied by any non-trivial variable; in this case assign all their literals in the clause to false;
• or this clause is satisfied by some of these variables; for each of p variables, consider a branchg where its literal is assigned to true while other p-1 literals are assigned to false.

Claim 1. Branching rule 3 is safe. It produces p+1 branches. If Branching rule 2 and Reduction rule 2 cannot be applied, it reduces the number of hard clauses with a non-trivial variable by at least p in each branch, and in one branch the decrease is at least p+1.

Proof. To see that Branching rule 3 is safe, note that the first item in its definition corresponds to the case when the selected hard clause is not satisfied by non-trivial variables. In this case, all non-trivial variables should be assigned a determined value.

The second item corresponds to when at least one of the non-trivial variables satisfy the clause. In this case, we can always assume that exactly one such variable satisfy the clause. If at least two non-trivial variables satisfy the clause, we can change the value of any of them and only increase the number of satisfied hard clauses, as each non-trivial variable appears exactly two times among hard clauses. Note that soft clauses are not influenced by this change at all. Thus, a greedy strategy of picking exactly one non-trivial variable for satisfying the clause is valid.

To show the number of clauses reduced in each branch, consider the number of hard clauses sharing a non-trivial variable with the selected clause. Since Reduction rule 2 cannot be applied, each of them shares exactly one non-trivial variable with the clause. Hence, there are exactly p such clauses. When we choose to not satisfy the selected clause with nontrivial variables, we satisfy exactly all p of them. In other p branches, where we flip the value of one non-trivial variable, we satisfy all but one of them and the selected clause, so the number of newly-satisfied clauses in these branches equals p as well.

While we do not satisfy the selected clause in the first branch, in this branch all non-trivial variables of this clause are assigned a value, so the selected clause no longer contain non-trivial variables. This gives the additional +1 to reduced clauses in exactly one of the branches as required.

The algorithm applies Branching rule 2, Reduction rule 2 and Branching rule 3 exhaustively. When none of them can be applied, then, clearly, there are no non-trivial variables with respect to hard clauses. In this case, the algorithm uses the algorithm of Lemma 4 as a subroutine and solves the instance of the current branch.

Running time analysis. Branching rule 2 reduces the total number of clauses in the formula by at least one in each branch, while in one branch the number of reduced clauses is at least two. The worst branching vector for this rule is (1, 2), and the derived branching factor is less than 1.6181.

Branching rule 3 gives a family of branching vectors, one for each p ∈ [q], namely vectors (1, 2),(2, 2, 3),(3, 3, 3, 4),. . . ,(q, q, . . . , q, q + 1). Note that the vector (1, 2) can trivially be expanded (by applying itself into its branches) into a vector (2, 3, . . . , t -2, t -1, t -1, t) for arbitrary t. Hence, its branching factor is not better than the factors of other q - 1 vectors. Then (1, 2) again gives the worst branching factor that is bounded by 1.6181. However, only hard clauses are in concern of this branching rule. Note also that Branching rule 2 is never applied after Branching rule 3 was applied. So once a clause containing a non-trivial variable was reduced, it will be never considered again by these two rules.

Finally, the algorithm of Lemma 4 gives us a subroutine that depends exponentially on the number of soft clauses, and the exponent is (2 - 1q ). Hence, when q ≥ 3 the worst exponent under the number of hard clauses is 1.6181, while for soft clauses it equals 2 - 1q . The upper bound of 1.6181h · (2- 1q )s · |φ|O(1) follows.

In Theorem 1 we have shown that PARTIAL MIN-SAT is not solvable significantly faster than O∗ (2n ) or O∗ (2m) assuming the SETH. One might start to suspect that even for all α ∈ [0, 1] there is no ϵ > 0 such that PARTIAL MIN-SAT admits O∗ ((2 - ϵ)αn+(1-α)m). The following theorem shows that this not the case. Moreover, when n is approximately equal to m the PARTIAL MIN-SAT problem can be solved faster than both O∗ (2n ) and O∗ (2m).

Theorem 7 (⋆). There is an algorithm for PARTIAL MINSAT with running time O∗ (1.755 n+m 2 ).

Acknowledgements

Research presented in Section "Algorithms" is supported by RSCF grant 18-71-10042. Research presented in Section "Minimum Union" is supported by HSE University and Leonhard Euler International Mathematical Institute in Saint Petersburg (agreement no. 075-15-2019-1620). Research presented in Section "Lower Bounds" is supported by the Austrian Science Fund (FWF) via project Y1329 (Parameterized Analysis in Artificial Intelligence).