waashk/acm huggingface dataset:
on the combinatorial and algebraic complexity of quantifier elimination  in this paper, a new algorithm for performing quantifier elimination from first order formulas over real closed fields in given. this algorithm improves the complexity of the asymptotically fastest algorithm for this problem, known to this data. a new feature of this algorithm is that the role of the algebraic part (the dependence on the degrees of the imput polynomials) and the combinatorial part (the dependence on the number of polynomials) are sparated. another new feature is that the degrees of the polynomials in the equivalent quantifier-free formula that is output, are independent of the number of input polynomials. as special cases of this algorithm new and improved algorithms for deciding a sentence in the first order theory over real closed fields, and also for solving the existential problem in the first order theory over real closed fields, are obtained.  saugata basu marie-françoise roy
convexity algorithms in parallel coordinates  with a system of parallel coordinates, objects in rn can be represented with planar "graphs" (i.e., planar diagrams) for arbitrary n [21]. in r2, embedded in the projective plane, parallel coordinates induce a point -&gt; line duality. this yields a new duality between bounded and unbounded convex sets and hstars (a generalization of hyperbolas), as well as a duality between convex union (convex merge) and intersection. from these results, algorithms for constructing the intersection and convex merge of convex polygons in o(n) time and the convex hull on the plane in o(log n) for real-time and o(n log n) worst-case construction, where n is the total number of points, are derived. by virtue of the duality, these algorithms also apply to polygons whose edges are a certain class of convex curves. these planar constructions are studied prior to exploring generalizations to n-dimensions. the needed results on parallel coordinates are given first.  alfred inselberg mordechai reif tuval chomut
on the complexity of ram with various operation sets  we prove that polynomial time bounded rams with the instruction set [shift, +, x, boolean ] accept exactly the languages in pspace. this generalizes previous results: [5] showed the same for the instruction set that does not include multiplication, [5] and [7] proved the weaker theorems, that rams (and even prams) with this instruction set could be simulated in exptape. the pram result is a simple corollary to our theorems. we also introduce other powerful string- manipulating instructions for rams, show a nontrivial simulation of turing machines by these rams, and show that in a sense such simulations are optimal.  janos simon mario szegedy
on the efficiency of subsumption algorithms  the costs of subsumption algorithms are analyzed by an estimation of the maximal number of unification attempts (worst-case unification complexity) made for deciding whether a clause c subsumes a clause d. for this purpose the clauses c and d are characterized by the following parameters: number of variables in c, number of literals in c, number of literals in d, and maximal length of the literals. the worst- case unification complexity immediately yields a lower bound for the worst- case time complexity.  first, two well-known algorithms (chang-lee, stillman) are investigated. both algorithms are shown to have a very high worst-case time complexity. then, a new subsumption algorithm is defined, which is based on an analysis of the connection between variables and predicates in c. an upper bound for the worst- case unification complexity of this algorithm, which is much lower than the lower bounds for the two other algorithms, is derived. examples in which exponential costs are reduced to polynomial costs are discussed. finally, the asymptotic growth of the worst-case complexity for all discussed algorithms is shown in a table (for several combinations of the parameters).  g. gottlob a. leitsch
some perspectives on computational complexity  in past decades, the theory of computational complexity has flourished in terms of both the revelation of its internal structures and the unfolding of its numerous applications. in this paper we discuss several persistent and interwoven themes underlying many of these accomplishments. chief among them are the interplay between communication and computation, the power of problem reduction, and the increasingly prominent role played by classical mathematics. we will also speculate on a few promising directions for future development of computational complexity.  andrew chi-chih yao
ccs expressions, finite state processes, and three problems of equivalence  we examine the computational complexity of testing finite state processes for equivalence, in the calculus of communicating systems (ccs). this equivalence problem in ccs is presented as a refinement of the familiar problem of testing whether two nondeterministic finite state automata (n.f.s.a.) accept the same language. three notions of equivalence, proposed for ccs, are investigated: (1) observation equivalence, (2) congruence, and (3) failure equivalence. we show that observation equivalence (@@@@) can be tested in cubic time and is the limit of a sequence of equivalence notions (@@@@k), where, @@@@1 is the familiar n.f.s.a. equivalence and, for each fixed k, @@@@k is pspace- complete. we provide an o(nlogn) test for congruence for n state processes of bounded fanout, by extending the algorithm that minimizes the states of d.f.s.a.'s. finally, we show that, even for a very restricted type of process, testing for failure equivalence is pspace-complete.  paris c. kanellakis scott a. smolka
computing algebraic formulas with a constant number of registers  we show that, over an arbitrary ring, the functions computed by polynomial- size algebraic formulas are also computed by polynomial-length algebraic straight- line programs which use only 3 registers (or 4 registers, depending on some definitions). we also show that polynomial-length products of 3 × 3 matrices compute precisely those functions that polynomial-size formulas compute (whereas, for general rings, polynomial-length 3-register straight- line programs compute strictly more functions than polynomial-size formulas). this can be viewed as an extension of the results of barrington in [ba1,ba2] from the boolean setting to the algebraic setting of an arbitrary ring.  richard cleve
a polynomial linear search algorithm for the n-dimensional knapsack problem  we present a linear search algorithm which decides the n-dimensional knapsack problem in n4log(n) + 0.(n3) steps. this algorithm works for inputs consisting of n numbers for some arbitrary but fixed integer n. this result solves an open problem posed for example in [6] and [7] by dobkin / lipton and a.c.c. yao, resp.. it destroys the hope of proving large lower bounds for this np- complete problem in the model of linear search algorithms.  friedhelm meyer auf der heide
polynomial time solutions of some problems of computational algebra  the first structure theory in abstract algebra was that of finite dimensional lie algebras (cartan-killing), followed by the structure theory of associative algebras (wedderburn-artin). these theories determine, in a non- constructive way, the basic building blocks of the respective algebras (the radical and the simple components of the factor by the radical). in view of the extensive computations done in such algebras, it seems important to design efficient algorithms to find these building blocks.  we find polynomial time solutions to a substantial part of these problems. we restrict our attention to algebras over finite fields and over algebraic number fields. we succeed in determining the radical (the "bad part" of the algebra) in polynomial time, using (in the case of prime characteristic) some new algebraic results developed in this paper. for associative algebras we are able to determine the simple components as well. this latter result generalizes factorization of polynomials over the given field. correspondingly, our algorithm over finite fields is las vegas.  some of the results generalize to fields given by oracles.  some fundamental problems remain open. an example: decide whether or not a given rational algebra is a noncommutative field.  k friedl l rónyai
bandwidth constrained np-complete problems  bandwidth restrictions are considered on several np-complete problems, including the following problems:  (1) 3-satisfiability,  (2) independent set and vertex cover,  (3) simple max cut  (4) partition into triangles,  (5) 3-dimensional matching,  (6) exact cover by 3 sets,  (7) dominating set,  (8) graph grundy numbering (for graphs of finite degree),  (9) 3-colorability,  (10) directed and undirected hamiltonian circuit,  (11) bandwidth minimization, and  (12) feedback vertex set and feedback arc set.  it is shown that each of the problems (1)-(12) when restricted to graphs (formulas, triples, or sets) of bandwidth bounded by a function f is log space hard for the complexity class ntisp (poly,f(n)). (ntisp(poly,f(n)) denotes the family of problems solvable nondeterministically in polynomial time and simultaneous f(n) space, e.g., ntisp(poly,poly) np and ntisp(poly, log n) nspace(log n).). in fact, (1)-(9) are log space complete for ntisp(poly,f(n)) when the bandwidth is bounded by the function f. this means, for example, that (1)-(9) provide several new examples of problems complete for nspace(log n), and hence solvable in polynomial time deterministically, when restricted to bandwidth log2n. in general, for a function f, if any of the problems (1)-(12), when restricted to bandwidth f(n), could be solved deterministically in polynomial time, then ntisp(poly, f(n)) @@@@ p. (this does not seem particularly likely even when f(n) log2n.) this indicates that several np- complete problems become easier with diminishing bandwidth. however, they remain intractable unless the bandwidth is restricted to c-log2n, for some c>0.  burkhard monien ivan hal sudborough
reliable computation with cellular automata  we construct a one- dimensional array of cellular automata on which arbitrarily large computations can be implemented reliably, even though each automaton at each step makes an error with some constant probability. to compute reliably with unreliable components, von neumann proposed boolean circuits whose intricate interconnection pattern (arising from the error- correcting organization) he had to assume to be immune to errors. in a uniform cellular medium, the error- correcting organization exists only in "software", therefore errors threaten to disable it. the real technical novelty of the paper is therefore the construction of a self-repairing organization.  peter gacs
a fast parallel algorithm for the maximal independent set problem  a parallel algorithm is presented which accepts as input a graph g and produces a maximal independent set of vertices in g. on a p-ram without the concurrent write or concurrent read features, the algorithm executes in o((log n)4) time and uses o((n/log n)3) processors, where n is the number of vertices in g.  the algorithm has several novel features that may find other applications. these include the use of balanced incomplete block designs to replace random sampling by deterministic sampling, and the use of a "dynamic pigeonhole principle" that generalizes the conventional pigeonhole principle.  richard m. karp avi wigderson
mechanizing a theory of program composition for unity compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. chandy and sanders [2000] have proposed a new approach to reasoning about composition, which charpentier and chandy [1999] have illustrated by developing a large example in the unity formalism. the present paper describes extensive experiments on mechanizing the compositionality theory and the example, using the proof tool isabelle. broader issues are discussed, in particular, the formalization of program states. the usual representation based upon maps from variables to values is contrasted with the alternatives, such as a signature of typed variables. properties need to be transferred from one program component's signature to the common signature of the system. safety properties can be so transferred, but progress properties cannot be. using polymorphism, this problem can be circumvented by making signatures sufficiently flexible. finally the proof of the example itself is outlined. lawrence c. paulson
dynamically maintaining configurations in the plane (detailed abstract)  for a number of common configurations of points (lines) in the plane, we develop datastructures in which insertions and deletions of points (or lines, respectively) can be processed rapidly without sacrificing much of the efficiency of query answering of known static structures for these configurations. as a main result we establish a fully dynamic maintenance algorithm for convex hulls that can process insertions and deletions of single points in only o(log3n) steps or less per transaction, where n is the number of points currently in the set. the algorithm has several intriguing applications, including that one can "peel" a set of n points in only o(log3n) steps and that one can maintain two sets at a costs of only o(log3n) or less per insertion and deletion such that it never takes more than o(log2n) steps to determine whether the two sets are separable by a straight line. also efficient algorithms are obtained for dynamically maintaining the common intersection of a set of half-spaces and for dynamically maintaining the maximal elements of a set of plane points. the results are all derived by means of one master technique, which is applied repeatedly and which seems to capture an appropriate notion of "decomposability" for configurations.  mark h. overmars jan van leeuwen
weak alternating automata are not that weak  automata on infinite words are used for specification and verification of nonterminating programs. different types of automata induce different levels of expressive power, of succinctness, and of complexity. alternating automata have both existential and universal branching modes and are particularly suitable for specification of programs. in a weak alternating automata the state space is partitioned into partially ordered sets, and the automaton can proceed from a certain set only to smaller sets. reasoning about weak alternating automata is easier than reasoning about alternating automata with no restricted structure. known translations of alternating automata to weak alternating automata involve determinization, and therefore involve a double- exponential blow-up. in this paper we describe a quadratic translation, which circumvents the need for determinization, of buchi and co-buchi alternating automata to weak alternating automata. beyond the independent interest of such a translation, it gives rise to a simple complementation algorithm for nondeterministic buchi automata.  orna kupferman moshe y. vardi
topological matching  there is a lot of practical and theoretical interest in designing algorithms to process digital pictures. of particular interest are problems arising when one starts with an nxn array of pixels and stores it, one pixel per processor, in some sort of array-like parallel computer. in this paper we give an optimal (n) time solution, based on a simpler (n) time solution for a more powerful computer called a mesh computer. beyer suggested that this problem was a prime candidate for a non-linear recognition problem, but our result shows that this is not true.  quentin f. stout
confluence properties of weak and strong calculi of explicit substitutions  categorical combinators [curien 1986/1993; hardin 1989; yokouchi 1989] and more recently λ -calculus [abadi 1991; hardin and levy 1989], have been introduced to provide an explicit treatment of substitutions in the λ-calculus. we reintroduce here the ingredients of these calculi in a self- contained and stepwise way, with a special emphasis on confluence properties. the main new results of the paper with respect to curien [1986/1993], hardin [1989], abadi [1991], and hardin and levy [1989] are the following:  (1) we present a confluent weak calculus of substitutions, where no variable clashes can be feared;(2) we solve a conjecture raised in abadi [1991]: λ -calculus is not confluent (it is confluent on ground terms only).  this unfortunate result is "repaired" by presenting a confluent version of λ -calculus, named the λenv-caldulus in hardin and levy [1989], called here the confluent λ -calculus.  pierre-louis curien therese hardin jean-jacques levy
chain mulitplication of matrices of approximately or exactly the same size  we present a different approach to finding an optimal computation order; it exploits both the difference between the size of the matrices and the difference between the number of nonzero elements in the matrices. therefore, this technique can be usefully applied where the matrices are almost or exactly the same size. we show that using the proposed technique, an optimal computation order can be determined in time o(n) if the matrices have the same size, and in time o(n) otherwise.  nicola santoro
approximate motion planning and the complexity of the boundary of the union of simple geometric figures  we study rigid motions of a rectangle amidst polygonal obstacles. the best known algorithms for this problem have running time (n2) where n is the number of obstacle corners. we introduce the tightness of a motion planning problem as a measure of the difficulty of a planning problem in an intuitive sense and describe an algorithm with running time  ((a/b * 1/ε crit + 1)n(log n)2), where a ≥ b are the lengths of the sides of a rectangle and εcrit is the tightness of the problem. we show further that the complexity (= number of vertices) of the boundary of n bow-ties (c.f. figure 1.1) is  (n). similar results for the union of other simple geometric figures such as triangles and wedges are also presented.  helmut alt rudolf fleischer michael kaufmann kurt mehlhorn stefan näher stefan schirra christian uhrig
empty types in polymorphic lambda calculus  the model theory of simply typed and polymorphic (second-order) lambda calculus changes when types are allowed to be empty. for example, the "polymorphic boolean" type really has exactly two elements in a polymorphic model only if the "absurd" type ∀t.t is empty. the standard β-ε axioms and equational inference rules which are complete when all types are nonempty are not complete for models with empty types. without a little care about variable elimination, the standard rules are not even sound for empty types. we extend the standard system to obtain a complete proof system for models with empty types. the completeness proof is complicated by the fact that equational "term models" are not so easily obtained: in contrast to the nonempty case, not every theory with empty types is the theory of a single model.  a. r. meyer j. c. mitchell e. moggi r. statman
hypergeometric dispersion and the orbit problem  we describe an algorithm for finding the positive integer solutions n of orbit problems of the form αn = β where α and β are given elements of a field k. our algorithm corrects the bounds given in [7], and shows that the problem is not polynomial in the euclidean norms of the polynomials involved. combined with a simplified version of the algorithm of [8] for the "specification of equivalence", this yields a complete algorithm for computing the dispersion of polynomials in nested hypergeometric extensions of rational function fields. this is a necessary step in computing symbolic sums, or solving difference equations, with coefficients in such fields. we also solve the related equations  ;p(αn&amp;l; t;/italic>) = 0 and p(n, αn) = 0 where p is a given polynomial and α is given.  sergei a. abramov manuel bronstein
block-matrix operations using orthogonal trees  hypercube algorithms are presented for distributed block-matrix operations. these algorithms are based entirely on an interconnection scheme which involves two orthogonal sets of binary trees. this switching topology makes use of all hypercube interconnection links in a synchronized manner.  an efficient novel matrix-vector multiplication algorithm based on this technique is described. also, matrix transpose operations moving just pointers rather than actual data, have been implemented for some applications by taking advantage of the above tree structures. for the cases where actual physical vector and matrix transposes are needed, possible techniques, including extensions of the above scheme, are discussed.  the algorithms support submatrix partitionings of the data, instead of being limited to row and/or column partitionings. this allows efficient use of nodal vector processors as well as shorter interprocessor communication packets. it also produces a favorable data distribution for applications which involve near neighbor operations such as image processing. the algorithms are based on an interprocessor communication paradigm which involves variable length, tagged block data transfers. they have been implemented on an intel ipsc hypercube system with the support of the hypercube library developed at the christian michelsen institute.  a. c. elster a. p. reeves
on the parallel decomposability of geometric problems  there is a large and growing body of literature concerning the solution of geometric problems on mesh-connected arrays of processors [5,9,14,17]. most of these algorithms are optimal (i.e., run in time  (_n1/d) on a d-dimensional n-processor array), and they all assume that the parallel machine is trying to solve a problem of size n on an n-processor array. what happens when we have parallel machine for efficiently solving a problem of size p, and we are interested in using it to solve a problem of size n < p? the answer to that question has to do with a fundamental, and yet (at least so far) little- studied property of geometric problems: their parallel-decomposability. more specifically, given that a problem of size p can be solved on a parallel machine p faster by a factor of (say) s(p) than on a ram alone, then that problem is fully parallel-decomposable for p if a ram to which the parallel machine p is attached can solve arbitrarily large problems with a speedup of also s(p) when compared to a ram alone. the issue has been settled for the sorting problem when p is a linear systolic array [1,2,3,11]. here we show that many geometric problems are fully parallel-decomposable for (multidimensional) mesh-connected arrays of processors.  m. j. atallah j. j. tsay
concurrent transition system semantics of process networks  using concurrent transition systems [sta86], we establish connections between three models of concurrent process networks, kahn functions, input/output automata, and labeled processes. for each model, we define three kinds of algebraic operations on processes: the product operation, abstraction operations, and connection operations. we obtain homomorphic mappings, from input/output automata to labeled processes, and from a subalgebra (called "input/output processes") of labeled processes to kahn functions. the proof that the latter mapping preserves connection operations amounts to a new proof of the "kahn principle." our approach yields: (1) extremely simple definitions of the process operations; (2) a simple and natural proof of the kahn principle that does not require the use of "strategies" or "scheduling arguments"; (3) a semantic characterization of a large class of labeled processes for which the kahn principle is valid, (4) a convenient operational semantics for nondeterminate process networks.  e. w. stark
bounding the number of geometric permutations induced by k-transversals  we prove that a (k 1)-separated family of n compact convex sets in & lt;f>rd can be met byk-transversals in at mostod&amp;l; t;sup>d22k+1-2knk+1& lt;rp post="par">kd-k or, for fixed k and d, o(nk(k+1)(d k)) different order types. this is the first non-trivial bound for 1< k<d 1.  jacob e. goodman richard pollack rephael wenger