waashk/dblp huggingface dataset:
techniques from combinatorial approximation algorithms yield efficient algorithms for random 2k-sat. we apply techniques from the theory of approximation algorithms to the problem of deciding whether a random k-sat formula is satisfiable. let form n,k,m denote a random k-sat instance with n variables and m clauses. using known approximation algorithms for max cut or min bisection, we show how to certify that formn,4,m is unsatisfiable efficiently, provided that m ≥ cn2 for a sufficiently large constant c > 0. in addition, we present an algorithm based on the lovász υ' function that decides within polynomial expected time whether formn,k,m is satisfiable, provided that k is even and m ≥ c ċ 4knk/2. finally, we present an algorithm that approximates random max 2-sat on input formn,2,m within a factor of 1 - o(n/m)1/2 in expected polynomial time. for m ≥ cn.
automated techniques for provably safe mobile code. we present a general framework for provably safe mobile code. it relies on a formal definition of a safety policy and explicit evidence for compliance with this policy which is attached to a binary. concrete realizations of this framework are proof-carrying code, where the evidence for safety is a formal proof generated by a certifying compiler, and typed assembly language, where the evidence for safety is given via type annotations propagated throughout the compilation process in typed intermediate languages. validity of the evidence is established via a small trusted type checker, either directly on the binary or indirectly on proof representations in a logical framework.
on the positional determinacy of edge-labeled games. it is well known that games with the parity winning condition admit positional determinacy: the winner has always a positional (memoryless) strategy. this property continues to hold if edges rather than vertices are labeled. we show that in this latter case the converse is also true. that is, a winning condition over arbitrary set of colors admits positional determinacy in all games if and only if it can be reduced to a parity condition with some finite number of priorities.
continuity and computability of reachable sets. the computation of reachable sets of nonlinear dynamic and control systems is an important problem of systems theory. in this paper we consider the computability of reachable sets using turing machines to perform approximate computations. we use weihrauch's type-two theory of effectivity for computable analysis and topolgy, which provides a natural setting for performing computations on sets and maps. the main result is that the reachable set is lower-computable, but is only outer-computable if it equals the chain-reachable set. in the course of the analysis, we extend the computable topology theory to locally-compact hausdorff spaces and semicontinuous set-valued maps, and provide a framework for computing approximations.
the evaluation of first-order substitution is monadic second-order compatible. we denote first-order substitutions of finite and infinite terms by function symbols indexed by the sequences of first-order variables to which substitutions are made. we consider the evaluation mapping from infinite terms to infinite terms that evaluates these substitution operations. this mapping may perform infinitely many nested substitutions, so that a term which has the structure of an infinite string can be transformed into one isomorphic to an infinite binary tree. we prove that this mapping is monadic second-order compatible which means that a monadic second-order formula expressing a property of the output term produced by the evaluation mapping can be translated into a monadic second-order formula expressing this property over the input term. this implies that, deciding the monadic second-order theory of the output term reduces to deciding that of the input term. as an application, we obtain another proof that the monadic second-order properties of the algebraic trees, which represent the behaviours of recursive applicative program schemes, are decidable. this proof extends to hyperalgebraic trees. these infinite trees correspond to certain recursive program schemes with functional parameters of arbitrary high type.
the recognizability of sets of graphs is a robust property. once the set of finite graphs is equipped with an algebra structure (arising from the definition of operations that generalize the concatenation of words), one can define the notion of a recognizable set of graphs in terms of finite congruences. applications to the construction of efficient algorithms and to the theory of context-free sets of graphs follow naturally. the class of recognizable sets depends on the signature of graph operations. we consider three signatures related respectively to hyperedge replacement (hr) context-free graph grammars, to vertex replacement (vr) context-free graph grammars, and to modular decompositions of graphs. we compare the corresponding classes of recognizable sets. we show that they are robust in the sense that many variants of each signature (where in particular operations are defined by quantifier-free formulas, a quite flexible framework) yield the same notions of recognizability. we prove that for graphs without large complete bipartite subgraphs, hr-recognizability and vr-recognizability coincide. the same combinatorial condition equates hr-context-free and vr-context-free sets of graphs. inasmuch as possible, results are formulated in the more general framework of relational structures.
tilings as a programming exercise. we investigate the problem of producing symmetric tilings by programs in a uniform way. by this, we mean that the construction of a tiling should be parameterized by the geometric model in which the tiling is defined (euclidean, hyperbolic, etc.), its formal symmetry group, the interpretation of this symmetry group in the geometric model and a specific tile that fits this interpretation. this parameterization can be obtained at a basic level using higher order functions as described in cousineau and mauny (the functional approach to programming, cambridge university press, cambridge, 1997) but this fails to reflect in the program the mathematical structure of tilings in an adequate way. we therefore explore the use of more abstract constructs such as modules and show that they allow to structure the program in a satisfying way. the objective caml programming language (objective caml, o'reilly, 2000) allows us to place this study in a convenient setting.
tree automata with one memory set constraints and cryptographic protocols. we introduce a class of tree automata that perform tests on a memory that is updated using function symbol application and projection. the language emptiness problem for this class of tree automata is shown to be in dexptime.we also introduce a class of set constraints with equality tests and prove its decidability by completion techniques and a reduction to tree automata with one memory.finally, we show how to apply these results to cryptographic protocols. we introduce a class of cryptographic protocols and show the decidability of secrecy for an arbitrary number of agents and an arbitrary number of (concurrent or successive) sessions, provided that only a bounded number of new data is generated. the hypothesis on the protocol (a restricted copying ability) is shown to be necessary: without this hypothesis, we prove that secrecy is undecidable, even for protocols without nonces.
constructive design of a hierarchy of semantics of a transition system by abstract interpretation. we construct a hierarchy of semantics by successive abstract interpretations. starting from the maximal trace semantics of a transition system, we derive the big-step semantics, termination and nontermination semantics, plotkin's natural, smyth's demoniac and hoare's angelic relational semantics and equivalent nondeterministic denotational semantics (with alternative powerdomains to the egli-milner and smyth constructions), d. scott's deterministic denotational semantics, the generalized and dijkstra's conservative/liberal predicate transformer semantics, the generalized/total and hoare's partial correctness axiomatic semantics and the corresponding proof methods. all the semantics are presented in a uniform fixpoint form and the correspondences between these semantics are established through composable galois connections, each semantics being formally calculated by abstract interpretation of a more concrete one using kleene and/or tarski fixpoint approximation transfer theorems. copyright 2002 elsevier science b.v.
parsing as abstract interpretation of grammar semantics. earley's parsing algorithm is shown to be an abstract interpretation of a refinement of the derivation semantics of context-free grammars.
strategies for combining decision procedures. implementing efficient algorithms for combining decision procedures has been a challenge and their correctness precarious. in this paper we describe an inference system that has the classical nelson-oppen procedure at its core and includes several optimizations: variable abstraction with sharing, canonization of terms at the theory level, and shostak's streamlined generation of new equalities for theories with solvers. the transitions of our system are fine-grained enough to model most of the mechanisms currently used in designing combination procedures. in particular, with a simple language of regular expressions we are able to describe several combination algorithms as strategies for our inference system, from the basic nelson-oppen to the very highly optimized one recently given by shankar and rueß. presenting the basic system at a high level of generality and nondeterminism allows transparent correctness proofs that can be extended in a modular fashion when new features are introduced in the system.
classifying rna pseudoknotted structures. computational prediction of the minimum free energy (mfe) secondary structure of an rna molecule from its base sequence is valuable in understanding the structure and function of the molecule. since the general problem of predicting pseudoknotted secondary structures is np-hard, several algorithms have been proposed that find the mfe secondary structure from a restricted class of secondary structures. in this work, we order the algorithms by generality of the structure classes that they handle. we provide simple characterizations of the classes of structures handled by four algorithms, as well as linear time methods to test whether a given secondary structure is in three of these classes. we report on the percentage of biological structures from the pseudobase and gutell databases that are handled by these three algorithms.
generalized satisfiability problems: minimal elements and phase transitions. we develop a probabilistic model on the generalized satisfiability problems defined by schaefer (in: proceedings of the 10th stoc, san diego, ca, usa, association for computing machinery, new york, 1978, pp. 216-226) for which the arity of the constraints is fixed in order to study the associated phase transition. we establish new results on minimal elements associated with such generalized satisfiability problems. these results are the keys of the exploration we conduct on the location and on the nature of the phase transition for generalized satisfiability. we first prove that the phase transition occurs at the same scale for every reasonable problem and we provide lower and upper bounds for the associated critical ratio. our framework allows one to get these bounds in a uniform way, in particular, we obtain a lower bound proportional to the number of variables for k-sat without analyzing any algorithm. finally, we reveal the seed of coarseness for the phase transition of generalized satisfiability: 2-xor-sat.
generalised fine and wilf's theorem for arbitrary number of periods. the well known fine and wilf's theorem for words states that if a word has two periods and its length is at least as long as the sum of the two periods minus their greatest common divisor, then the word also has as period the greatest common divisor. we generalise this result for an arbitrary number of periods. our bound is strictly better in some cases than previous generalisations. moreover, we prove it optimal. we show also that any extrenal word is unique up to letter renaming and give an algorithm to compute both the bound and a corresponding extremal word.
hypercomputation: philosophical issues. a survey of the field of hypercomputation, including discussion of four a priori objections to the possibility of hypercomputation. an exegesis of turing's pre- and post-war writings on the mind is given, and turing's views on the scope of machines are discussed.
injective synchronisation: an extension of the authentication hierarchy. authentication is one of the foremost goals of many security protocols. it is most often formalised as a form of agreement, which expresses that the communicating partners agree on the values of a number of variables. in this paper we formalise and study an intensional form of authentication which we call synchronisation. synchronisation expresses that the messages are transmitted exactly as prescribed by the protocol description. synchronisation is a strictly stronger property than agreement for the standard intruder model, because it can be used to detect preplay attacks. in order to prevent replay attacks on simple protocols, we also define injective synchronisation. given a synchronising protocol, we show that a sufficient syntactic criterion exists that guarantees that the protocol is injective as well.
strictness, totality, and non-standard-type inference. in this paper we present two non-standard-type inference systems for conjunctive strictness and totality analyses of higher-order-typed functional programs and prove completeness results for both the strictness and the totality-type entailment relations. we also study the interactions between strictness and totality analyses, showing that the information obtainable by a system that combines the two analyses, even though more refined than the information given by the two separate systems, cannot be effectively used. a main feature of our approach is that all the results are proved by relying directly on the operational semantics of the programming language considered. this leads to a rather direct presentation which involves relatively little mathematical overhead. copyright 2002 elsevier science b.v.
a syntactical proof of the marriage lemma. we give a proof of the classical marriage lemma (amer. j. math. 72 (1950) 214) using completeness of hyperresolution. this argument is purely syntactical, and extends directly to the infinite case. as an application we give a purely syntactical version of a proof that resolution is exponential on the pigeon-hole principle.
on the hamming distance of constraint satisfaction problems. in this paper we consider a new optimization problem, called max hammingdistance(f) where f is a family of boolean constraints. this problem consists in finding two satisfying assignments that differ in the maximum number of variable values: in other words, the problem looks for the maximum difference between two models of the constraints given in input. we give a complete classification of the approximability properties of max hammingdistance(f) by using a specialization of the criteria introduced by schaefer in order to classify constraint satisfaction problems and subsequently used by khanna, sudan, trevisan, and williamson to classify constraint satisfaction optimization problems.
sharing one secret vs. sharing many secrets. a secret sharing scheme is a method for distributing a secret among several parties in such a way that only qualified subsets of the parties can reconstruct it and unqualified subsets receive no information about the secret. a multi-secret sharing scheme is the natural extension of a secret sharing scheme to the case in which many secrets need to be shared, each with respect to possibly different subsets of qualified parties. a multi-secret sharing scheme can be trivially realized by realizing a secret sharing scheme for each of the secrets.in this paper we address the natural questions of whether this simple construction is the most efficient as well, and, if not, how much improvement is possible over it, with respect to both efficiency measures used in the literature; namely, the maximum piece of information and the sum of all pieces of information distributed to all parties. we completely answer these questions, as follows. we show the first instance for which an improvement is possible; we prove a bound on how much improvement is possible with respect to both measures; and we show instances of multi-secret sharing schemes which achieve this improvement, with respect to both measures, thus showing that the above bound is tight.
a representation of stably compact spaces, and patch topology. this note presents a concrete representation of stably compact spaces. this is used to give a simple, and predicative, description of the patch topology of a stably compact space (j. pure appl. algebra, to appear).
tile rewriting grammars and picture languages. tile rewriting grammars (trg) are a new model for defining picture languages. a rewriting rule changes a homogeneous rectangular subpicture into an isometric one tiled with specified tiles. derivation and language generation with trg rules are similar to context-free grammars. a normal form and some closure properties are presented. we prove this model has greater generative capacity than the tiling systems of giammarresi and restivo and the grammars of matz, another generalization of context-free string grammars to 2d. examples are shown for pictures made by nested frames and spirals.
reducing space for index implementation. this article considers several strategies to implement efficiently full indexes on raw textual data. indexes are based on representations of all the suffixes of the original text, for which we describe three types of implementations aimed at reducing the memory space. the first method is a combination of compaction and minimization that leads to the compact suffix automaton. as a second method we show that considering a complement language can be useful especially when it is related to data compression. finally, approximation of the set of suffixes is the third technique used to reduce the space of the implementation.
description trees and tutte formulas. in this paper we introduce and enumerate families of description trees. these families of trees consist of plane trees in which the nodes are labelled by nonnegative integers, and where the label of each node satisfies a condition relating it to the labels of its sons.we give a recursive construction of these trees which translates simply in an equation for their generating function. by solving this equation via the quadratic method introduced by brown and tutte, we prove that this generating function is algebraic. for some families the number of trees we obtain is equal to the numbers given by tutte to enumerate different kinds of planar maps. we provide bijections between description trees and corresponding families of planar maps to explain these equalities.description trees are instances of objects that can be described by description operators; we conjecture that such families of objects have algebraic generating functions. they were find also to be related to the enumeration of pattern avoiding permutations.
longest repeats with a block of don't cares. a k-repeat is a string wk = u*k v that matches more than one substring of x, where * is the don't care letter and k > 0. we propose an o(n log n)-time algorithm for computing all longest k-repeats in a given string x = x[1..n]. the proposed algorithm uses suffix trees to fulfill this task and relies on the ability to answer lowest common ancestor queries in constant time.
the abc conjecture and correctly rounded reciprocal square roots. the reciprocal square root calculation α = 1/√ x is very common in scientific computations. having a correctly rounded implementation of it is of great importance in producing numerically predictable code among today's heterogenous computing environment. existing results suggest that to get the correctly rounded α in a floating point number system with p significant bits, we may have to compute up to 3p + 1 leading bits of α. however, numerical evidence indicates the actual number may be as small as 2p plus a few more bits. this paper attempts to bridge the gap by showing that this is indeed true, assuming the abc conjecture which is widely purported to hold. (but our results do not tell exactly how many more bits beyond the 2p bits, due to the fact that the constants involved in the conjecture are ineffective.) along the way, rough bounds which are comparable to the existing ones are also proven. the technique used here is a combination of the classical liouville's estimation and contemporary number theory.
a functorial semantics for multi-algebras and partial algebras, with applications to syntax. multi-algebras allow for the modelling of nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results. we propose a functorial presentation of various categories of multi-algebras and partial algebras, analogous to the classical presentation of algebras over a signature σ as cartesian functors from the algebraic theory over σ to set. we introduce two different notions of theory over a signature, both having a structure weaker than cartesian, and we consider functors from them to rel or pfn, the categories of sets and relations or partial functions, respectively.next we discuss how the functorial presentation provides guidelines when choosing syntactical notions for a class of algebras, and as an application we argue that the natural generalization of usual terms are "conditioned terms" for partial algebras, and "term graphs" for multi-algebras.
on axioms for commutative regular equations without addition. algebras of commutative languages consist of all subsets of a free commutative monoid over a given alphabet σ, and they are endowed with the operations of union, complex multiplication, kleene iteration (submonoid generation), and the empty set and the set whose unique element is the unit of the free monoid, as constants. there is a well-known equational axiomatization for these algebras. however, any such axiomatization is necessarily infinite. now, by removing the operation of union (addition) from the described algebras, the corresponding equational theory reduces to the collection of those equations which contain no symbols of addition. we supply a nontrivial list of equational axioms for the so obtained equational theory, and prove that it has no finite equational base, too.
compositional sos and beyond: a coalgebraic view of open systems. in this paper we address the issue of providing a structured coalgebra presentation of transition systems with algebraic structure on states determined by an equational specification . more precisely, we aim at representing such systems as coalgebras for an endofunctor on the category of -algebras. the systems we consider are specified by using arbitrary sos rules, which in general do not guarantee that bisimilarity is a congruence. we first show that the structured coalgebra representation works only for systems where transitions out of complex states can~be derived from transitions out of corresponding component states. this decomposition property of transitions indeed ensures that bisimilarity is a congruence. for a system not satisfying this requirement, next we propose a closure construction which adds context transitions, i.e., transitions that spontaneously embed a state into a bigger context or vice versa. the notion of bisimulation for the enriched system coincides with the notion of dynamic bisimilarity for the original one, i.e., with the coarsest bisimulation which is a congruence. this is sufficient to ensure that the structured coalgebra representation works for the systems obtained as result of the closure construction.