Breadth-first search and the Andrews-Curtis conjecture

Andrews and Curtis conjectured in 1965 that every balanced presentation of the trivial group can be transformed into a standard presentation by a finite sequence of elementary transformations. Recent computational work by Miasnikov and Myasnikov on this problem has been based on genetic algorithms. We show that a computational attack based on a breadth-first search of the tree of equivalent presentations is also viable, and seems to outperform that based on genetic algorithms. It allows us to extract shorter proofs (in some cases, provably shortest) and to consider the length thirteen case for two generators. We prove that, up to equivalence, there is a unique minimum potential counterexample.

The Fa,b,c conjecture, I

In 1977 a five-part conjecture was made about a family of groups related to trivalent graphs and one part of the conjecture was proved. The conjecture completely determines all finite members of the family. Here we prove another part of the conjecture and foreshadow a paper which completes the proof of the other three parts.

The Fa,b,c conjecture is true, II

In 1977 a five-part conjecture was made about a family of groups related to trivalent graphs and subsequently two parts of the conjecture were proved. The conjecture completely determines all finite members of the family. Here we complete the proof of the conjecture by giving proofs for the remaining three parts. (c) 2006 Elsevier Inc. All rights reserved.

Irreducible cyclic presentations of the trivial group

We produce families of irreducible cyclic presentations of the trivial group. These families comprehensively answer questions about such presentations asked by Dunwoody and by Edjvet, Hammond, and Thomas. Our theorems are purely theoretical, but their derivation is based on practical computations. We explain how we chose the computations and how we deduced the theorems.

Testing integrability with a single bit of quantum information

We show that deterministic quantum computing with a single bit can determine whether the classical limit of a quantum system is chaotic or integrable using O(N) physical resources, where N is the dimension of the Hilbert space of the system under study. This is a square-root improvement over all known classical procedures. Our study relies strictly on the random matrix conjecture. We also present numerical results for the nonlinear kicked top.

Decompositions of complete graphs into triangles and Hamilton cycles

For all odd integers n greater than or equal to 1, let G(n) denote the complete graph of order n, and for all even integers n greater than or equal to 2 let G,, denote the complete graph of order n with the edges of a 1-factor removed. It is shown that for all non-negative integers h and t and all positive integers n, G, can be decomposed into h Hamilton cycles and t triangles if and only if nh + 3t is the number of edges in G(n). (C) 2004 Wiley Periodicals, Inc.

A note on execution costs for stock index futures: Information versus liquidity effects

This paper examines execution costs and the impact of trade size for stock index futures using price-volume transaction data from the London International Financial Futures and Options Exchange. Consistent with Subrahmanyam [Rev. Financ. Stud. 4 (1991) 11] we find that effective half spreads in the stock index futures market are small compared to stock markets, and that trades in stock index futures have only a small permanent price impact. This result is important as it helps to better understand the success of equity index products such as index futures and Exchange Traded Funds. We also find that there is no asymmetry in the post-trade price reaction between purchases and sales for stock index futures across various trade sizes. This result is consistent with the conjecture in Chan and Lakonishok [J. Financ. Econ. 33 (1993) 173] that the asymmetry surrounding block trades in stock markets is due to the high cost of short selling and the general reluctance of traders to short sell on stock markets. (C) 2004 Elsevier B.V. All rights reserved.

Quantum entanglement and fixed-point bifurcations

How does the classical phase-space structure for a composite system relate to the entanglement characteristics of the corresponding quantum system? We demonstrate how the entanglement in nonlinear bipartite systems can be associated with a fixed-point bifurcation in the classical dynamics. Using the example of coupled giant spins we show that when a fixed point undergoes a supercritical pitchfork bifurcation, the corresponding quantum state-the ground state-achieves its maximum amount of entanglement near the critical point. We conjecture that this will be a generic feature of systems whose classical limit exhibits such a bifurcation.

Decomposition of complete graphs into 5-cubes

Necessary conditions for the complete graph on n vertices to have a decomposition into 5-cubes are that 5 divides it - 1 and 80 divides it (it - 1)/2. These are known to be sufficient when n is odd. We prove them also sufficient for it even, thus completing the spectrum problem for the 5-cube and lending further weight to a long-standing conjecture of Kotzig. (c) 2005 Wiley Periodicals, Inc.

Do different surrogate methods detect lateral genetic transfer events of different relative ages?

Non-tree-based ('surrogate') methods have been used to identify instances of lateral genetic transfer in microbial genomes but agreement among predictions of different methods can be poor. It has been proposed that this disagreement arises because different surrogate methods are biased towards the detection of certain types of transfer events. This conjecture is supported by a rigorous phylogenetic analysis of 3776 proteins in Escherichia coli K12 MG1655 to map the ages of transfer events relative to one another.

Flexible proof reuse for software verification

Proof reuse, or analogical reasoning, involves reusing the proof of a source theorem in the proof of a target conjecture. We have developed a method for proof reuse that is based on the generalisation replay paradigm described in the literature, in which a generalisation of the source proof is replayed to construct the target proof. In this paper, we describe the novel aspects of our method, which include a technique for producing more accurate source proof generalisations (using knowledge of the target goal), as well as a flexible replay strategy that allows the user to set various parameters to control the size and the shape of the search space. Finally, we report on the results of applying this method to a case study from the realm of software verification.

Estimating buffer overflows in three stages using cross-entropy

In this paper we propose a fast adaptive Importance Sampling method for the efficient simulation of buffer overflow probabilities in queueing networks. The method comprises three stages. First we estimate the minimum Cross-Entropy tilting parameter for a small buffer level; next, we use this as a starting value for the estimation of the optimal tilting parameter for the actual (large) buffer level; finally, the tilting parameter just found is used to estimate the overflow probability of interest. We recognize three distinct properties of the method which together explain why the method works well; we conjecture that they hold for quite general queueing networks. Numerical results support this conjecture and demonstrate the high efficiency of the proposed algorithm.