The Parameterized Inapproximability Hypothesis (PIH), which is an analog of the PCP theorem in parameterized complexity, asserts the following: there is a constant ϵ> 0 such that for any computable function f:λ.,•→λ.,•, no f(k)· nO(1)-time algorithm can, on input a k-variable CSP instance with domain size n, find an assignment satisfying 1-ϵ fraction of the constraints. A recent work by Guruswami, Lin, Ren, Sun, and Wu (STOC'24) established PIH under the Exponential Time Hypothesis (ETH). In this work, we improve the quantitative aspects of PIH and prove (under ETH) that approximating sparse parameterized CSPs within a constant factor requires nk1-o(1) time. This immediately implies, for example, that finding a (k/2)-clique in an n-vertex graph with a k-clique requires nk1-o(1) time (assuming ETH). We also prove almost optimal time lower bounds for approximating k-ExactCover and Max k-Coverage. Our proof follows the blueprint of the previous work to identify a "vector-structured"ETH-hard CSP whose satisfiability can be checked via an appropriate form of "parallel"PCP. Using further ideas in the reduction, we guarantee additional structures for constraints in the CSP. We then leverage this to design a parallel PCP of almost linear size based on Reed-Muller codes and derandomized low degree testing.

The Parameterized Inapproximability Hypothesis (PIH) asserts that no fixed parameter tractable (FPT) algorithm can distinguish a satisfiable CSP instance, parameterized by the number of variables, from one where every assignment fails to satisfy an ɛ fraction of constraints for some absolute constant ɛ > 0. PIH plays the role of the PCP theorem in parameterized complexity. However, PIH has only been established under the Gap Exponential Time Hypothesis (ETH), a very strong assumption with an inherent gap. In this work, we prove PIH under the ETH. This is the first proof of PIH from a gap-free assumption. Our proof is self-contained and elementary. We identify an ETH-hard CSP whose variables take vector values, and constraints are either linear or of a special parallel structure. Both kinds of constraints can be checked with constant soundness via a “parallel PCP of proximity” based on the Walsh-Hadamard code.

Abstract Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning about algebraic data types (ADTs) and compositions of structural recursions. Modern theorem provers provide structural induction for such reasoning, but a structural induction on the original theorem is often insufficient for many equivalence theorems. In such cases, one has to invent a set of lemmas, prove these lemmas by additional induction, and use these lemmas to prove the original theorem. There is, however, a lack of systematic understanding of what lemmas are needed for inductive proofs and how these lemmas can be synthesized automatically. This paper presents directed lemma synthesis, an effective approach to automating equivalence proofs by discovering critical lemmas using program synthesis techniques. We first identify two induction-friendly forms of propositions that give formal guarantees to the progress of the proof. We then propose two tactics that synthesize and apply lemmas, thereby transforming the proof goal into induction-friendly forms. Both tactics reduce lemma synthesis to a set of independent and typically small program synthesis problems that can be efficiently solved. Experimental results demonstrate the effectiveness of our approach: Compared to state-of-the-art equivalence checkers employing heuristic-based lemma enumeration, directed lemma synthesis saves 95.47% runtime on average and solves 38 more tasks over an extended version of the standard benchmark set.

The Parameterized Inapproximability Hypothesis (PIH) asserts that no fixed parameter tractable (FPT) algorithm can distinguish a satisfiable CSP instance, parameterized by the number of variables, from one where every assignment fails to satisfy an ε fraction of constraints for some absolute constant ε > 0. PIH plays the role of the PCP theorem in parameterized complexity. However, PIH has only been established under Gap-ETH, a very strong assumption with an inherent gap. In this work, we prove PIH under the Exponential Time Hypothesis (ETH). This is the first proof of PIH from a gap-free assumption. Our proof is self-contained and elementary. We identify an ETH-hard CSP whose variables take vector values, and constraints are either linear or of a special parallel structure. Both kinds of constraints can be checked with constant soundness via a “parallel PCP of proximity” based on the Walsh-Hadamard code.

Abstract Probabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit $$\kappa $$ κ , we consider the tail probability $$\Pr [T \ge \kappa ]$$ Pr [ T ≥ κ ] , i.e., the probability that the randomized runtime T of the PRR exceeds $$\kappa $$ κ . Our focus is the formal analysis of tail bounds that aims at finding a tight asymptotic upper bound $$u \ge \Pr [T\ge \kappa ]$$ u ≥ Pr [ T ≥ κ ] . To address this problem, the classical and most well-known approach is the cookbook method by Karp (JACM 1994), while other approaches are mostly limited to deriving tail bounds of specific PRRs via involved custom analysis. In this work, we propose a novel approach for deriving the common exponentially-decreasing tail bounds for PRRs whose preprocessing time and random passed sizes observe discrete or (piecewise) uniform distribution and whose recursive call is either a single procedure call or a divide-and-conquer. We first establish a theoretical approach via Markov’s inequality, and then instantiate the theoretical approach with a template-based algorithmic approach via a refined treatment of exponentiation. Experimental evaluation shows that our algorithmic approach is capable of deriving tail bounds that are (i) asymptotically tighter than Karp’s method, (ii) match the best-known manually-derived asymptotic tail bound for QuickSelect, and (iii) is only slightly worse (with a $$\log \log n$$ log log n factor) than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover, our algorithmic approach handles all examples (including realistic PRRs such as QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1 s, showing that our approach is efficient in practice.

In this paper, we prove that assuming the exponential time hypothesis (ETH), there is no $f(k) \cdot n^{k^{o(1 / \log \log k)}}$-time algorithm that can decide whether an n-vertex graph contains a clique of size k or contains no clique of size $k / 2$, and no FPT algorithm can decide whether an input graph has a clique of size k or no clique of size $k / f(k)$, where $f(k)$ is some function in $k^{1-o(1)}$. Our results significantly improve the previous works [1], [2]. The crux of our proof is a framework to construct gap-producing reductions for the k-CLIQUE problem. More precisely, we show that given an error-correcting code $C: \Sigma_{1}^{k} \rightarrow \Sigma_{2}^{k^{\prime}}$ that is locally testable and smooth locally decodable in the parallel setting, one can construct a reduction which on input a graph G outputs a graph $G^{\prime}$ in $\left(k^{\prime}\right)^{O(1)} \cdot n^{O\left(\log \left|\Sigma_{2}\right| / \log \left|\Sigma_{1}\right|\right)}$ time such•if G has a clique of size k, then $G^{\prime}$ has a clique of size K, where $K=\left(k^{\prime}\right)^{O(1)}$.•if G has no clique of size k, then $G^{\prime}$ has no clique of size $(1-\varepsilon) \cdot K$ for some constant $\varepsilon \in(0,1)$.We then construct such a code with $k^{\prime}=k^{\Theta(\log \log k)}$ and $\left|\Sigma_{2}\right|=\left|\Sigma_{1}\right|^{k^{0.54}}$, establishing the hardness result above. Our code generalizes the derivative code [3] into the case with a super constant order of derivatives.

In this paper, we prove that it is W[2]-hard to approximate k-SETCOVER within any constant ratio. Our proof is built upon the recently developed threshold graph composition technique. We propose a strong notion of threshold graphs and use a new composition method to prove this result. Our technique could also be applied to rule out polynomial time ratio approximation algorithms for the non-parameterized k-SETCOVER problem with k as small as , assuming W[1] ≠ FPT. We highlight that our proof does not depend on the well-known PCP theorem, and only involves simple combinatorial objects.

In this paper, we propose an automated approach to finding correct and efficient memoization algorithms from a given declarative specification. This problem has two major challenges: (i) a memoization algorithm is too large to be handled by conventional program synthesizers; (ii) we need to guarantee the efficiency of the memoization algorithm. To address this challenge, we structure the synthesis of memoization algorithms by introducing the local objective function and the memoization partition function and reduce the synthesis task to two smaller independent program synthesis tasks. Moreover, the number of distinct outputs of the function synthesized in the second synthesis task also decides the efficiency of the synthesized memoization algorithm, and we only need to minimize the number of different output values of the synthesized function. However, the generated synthesis task is still too complex for existing synthesizers. Thus, we propose a novel synthesis algorithm that combines the deductive and inductive methods to solve these tasks. To evaluate our algorithm, we collect 42 real-world benchmarks from Leetcode, the National Olympiad in Informatics in Provinces-Junior (a national-wide algorithmic programming contest in China), and previous approaches. Our approach successfully synhesizes 39/42 problems in a reasonable time, outperforming the baselines.

Given a simple graph $G$ and an integer $k$, the goal of $k$-Clique problem is to decide if $G$ contains a complete subgraph of size $k$. We say an algorithm approximates $k$-Clique within a factor $g(k)$ if it can find a clique of size at least $k / g(k)$ when $G$ is guaranteed to have a $k$-clique. Recently, it was shown that approximating $k$-Clique within a constant factor is W[1]-hard [Lin21]. We study the approximation of $k$-Clique under the Exponential Time Hypothesis (ETH). The reduction of [Lin21] already implies an $n^{Ω(\sqrt[6]{\log k})}$-time lower bound under ETH. We improve this lower bound to $n^{Ω(\log k)}$. Using the gap-amplification technique by expander graphs, we also prove that there is no $k^{o(1)}$ factor FPT-approximation algorithm for $k$-Clique under ETH. We also suggest a new way to prove the Parameterized Inapproximability Hypothesis (PIH) under ETH. We show that if there is no $n^{O(\frac{k}{\log k})}$ algorithm to approximate $k$-Clique within a constant factor, then PIH is true.

We consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide automated algorithms that obtain both lower and upper bounds on the assertion violation probability. The main novelty of our approach is that we prove new and dedicated fixed-point theorems which serve as the theoretical basis of our algorithms and enable us to reason about assertion violation bounds in terms of pre and post fixed-point functions. To synthesize such fixed-points, we devise algorithms that utilize a wide range of mathematical tools, including repulsing ranking supermartingales, Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization. On the theoretical side, we provide (i) the first automated algorithm for lower-bounds on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds of exponential form in affine programs, and (iii) provably and significantly tighter upper-bounds than the previous approaches. On the practical side, we show our algorithms can handle a wide variety of programs from the literature and synthesize bounds that are remarkably tighter than previous results, in some cases by thousands of orders of magnitude.

A code generation system generates programming language code based on an input natural language description. State-of-the-art approaches rely on neural networks for code generation. However, these code generators suffer from two problems. One is the long dependency problem, where a code element often depends on another far-away code element. A variable reference, for example, depends on its definition, which may appear quite a few lines before. The other problem is structure modeling, as programs contain rich structural information. In this paper, we propose a novel tree-based neural architecture, TreeGen, for code generation. TreeGen uses the attention mechanism of Transformers to alleviate the long-dependency problem, and introduces a novel AST reader (encoder) to incorporate grammar rules and AST structures into the network. We evaluated TreeGen on a Python benchmark, HearthStone, and two semantic parsing benchmarks, ATIS and GEO. TreeGen outperformed the previous state-of-the-art approach by 4.5 percentage points on HearthStone, and achieved the best accuracy among neural network-based approaches on ATIS (89.1%) and GEO (89.6%). We also conducted an ablation test to better understand each component of our model.

Programming by example (PBE) is an important subproblem of program synthesis, and PBE techniques have been applied to many domains. Though many techniques for accelerating PBE systems have been explored, the scalability remains one of the main challenges: There is still a gap between the performances of state-of-the-art synthesizers and the industrial requirement. To further speed up solving PBE tasks, in this paper, we propose a novel PBE framework MaxFlash. MaxFlash uses a model based on structural probability, named topdown prediction models, to guide a search based on dynamic programming, such that the search will focus on subproblems that form probable programs, and avoid improbable programs. Our evaluation shows that MaxFlash achieves × 4.107− × 2080 speed-ups against state-of-the-art solvers on 244 real-world tasks.