Showing 1–19 of 19 results for author: McCallum, S

GPTNT: Benchmarking Real-Time Collaboration Between Multimodal Agents on Keep Talking And Nobody Explodes

Authors: Amit Parekh, Sabrina McCallum, Kareem Al-Hasan, Malvina Nikandrou, Alessandro Suglia, Ioannis Konstas

Abstract: Multimodal models are increasingly deployed to solve tasks collaboratively with humans or other artificial agents. Existing benchmarks show that these models possess many of the required component capabilities, but the conditions that coincide in collaboration, including time pressure, information asymmetry, and imperfect communication, are usually studied in isolation. We introduce GPTNT, a bench… ▽ More Multimodal models are increasingly deployed to solve tasks collaboratively with humans or other artificial agents. Existing benchmarks show that these models possess many of the required component capabilities, but the conditions that coincide in collaboration, including time pressure, information asymmetry, and imperfect communication, are usually studied in isolation. We introduce GPTNT, a benchmark built on the cooperative video game Keep Talking and Nobody Explodes, in which two agents must coordinate to defuse procedurally generated bomb puzzles against a live countdown. One agent can see and manipulate the bomb but does not have the defusal instructions; the other has the instructions but cannot see or manipulate the bomb. Neither agent can succeed alone: success requires effective and efficient communication. Unlike turn-based proxies, GPTNT requires agents to act asynchronously and communicate in real time. GPTNT is designed to separate collaboration from reliance on memorized solutions: the instruction manual, the partner, or both can be withheld to isolate what a model derives in the moment from what it already knows. We show that GPTNT poses a substantial challenge for state-of-the-art systems: none of the closed- or open-source models we test defuses a single bomb in real time, a bar that human players clear. Through controlled experiments, we identify critical weaknesses in state tracking, efficient action under time pressure, ambiguity handling, and error recovery. We release GPTNT as a benchmark for collaborative performance that current evaluations leave unmeasured. Because it runs on the real game, GPTNT benefits from procedural generation and inherits a living modding community, allowing the benchmark to evolve as models improve rather than being solved once and retired. △ Less

Submitted 26 June, 2026; originally announced June 2026.

Comments: Project website and code at https://gptnt.github.io

Strong Stochastic Flow Maps

Authors: Sam McCallum, Zander W. Blasingame, Timothy Herschell, Niklas Rindtorff, Alexander Tong, James Foster

Abstract: Flow and diffusion models generate high-quality samples in many modalities; however, many network evaluations are required during inference due to numerical integration of an underlying differential equation. Flow maps alleviate this problem by learning the solution map of the differential equation directly, enabling few-step sampling. Yet, current methods are restricted to approximating the solut… ▽ More Flow and diffusion models generate high-quality samples in many modalities; however, many network evaluations are required during inference due to numerical integration of an underlying differential equation. Flow maps alleviate this problem by learning the solution map of the differential equation directly, enabling few-step sampling. Yet, current methods are restricted to approximating the solution map of ODEs. These methods can be used to learn the transition kernel of an SDE, thereby obtaining a solution map that recovers the marginal distributions of the process (weak convergence) rather than the solution path (strong convergence). We propose Strong Stochastic Flow Maps (SSFMs) as a novel framework for learning the strong solution map of additive-noise SDEs, directly generalizing deterministic flow maps to the stochastic setting. Further, a polynomial approximation to Brownian motion is introduced and shown to converge pathwise. These results enable a simulation-free training objective for the solution map of diffusion models. We demonstrate that SSFMs outperform previous stochastic flow map methods on image generation and enable few-step sampling of molecular systems. △ Less

Submitted 31 May, 2026; originally announced June 2026.

Comments: Preprint

Enhanced CAD-Based Quantifier Elimination With Multiple Equational Constraints

Authors: James H. Davenport, Matthew England, Scott McCallum

Abstract: This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present in the given input formula $φ^*$. The first enhancement provides more detail in the output when there is a conceptual partition of the set of variables of $φ^*$ into parameters and unknowns. In such cases, we describe how… ▽ More This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present in the given input formula $φ^*$. The first enhancement provides more detail in the output when there is a conceptual partition of the set of variables of $φ^*$ into parameters and unknowns. In such cases, we describe how to partition the parameter space so that: (1) in each open set of the partition the number $ν$ of associated unknowns is a finite constant or is infinite; and (2) for each such open set for which $ν$ is finite, an expression for the unknowns in terms of the parameters is provided. The second enhancement is an efficiency gain achievable in certain situations. Indeed, when certain conditions are met, the second CAD equational projection step can be reduced more significantly than is supported by the prior existing theory. Relevant theorems and worked examples for both enhancements are provided. Application areas include approximation theory, cuspidal manipulator classification, and biological/chemical systems. △ Less

Submitted 5 June, 2026; v1 submitted 26 April, 2026; originally announced April 2026.

Comments: Preliminary Draft; updated to reference related prior work

MSC Class: 68W30; 03C10 ACM Class: I.1.2

FOSSIL: Harnessing Feedback on Suboptimal Samples for Data-Efficient Generalisation with Imitation Learning for Embodied Vision-and-Language Tasks

Authors: Sabrina McCallum, Amit Parekh, Alessandro Suglia

Abstract: Current approaches to embodied AI tend to learn policies from expert demonstrations. However, without a mechanism to evaluate the quality of demonstrated actions, they are limited to learning from optimal behaviour, or they risk replicating errors and inefficiencies. While reinforcement learning offers one alternative, the associated exploration typically results in sacrificing data efficiency. Th… ▽ More Current approaches to embodied AI tend to learn policies from expert demonstrations. However, without a mechanism to evaluate the quality of demonstrated actions, they are limited to learning from optimal behaviour, or they risk replicating errors and inefficiencies. While reinforcement learning offers one alternative, the associated exploration typically results in sacrificing data efficiency. This work explores how agents trained with imitation learning can learn robust representations from both optimal and suboptimal demonstrations when given access to constructive language feedback as a means to contextualise different modes of behaviour. We directly provide language feedback embeddings as part of the input sequence into a Transformer-based policy, and optionally complement the traditional next action prediction objective with auxiliary self-supervised learning objectives for feedback prediction. We test our approach on a range of embodied Vision-and-Language tasks in our custom BabyAI-XGen environment and show significant improvements in agents' compositional generalisation abilities and robustness, suggesting that our data-efficient method allows models to successfully convert suboptimal behaviour into learning opportunities. Overall, our results suggest that language feedback is a competitive and intuitive alternative to intermediate scalar rewards for language-specified embodied tasks. △ Less

Submitted 13 October, 2025; originally announced October 2025.

Comments: EMNLP 2025 Findings

Linear Regression in p-adic metric spaces

Authors: Gregory D. Baker, Scott McCallum, Dirk Pattinson

Abstract: Many real-world machine learning problems involve inherently hierarchical data, yet traditional approaches rely on Euclidean metrics that fail to capture the discrete, branching nature of hierarchical relationships. We present a theoretical foundation for machine learning in p-adic metric spaces, which naturally respect hierarchical structure. Our main result proves that an n-dimensional plane min… ▽ More Many real-world machine learning problems involve inherently hierarchical data, yet traditional approaches rely on Euclidean metrics that fail to capture the discrete, branching nature of hierarchical relationships. We present a theoretical foundation for machine learning in p-adic metric spaces, which naturally respect hierarchical structure. Our main result proves that an n-dimensional plane minimizing the p-adic sum of distances to points in a dataset must pass through at least n + 1 of those points -- a striking contrast to Euclidean regression that highlights how p-adic metrics better align with the discrete nature of hierarchical data. As a corollary, a polynomial of degree n constructed to minimise the p-adic sum of residuals will pass through at least n + 1 points. As a further corollary, a polynomial of degree n approximating a higher degree polynomial at a finite number of points will yield a difference polynomial that has distinct rational roots. We demonstrate the practical significance of this result through two applications in natural language processing: analyzing hierarchical taxonomies and modeling grammatical morphology. These results suggest that p-adic metrics may be fundamental to properly handling hierarchical data structures in machine learning. In hierarchical data, interpolation between points often makes less sense than selecting actual observed points as representatives. △ Less

Submitted 27 September, 2025; originally announced October 2025.

MSC Class: 11D88; 62J99; 68T50 ACM Class: G.3; I.2.6; I.2.7; I.5.1; I.5.4

Journal ref: p-Adic Numbers, Ultrametric Analysis and Applications, volume 17(4), 2025

Reversible Deep Equilibrium Models

Authors: Sam McCallum, Kamran Arora, James Foster

Abstract: Deep Equilibrium Models (DEQs) are an interesting class of implicit model where the model output is implicitly defined as the fixed point of a learned function. These models have been shown to outperform explicit (fixed-depth) models in large-scale tasks by trading many deep layers for a single layer that is iterated many times. However, gradient calculation through DEQs is approximate. This often… ▽ More Deep Equilibrium Models (DEQs) are an interesting class of implicit model where the model output is implicitly defined as the fixed point of a learned function. These models have been shown to outperform explicit (fixed-depth) models in large-scale tasks by trading many deep layers for a single layer that is iterated many times. However, gradient calculation through DEQs is approximate. This often leads to unstable training dynamics and requires regularisation or many function evaluations to fix. Here, we introduce Reversible Deep Equilibrium Models (RevDEQs) that allow for exact gradient calculation, no regularisation and far fewer function evaluations than DEQs. We show that RevDEQs significantly improve performance on language modelling and image classification tasks against comparable implicit and explicit models. △ Less

Submitted 3 December, 2025; v1 submitted 16 September, 2025; originally announced September 2025.

Efficient, Accurate and Stable Gradients for Neural ODEs

Authors: Sam McCallum, James Foster

Abstract: Training Neural ODEs requires backpropagating through an ODE solve. The state-of-the-art backpropagation method is recursive checkpointing that balances recomputation with memory cost. Here, we introduce a class of algebraically reversible ODE solvers that significantly improve upon both the time and memory cost of recursive checkpointing. The reversible solvers presented calculate exact gradients… ▽ More Training Neural ODEs requires backpropagating through an ODE solve. The state-of-the-art backpropagation method is recursive checkpointing that balances recomputation with memory cost. Here, we introduce a class of algebraically reversible ODE solvers that significantly improve upon both the time and memory cost of recursive checkpointing. The reversible solvers presented calculate exact gradients, are high-order and numerically stable -- strictly improving on previous reversible architectures. △ Less

Submitted 29 January, 2025; v1 submitted 15 October, 2024; originally announced October 2024.

Comments: Preprint

Iterated Resultants and Rational Functions in Real Quantifier Elimination

Authors: James H. Davenport, Matthew England, Scott McCallum, Ali K. Uncu

Abstract: This paper builds and extends on the authors' previous work related to the algorithmic tool, Cylindrical Algebraic Decomposition (CAD), and one of its core applications, Real Quantifier Elimination (QE). These topics are at the heart of symbolic computation and were first implemented in computer algebra systems decades ago, but have recently received renewed interest as part of the ongoing develop… ▽ More This paper builds and extends on the authors' previous work related to the algorithmic tool, Cylindrical Algebraic Decomposition (CAD), and one of its core applications, Real Quantifier Elimination (QE). These topics are at the heart of symbolic computation and were first implemented in computer algebra systems decades ago, but have recently received renewed interest as part of the ongoing development of SMT solvers for non-linear real arithmetic. First, we consider the use of iterated univariate resultants in traditional CAD, and how this leads to inefficiencies, especially in the case of an input with multiple equational constraints. We reproduce the workshop paper [Davenport and England, 2023], adding important clarifications to our suggestions first made there to make use of multivariate resultants in the projection phase of CAD. We then consider an alternative approach to this problem first documented in [McCallum and Brown, 2009] which redefines the actual object under construction, albeit only in the case of two equational constraints. We correct an unhelpful typo and provide a proof missing from that paper. We finish by revising the topic of how to deal with SMT or Real QE problems expressed using rational functions (as opposed to the usual polynomial ones) noting that these are often found in industrial applications. We revisit a proposal made in [Uncu, Davenport and England, 2023] for doing this in the case of satisfiability, explaining why such an approach does not trivially extend to more complicated quantification structure and giving a suitable alternative. △ Less

Submitted 26 December, 2024; v1 submitted 23 December, 2023; originally announced December 2023.

Comments: Submitted to Mathematics in Computer Science

MSC Class: 14W30 (primary) 68W30 (secondary) ACM Class: I.1.2

Journal ref: Mathematics in Computer Science, volume 19, article number 12, Springer, 2025

Is Feedback All You Need? Leveraging Natural Language Feedback in Goal-Conditioned Reinforcement Learning

Authors: Sabrina McCallum, Max Taylor-Davies, Stefano V. Albrecht, Alessandro Suglia

Abstract: Despite numerous successes, the field of reinforcement learning (RL) remains far from matching the impressive generalisation power of human behaviour learning. One possible way to help bridge this gap be to provide RL agents with richer, more human-like feedback expressed in natural language. To investigate this idea, we first extend BabyAI to automatically generate language feedback from the envi… ▽ More Despite numerous successes, the field of reinforcement learning (RL) remains far from matching the impressive generalisation power of human behaviour learning. One possible way to help bridge this gap be to provide RL agents with richer, more human-like feedback expressed in natural language. To investigate this idea, we first extend BabyAI to automatically generate language feedback from the environment dynamics and goal condition success. Then, we modify the Decision Transformer architecture to take advantage of this additional signal. We find that training with language feedback either in place of or in addition to the return-to-go or goal descriptions improves agents' generalisation performance, and that agents can benefit from feedback even when this is only available during training, but not at inference. △ Less

Submitted 7 December, 2023; originally announced December 2023.

Comments: Accepted at Workshop on Goal-conditioned Reinforcement Learning, NeurIPS 2023

Bayesian parameter estimation for characterising mobile ion vacancies in perovskite solar cells

Authors: Samuel G. McCallum, Oliver Nicholls, Kjeld O. Jensen, Matthew V. Cowley, James E. Lerpinière, Alison B. Walker

Abstract: To overcome the challenges associated with poor temporal stability of perovskite solar cells, methods are required that allow for fast iteration of fabrication and characterisation, such that optimal device performance and stability may be actively pursued. Currently, establishing the causes of underperformance is both complex and time-consuming, and optimisation of device fabrication thus inheren… ▽ More To overcome the challenges associated with poor temporal stability of perovskite solar cells, methods are required that allow for fast iteration of fabrication and characterisation, such that optimal device performance and stability may be actively pursued. Currently, establishing the causes of underperformance is both complex and time-consuming, and optimisation of device fabrication thus inherently slow. Here, we present a means of computational device characterisation of mobile halide ion parameters from room temperature current-voltage (J-V) measurements only, requiring $\sim 2$ hours of computation on basic computing resources. With our approach, the physical parameters of the device may be reverse modelled from experimental J-V measurements. In a drift-diffusion model, the set of coupled drift-diffusion partial differential equations cannot be inverted explicitly, so a method for inverting the drift-diffusion simulation is required. We show how Bayesian Parameter Estimation (BPE) coupled with a drift-diffusion perovskite solar cell model can determine the extent to which device parameters affect performance measured by J-V characteristics. Our method is demonstrated by investigating the extent to which device performance is influenced by mobile halide ions for a specific fabricated device. The ion vacancy density $N_0$ and diffusion coefficient $D_I$ were found to be precisely characterised for both simulated and fabricated devices. This result opens up the possibility of pinpointing origins of degradation by finding which parameters most influence device J-V curves as the cell degrades. △ Less

Submitted 25 September, 2023; originally announced September 2023.

Bayesian optimisation approach to quantify the effect of input parameter uncertainty on predictions of numerical physics simulations

Authors: Samuel G. McCallum, James E. Lerpiniére, Kjeld O. Jensen, Alison B. Walker

Abstract: An understanding of how input parameter uncertainty in the numerical simulation of physical models leads to simulation output uncertainty is a challenging task. Common methods for quantifying output uncertainty, such as performing a grid or random search over the model input space, are computationally intractable for a large number of input parameters, represented by a high-dimensional input space… ▽ More An understanding of how input parameter uncertainty in the numerical simulation of physical models leads to simulation output uncertainty is a challenging task. Common methods for quantifying output uncertainty, such as performing a grid or random search over the model input space, are computationally intractable for a large number of input parameters, represented by a high-dimensional input space. It is therefore generally unclear as to whether a numerical simulation can reproduce a particular outcome (e.g. a set of experimental results) with a plausible set of model input parameters. Here, we present a method for efficiently searching the input space using Bayesian Optimisation to minimise the difference between the simulation output and a set of experimental results. Our method allows explicit evaluation of the probability that the simulation can reproduce the measured experimental results in the region of input space defined by the uncertainty in each input parameter. We apply this method to the simulation of charge-carrier dynamics in the perovskite semiconductor methyl-ammonium lead iodide MAPbI$_3$ that has attracted attention as a light harvesting material in solar cells. From our analysis we conclude that the formation of large polarons, quasiparticles created by the coupling of excess electrons or holes with ionic vibrations, cannot explain the experimentally observed temperature dependence of electron mobility. △ Less

Submitted 21 September, 2023; originally announced September 2023.

Assessment of the reliability of Deconvolution Procedures for RCF Spectroscopy of Laser-Driven Ion Beams

Authors: S. McCallum, G. Milluzzo, M. Borghesi, A. Subiel, F. Romano

Abstract: Laser-driven ion beams are defined by a number of unique features, including a large spread in energy. A stack configuration of radiochromic film (RCF) can be utilized to characterize such beams through measurements of their energy spectra. A spectroscopic procedure is reported that allows the proton energy density within each active layer of a radiochromic film (RCF) stack to be retrieved. This i… ▽ More Laser-driven ion beams are defined by a number of unique features, including a large spread in energy. A stack configuration of radiochromic film (RCF) can be utilized to characterize such beams through measurements of their energy spectra. A spectroscopic procedure is reported that allows the proton energy density within each active layer of a radiochromic film (RCF) stack to be retrieved. This is based upon on a deconvolution algorithm developed through Geant4 Monte Carlo simulations to correct the contributions of energy depositions within a given film layer. Through Monte Carlo calculations, the spectrum retrieved from a simulated film stack can be retrieved and compared with a known energy spectrum, providing an examination of the efficacy of this tool. Application of the developed deconvolution procedure thus offers the potential to correctly reconstruct the incident energy spectrum of a laser-driven proton and ion beam from a stack of irradiated RCF. △ Less

Submitted 20 January, 2023; originally announced January 2023.

Comments: 6 pages, 3 figures, submission as a proceeding to ECPD 2021

Journal ref: Journal of Instrumentation, Volume 17, February 2022

Singularities and Catastrophes in Economics: Historical Perspectives and Future Directions

Authors: Michael S. Harré, Adam Harris, Scott McCallum

Abstract: Economic theory is a mathematically rich field in which there are opportunities for the formal analysis of singularities and catastrophes. This article looks at the historical context of singularities through the work of two eminent Frenchmen around the late 1960s and 1970s. René Thom (1923-2002) was an acclaimed mathematician having received the Fields Medal in 1958, whereas Gérard Debreu (1921-2… ▽ More Economic theory is a mathematically rich field in which there are opportunities for the formal analysis of singularities and catastrophes. This article looks at the historical context of singularities through the work of two eminent Frenchmen around the late 1960s and 1970s. René Thom (1923-2002) was an acclaimed mathematician having received the Fields Medal in 1958, whereas Gérard Debreu (1921-2004) would receive the Nobel Prize in economics in 1983. Both were highly influential within their fields and given the fundamental nature of their work, the potential for cross-fertilisation would seem to be quite promising. This was not to be the case: Debreu knew of Thom's work and cited it in the analysis of his own work, but despite this and other applied mathematicians taking catastrophe theory to economics, the theory never achieved a lasting following and relatively few results were published. This article reviews Debreu's analysis of the so called ${\it regular}$ and ${\it crtitical}$ economies in order to draw some insights into the economic perspective of singularities before moving to how singularities arise naturally in the Nash equilibria of game theory. Finally a modern treatment of stochastic game theory is covered through recent work on the quantal response equilibrium. In this view the Nash equilibrium is to the quantal response equilibrium what deterministic catastrophe theory is to stochastic catastrophe theory, with some caveats regarding when this analogy breaks down discussed at the end. △ Less

Submitted 12 July, 2019; originally announced July 2019.

Comments: 23 pages, 5 figures

MSC Class: 91A15; 91A80; 91A05; 91B50; 91B06

Validity proof of Lazard's method for CAD construction

Authors: Scott McCallum, Adam Parusinski, Laurentiu Paunescu

Abstract: In 1994 Lazard proposed an improved method for cylindrical algebraic decomposition (CAD). The method comprised a simplified projection operation together with a generalized cell lifting (that is, stack construction) technique. For the proof of the method's validity Lazard introduced a new notion of valuation of a multivariate polynomial at a point. However a gap in one of the key supporting result… ▽ More In 1994 Lazard proposed an improved method for cylindrical algebraic decomposition (CAD). The method comprised a simplified projection operation together with a generalized cell lifting (that is, stack construction) technique. For the proof of the method's validity Lazard introduced a new notion of valuation of a multivariate polynomial at a point. However a gap in one of the key supporting results for his proof was subsequently noticed. In the present paper we provide a complete validity proof of Lazard's method. Our proof is based on the classical parametrized version of Puiseux's theorem and basic properties of Lazard's valuation. This result is significant because Lazard's method can be applied to any finite family of polynomials, without any assumption on the system of coordinates. It therefore has wider applicability and may be more efficient than other projection and lifting schemes for CAD. △ Less

Submitted 26 July, 2017; v1 submitted 1 July, 2016; originally announced July 2016.

Comments: 21 pages

MSC Class: 14P10; 68W30 ACM Class: I.1.2

On Lazard's Valuation and CAD Construction

Authors: Scott McCallum, Hoon Hong

Abstract: In 1990 Lazard proposed an improved projection operation for cylindrical algebraic decomposition (CAD). For the proof he introduced a certain notion of valuation of a multivariate Puiseux series at a point. However a gap in one of the key supporting results for the improved projection was subsequently noticed. In this report we study a more limited but rigorous concept of Lazard's valuation: namel… ▽ More In 1990 Lazard proposed an improved projection operation for cylindrical algebraic decomposition (CAD). For the proof he introduced a certain notion of valuation of a multivariate Puiseux series at a point. However a gap in one of the key supporting results for the improved projection was subsequently noticed. In this report we study a more limited but rigorous concept of Lazard's valuation: namely, we study Lazard's valuation of a multivariate polynomial at a point. We prove some basic properties of the limited Lazard valuation and identify some relationships between valuation-invariance and order-invariance. △ Less

Submitted 9 February, 2015; v1 submitted 26 January, 2015; originally announced January 2015.

MSC Class: 14P10 ACM Class: I.1.2

A Pilot Study on Coupling CT and MRI through Use of Semiconductor Nanoparticles

Authors: Matthew Getzin, Lars Gjesteby, Yen-Jun Chuang, Scott McCallum, Wenxiang Cong, Chao Wang, Zhengwei Pan, Guohao Dai, Ge Wang

Abstract: CT and MRI are the two most widely used imaging modalities in healthcare, each with its own merits and drawbacks. Combining these techniques in one machine could provide unprecedented resolution and sensitivity in a single scan, and serve as an ideal platform to explore physical coupling of x-ray excitation and magnetic resonance. Molecular probes such as functionalized nanophosphors present an op… ▽ More CT and MRI are the two most widely used imaging modalities in healthcare, each with its own merits and drawbacks. Combining these techniques in one machine could provide unprecedented resolution and sensitivity in a single scan, and serve as an ideal platform to explore physical coupling of x-ray excitation and magnetic resonance. Molecular probes such as functionalized nanophosphors present an opportunity to demonstrate a synergy between these modalities. However, a simultaneous CT-MRI scanner does not exist at this moment. As a pilot study, here we propose a mechanism in which water solutions containing LiGa5O8:Cr3+ nanophosphors can be excited with x-rays to store energy, and these excited particles may subsequently influence the T2 relaxation times of the solutions so that a difference in T2 can be measured by MRI before and after x-ray excitation. The trends seen in our study suggest that a measurable effect may exist from x-ray excitation of the nanophosphors. However, there are several experimental conditions that hinder the clarity of the results to be statistically significant up to a commonly accepted level (p=0.05), including insoluble nanoparticles and inter-scan variability. Nevertheless, the initial results from our experiments seem a consistent and inspiring story that x-rays modify MRI T2 values around nanophosphors. Upon availability of soluble nanophosphors, we will repeat our experiments to confirm these observations. △ Less

Submitted 23 December, 2014; originally announced December 2014.

Comments: 24 total pages, 9 pages of text, 10 figures with captions (6 pages), supplemental material including analysis code and tutorial (9 pages)

Truth Table Invariant Cylindrical Algebraic Decomposition

Authors: Russell Bradford, James H. Davenport, Matthew England, Scott McCallum, David Wilson

Abstract: When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current author… ▽ More When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions. △ Less

Submitted 13 November, 2015; v1 submitted 3 January, 2014; originally announced January 2014.

Comments: 40 pages

MSC Class: 68W30; 03C10 ACM Class: I.1.2

Journal ref: Journal of Symbolic Computation 76, pp. 1-35, 2016

Cylindrical Algebraic Decompositions for Boolean Combinations

Authors: Russell Bradford, James H. Davenport, Matthew England, Scott McCallum, David Wilson

Abstract: This article makes the key observation that when using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is not always the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This motivates our definition of a Truth Table Invariant CAD (TTICAD). We generalise… ▽ More This article makes the key observation that when using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is not always the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This motivates our definition of a Truth Table Invariant CAD (TTICAD). We generalise the theory of equational constraints to design an algorithm which will efficiently construct a TTICAD for a wide class of problems, producing stronger results than when using equational constraints alone. The algorithm is implemented fully in Maple and we present promising results from experimentation. △ Less

Submitted 29 April, 2013; originally announced April 2013.

Comments: To appear in the proceedings of the 38th International Symposium on Symbolic and Algebraic Computation (ISSAC '13)

MSC Class: 68W30; 03C10 ACM Class: I.1.2

Journal ref: In: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, (ISSAC '13), pp 125-132, 2013

Quantifier elimination for approximate Beals-Kartashova factorization

Authors: Elena Kartashova, Scott McCallum

Abstract: The only known constructive factorization algorithm for linear partial differential operators (LPDOs) is Beals-Kartashova (BK) factorization \cite{bk2005}. One of the most interesting features of BK-factorization: at the beginning all the first-order factors are constructed and afterwards the factorization condition(s) should be checked. This leads to the important application area - namely, num… ▽ More The only known constructive factorization algorithm for linear partial differential operators (LPDOs) is Beals-Kartashova (BK) factorization \cite{bk2005}. One of the most interesting features of BK-factorization: at the beginning all the first-order factors are constructed and afterwards the factorization condition(s) should be checked. This leads to the important application area - namely, numerical simulations which could be simplified substantially if instead of computation with one LPDE of order $n$ we will be able to proceed computations with $n$ LPDEs all of order 1. In numerical simulations it is not necessary to fulfill factorization conditions exactly but with some given accuracy, which we call approximate factorization. The idea of the present paper is to look into the feasibility of solving problems of this kind using quantifier elinination by cylindrical algebraic decomposition. △ Less

Submitted 7 January, 2007; originally announced January 2007.

Journal ref: Lecture Notes in Computer Science (LNCS) 4573, pp. 106-115 ( 2007). Springer