Search

In this paper an implicit characterization of the complexity classes k - EXP and k - FEXP , for k ≥ 0 , is given, by a type assignment system for a stratified λ -calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic ( ELL ), and the hierarchy of complexity classes k - EXP is characterized by a hierarchy of types. [ABSTRACT FROM AUTHOR]

Martin-Löf defined algorithmic randomness, the use of martingales in this definition and several variants were explored by Schnorr, and Lutz introduced resource-bounded randomness. Ambos-Spies et al. have studied resource-bounded randomness under time-bounds and have shown that resource-bounded randomness implies resource-bounded genericity. While the genericity of Ambos-Spies is based on time-bound on finite-extension strategy, the genericity of Dowd, the main topic of this paper, is based on an analogy of the forcing theorem. For a positive integer r , an oracle D is r -generic in the sense of Dowd ( r -Dowd) if the following holds: If a certain formula F on an exponential-sized portion of D is a tautology then a polynomial-sized subfunction of D forces F to be a tautology. Here, r is the number of occurrences of query symbols in F . The relationship between resource-bounded randomness and Dowd-type genericity has been not clear so far. We show that there exists a primitive recursive function t ( n ) with the following property: Every t ( n ) -random set is r -Dowd for each positive integer r . A proof is done by means of constructing resource-bounded martingales. In our former paper, we left an open problem whether there exists a primitive recursive set which is r -Dowd for every positive integer r . In our recent work, we give an affirmative answer to the problem. The main theorem of the present paper gives an alternative proof of the affirmative answer. [ABSTRACT FROM AUTHOR]

This paper studies exact algorithms for the Maximum Induced Matching problem, in which an n -vertex graph is given and we are asked to find a set of maximum number of edges in the graph such that no pair of edges in the set have a common endpoint or are adjacent by another edge. This problem has applications in many different areas. We give several structural properties of the problem and show that the problem can be solved in O ⁎ ( 1.4231 n ) time and polynomial space or O ⁎ ( 1.3752 n ) time and exponential space. [ABSTRACT FROM AUTHOR]

Abstract: This paper presents a pattern language based on regular expressions that allows the introduction of variables that can be instantiated to portions of the path that matches the expression. The paper will define a simple syntax for the language and its formal semantics. It will also study a modification of finite state automata that, through the introduction of actions on transitions, allows the variables to be instantiated while matching the expression. Finally, the paper will show that the problem of answering queries with variables is inherently harder than simple matching, essentially because, even for fairly simple expressions, the size of the results can be exponential in the size of the graph. The class of expressions and a class of graphs for which query answering is polynomial will be identified, and a processing algorithm for these expressions based on the intersection graph will be provided and analyzed. [Copyright &y& Elsevier]

Abstract: “Clarithmetic” is a generic name for formal number theories similar to Peano arithmetic, but based on computability logic instead of the more traditional classical or intuitionistic logics. Formulas of clarithmetical theories represent interactive computational problems, and their “truth” is understood as existence of an algorithmic solution. Imposing various complexity constraints on such solutions yields various versions of clarithmetic. The present paper introduces a system of clarithmetic for polynomial time computability, which is shown to be sound and complete. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a polynomial time solution and, furthermore, such a solution can be efficiently extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a polynomial time solution is represented by some theorem T of the system. The paper is written in a semitutorial style and targets readers with no prior familiarity with computability logic. [Copyright &y& Elsevier]

Abstract: Bisimulation equivalence is decidable in polynomial time for both sequential and commutative normed context-free processes, known as BPA and BPP, respectively. Despite apparent similarity between the two classes, different algorithmic techniques were used in each case. We provide one polynomial-time algorithm that works in a superclass of both normed BPA and BPP. It is derived in the setting of partially-commutative context-free processes, a new process class introduced in the paper. It subsumes both BPA and BPP and seems to be of independent interest. Expressibility issue of the new class, in comparison with the normed PA class, is also tackled in the paper. [Copyright &y& Elsevier]

New post-quantum Key Encapsulation Mechanism (KEM) designs, evaluated as part of the NIST PQC standardization Project, pose challenging tradeoffs between communication bandwidth and computational overheads. Several KEM designs evaluated in Round-2 of the project are based on QC-MDPC codes. BIKE-2 uses the smallest communication bandwidth, but its key generation requires a costly polynomial inversion. In this paper, we provide details on the optimized polynomial inversion algorithm for QC-MDPC codes (originally proposed in the conference version of this work). This algorithm makes the runtime of BIKE-2 key generation tolerable. It brings a speedup of 11.4× over the commonly used NTL library, and 83.5× over OpenSSL. We achieve additional speedups by leveraging the latest Intel's Vector-PCLMULQDQ instructions, 14.3× over NTL and 103.9× over OpenSSL. Our algorithm and implementation were the reason that BIKE team chose BIKE-2 as the only scheme for its Round-3 specification (now called BIKE). [ABSTRACT FROM AUTHOR]

Abstract: Haplotyping, also known as haplotype phase prediction, is the problem of predicting likely haplotypes based on genotype data. One fast computational haplotyping method is based on an evolutionary model where a perfect phylogenetic tree is sought that explains the observed data. An extension of this approach tries to incorporate prior knowledge in the form of a set of candidate haplotypes from which the right haplotypes must be chosen. The objective is to increase the accuracy of haplotyping methods, but it was conjectured that the resulting formal problem constrained perfect phylogeny haplotyping might be NP-complete. In the paper at hand we present a polynomial-time algorithm for it. Our algorithmic ideas also yield new fixed-parameter algorithms for related haplotyping problems based on the maximum parsimony assumption. [Copyright &y& Elsevier]

Abstract: It is well-known that the existential theory of equations in free groups is decidable. This is a celebrated result of Makanin which was published 1982. Makanin did not discuss complexity issues, but later it was shown that the scheme of his algorithm is not primitive recursive. In this paper we present an algorithm that works in polynomial space. This improvement is based upon an extension of Plandowski’s techniques for solving word equations. We present a pspace-algorithm in a more general setting where each variable has a rational constraint, that is, the solution has to respect a specification given by a regular word language. We obtain our main result about the existential theory in free groups as a corollary of the corresponding statement in free monoids with involution. [Copyright &y& Elsevier]

Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has received special attention. However, all these works impose a strong restriction on the possible valuations of atomic propositions: whether a configuration of the pushdown system satisfies an atomic proposition or not can only depend on the current control state of the pushdown automaton and on its topmost stack symbol. In this paper we consider LTL with regular valuations: the set of configurations satisfying an atomic proposition can be an arbitrary regular language. The model-checking problem is solved via two different techniques, with an eye on efficiency. The resulting algorithms are polynomial in certain measures of the problem which are usually small, but can be exponential in the size of the problem instance. However, we show that this exponential blowup is inevitable. The extension to regular valuations allows to model problems in different areas; for instance, we show an application to the analysis of systems with checkpoints. We claim that our model-checking algorithms provide a general, unifying and efficient framework for solving them. [Copyright &y& Elsevier]

Some computationally hard problems, e.g., deduction in logical knowledge bases– are such that part of an instance is known well before the rest of it, and remains the same for several subsequent instances of the problem. In these cases, it is useful to preprocess off-line this known part so as to simplify the remaining on-line problem. In this paper we investigate such a technique in the context of intractable, i.e., NP-hard, problems. Recent results in the literature show that not all NP-hard problems behave in the same way: for some of them preprocessing yields polynomial-time on-line simplified problems (we call them compilable), while for other ones their compilability implies some consequences that are considered unlikely. Our primary goal is to provide a sound methodology that can be used to either prove or disprove that a problem is compilable. To this end, we define new models of computation, complexity classes, and reductions. We find complete problems for such classes, “completeness” meaning they are “the less likely to be compilable.” We also investigate preprocessing that does not yield polynomial-time on-line algorithms, but generically “decreases” complexity. This leads us to define “hierarchies of compilability,” that are the analog of the polynomial hierarchy. A detailed comparison of our framework to the idea of “parameterized tractability” shows the differences between the two approaches. [Copyright &y& Elsevier]