An abstract is not available for this content so a preview has been provided. As you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Proust is a small Racket program offering rudimentary interactive assistance in the development of verified proofs for propositional and predicate logic. It is constructed in stages, some of which are done by students before using it to complete proof exercises, and in parallel with the study of its theoretical underpinnings, including elements of Martin-Lof type theory. The goal is twofold: to demystify some of the machinery behind full-featured proof assistants such as Coq and Agda, and to better integrate the study of formal logic with other core elements of an undergraduate computer science curriculum.

Efficient implementations of sets and maps (dictionaries) are important in computer science, and balanced binary search trees are the basis of the best practical implementations. Pedagogically, however, they are often quite complicated, especially with respect to deletion. I present complete code (with justification and analysis not previously available in the literature) for a purely-functional implementation based on AA trees, which is the simplest treatment of the subject of which I am aware.

functional abstraction, and laziness, that are new to students often find hard on first encounter but are treated steadily and sympathetically through generally well-conceived, if occasionally irritating, practical examples to illuminate wider theory. The book’s main strength is the thorough treatment of I/O, monads, monoids, and stateful functional programming, where many introductory Haskell texts are covered just enough to enable basic interaction. The equally substantial coverage of these topics in Real World Haskell (O’Sullivan et al., 2009) may be better arranged for people who know what they are looking for, and lacks the distracting asides and cartoons, but the Real World Haskell examples are dry and have low motivation in comparison to Learn You a Haskell. . .. Frankly, if I had not been sent this book for review, I would have not bought it. But I will have no hesitation in lending it to my students.

We commonly think of mathematics as bringing precision to application domains, but its relationship with computer science is more complex. This experience report on the use of Racket and Haskell to teach a required first university CS course to students with very good mathematical skills focusses on the ways that programming forces one to get the details right, with consequent benefits in the mathematical domain. Conversely, imprecision in mathematical abstractions and notation can work to the benefit of beginning programmers, if handled carefully.

The transitional course following an introduction to computer science using functional programming must prepare students to handle a traditional, imperative-based curriculum while ensuring that the lessons of the introductory course are not lost. This paper describes the design of a second course using both Scheme and C, and examines the rationales behind the major design decisions.

We propose an exact algorithm for counting the models of propositional formulas in conjunctive normal form (CNF). Our algorithm is based on the detection of strong backdoor sets of bounded size; each instantiation of the variables of a strong backdoor set puts the given formula into a class of formulas for which models can be counted in polynomial time. For the backdoor set detection we utilize an efficient vertex cover algorithm applied to a certain “obstruction graph” that we associate with the given formula. This approach gives rise to a new hardness index for formulas, the clustering-width. Our algorithm runs in uniform polynomial time on formulas with bounded clustering-width. It is known that the number of models of formulas with bounded clique-width, bounded treewidth, or bounded branchwidth can be computed in polynomial time; these graph parameters are applied to formulas via certain (hyper)graphs associated with formulas. We show that clustering-width and the other parameters mentioned are incomparable: there are formulas with bounded clustering-width and arbitrarily large clique-width, treewidth, and branchwidth. Conversely, there are formulas with arbitrarily large clustering-width and bounded clique-width, treewidth, and branchwidth.

We examine the general problem of covering graphs by graphs: given a graph G, a collection $\mathcal{P}$ of graphs each on at most p vertices, and an integer r, is there a collection $\mathcal{C}$ of subgraphs of G, each belonging to $\mathcal{P}$ , such that the removal of the graphs in $\mathcal{C}$ from G creates a graph none of whose components have more than r vertices? We can also require that the graphs in $\mathcal{C}$ be disjoint (forming a “matching”). This framework generalizes vertex cover, edge dominating set, and minimal maximum matching. In this paper, we examine the parameterized complexity of the counting version of the above general problem. In particular, we show how to count the solutions of size at most k of the covering and matching problems in time O(n · r(pk+r)+2 f(k,p,r)), where n is the number of vertices in G and f is a simple polynomial. In order to achieve the additive relation between the polynomial and the non-polynomial parts of the time complexity of our algorithms, we use the compactor technique, the counting analogue of kernelization for parameterized decision problems.

Given a set of values x 1, x 2, ... x n , of which k are nonzero, the compaction problem is the problem of moving the nonzero elements into the first k consecutive memory locations. The chaining problem asks that the nonzero elements be put into a linked list. One can in addition require that the elements remain in the same order, leading to the problems of ordered compaction and ordered chaining respectively. Parallel algorithms for these problems were considered by Hagerup and Nowak (ICALP 1989). This paper improves their results by introducing a technique involving perfect hash functions. This leads to a deterministic algorithm for ordered compaction running on a CRCW PRAM in time O(log k/log log n) using n processors. A matching lower bound for unordered compaction is given. In addition, the ordered chaining problem is shown to be solvable in time O(α(k)) with n processors (where α is a functional inverse of Ackermann's function) and unordered chaining can be solved in constant time with n processors when k

We consider the problem of computing the minimum of n values, and several well-known generalizations (prefix minima, range minima, and all-nearest-smaller-values (ANSV) problems) for input elements drawn from the integer domain [1., s] where s≥n. Recent work [4] has shown that parallel algorithms that are sensitive to the size of the input domain can improve on more general parallel algorithms. The cited paper demonstrates an O(log log log s)-step algorithm on an n-processor Priority CRCW PRAM for finding the prefix-minima of n numbers in the range [1., s]. The best known upper bounds for the range minima and ANSV problems were previously O(log log n) (using algorithms for general input). This was also the best known upper bound for computing prefix minima or even just the minimum on the common CRCW PRAM; this model has a Θ(log n/ log log n) time separation from the stronger Priority model when using the same number of processors. In this paper we give simple and efficient algorithms for all of the above problems. These algorithms all take O(log log log s) time using an optimal number of processors and O(ns)∈ space on the Common CRCW PRAM. We also prove a lower bound demonstrating that no algorithm is asymptotically faster as a function of s, by showing that for s = 2^2^Ω (log n log log n) the upper bounds are tight.

The k-compaction problem arises when k out of n cells in an array are non-empty and the contents of these cells must be moved to the first k locations in the array. Parallel algorithms for k-compaction have obvious applications in processor allocation and load balancing; k-compaction is also an important subroutine in many recently developed parallel algorithms. We show that any EREW PRAM that solves the k-compaction problem requires Ω(√log n) time, even if the number of processors is arbitrarily large and k=2. On the CREW PRAM, we show that every n-processor algorithm for k-compaction problem requires Ω(loglog n) time, even if k=2. Finally, we show that O(log k) time can be achieved on the ROBUST PRAM, a very weak CRCW PRAM model.

We obtain faster algorithms for problems such as r-dimensional matching and r-set packing when the size k of the solution is considered a parameter. We first establish a general framework for finding and exploiting small problem kernels (of size polynomial in k). This technique lets us combine Alon, Yuster and Zwick's color-coding technique with dynamic programming to obtain faster fixed-parameter algorithms for these problems. Our algorithms run in time O(n+2O(k)), an improvement over previous algorithms for some of these problems running in time O(n+kO(k)). The flexibility of our approach allows tuning of algorithms to obtain smaller constants in the exponent.

We demonstrate a kernel of size O(k 2) for 3-Hitting Set (Hitting Set when all subsets in the collection to be hit are of size at most three), giving a partial answer to an open question of Niedermeier by improving on the O(k 3) kernel of Niedermeier and Rossmanith. Our technique uses the Nemhauser-Trotter linear-size kernel for Vertex Cover, and generalizes to demonstrating a kernel of size O(k r − − 1) for r -Hitting Set (for fixed r).

We study the parameterized complexity of detecting backdoor sets for instances of the propositional satisfiability problem (SAT) with respect to the polynomially solvable classes horn and 2-cnf. A backdoor set is a subset of variables; for a strong backdoor set, the simplified formulas resulting from any setting of these variables is in a polynomially solvable class, and for a weak backdoor set, there exists one setting which puts the satisfiable simplified formula in the class. We show that with respect to both horn and 2-cnf classes, the detection of a strong backdoor set is fixed-parameter tractable (the existence of a set of size k for a formula of length N can be decided in time f(k)NO(1)), but that the detection of a weak backdoor set is W[2]-hard, implying that this problem is not fixed-parameter tractable.

If the primary sequence of a protein is given, what is its three-dimensional structure? This is one of the most important and difficult problems in molecular biology and has tremendous implication to proteomics. Over the last three decades, this issue has been intensely researched. Protein threading represents one of the most promising techniques. So far, there are many protein structure prediction computer programs based on protein threading; however, almost none incorporates the pairwise contact (interaction) potential explicitly in its energy function, although scientists believe that pairwise interactions are important for fold recognition targets. The underlying reason for ignoring the pairwise potential is that the protein threading problem is NP-hard (i.e., it is unlikely to have a polynomial-time algorithm), if the pairwise interactions are treated rigorously. The key contribution of this dissertation is to show that there is actually a practically efficient algorithm for protein threading, even if the pairwise interactions are treated explicitly and rigorously. In this thesis, we propose a novel integer programming approach to solve the protein threading problem. The key element is a set of strong linear constraints to formulate the problem. In addition, we employ polyhedral combinatorics to analyze our formulation, and confirm that our formulation is well-described for the protein threading problem. Large scale experimental tests demonstrate that the optimal linear solutions of almost all the linear programs that formulate real threading instances solve to integrality, indicating that the protein threading problem is tractable in practice (i.e., it can be solved within polynomial time). We have implemented the proposed algorithm combined with several other components as a protein structure prediction computer program RAPTOR (RApid Protein Threading predictOR). CAFASP3 (The Third Critical Assessment of Fully Automated Structure Prediction) evaluation, the latest worldwide protein structure prediction competition, ranks RAPTOR first among all the non-meta structure prediction programs. The latest LiveBench evaluation also shows that the performance of RAPTOR is superior compared to other structure prediction tools. These indicate that the integer programming approach is promising in further improving the prediction rate of the protein threading approach.

We consider the parameterized complexity of a generalized version of the game Rush Hour 1 , which is a puzzle requiring the player to find a sequence of moves by vehicles to enable a special target vehicle to escape from a grid-shaped game board that may contain obstacles. Although the problem is PSPACE-complete, we demonstrate algorithms that work in polynomial time when either the total number of vehicles or the total number of moves is bounded by a constant. Our contributions are two-fold, entailing the application of ideas of parameterized complexity to games and to motion-planning problems (albeit motion-planning problems of a very constrained nature).