Showing 1–22 of 22 results for author: Day, J

Operations & Supply Chain Management: Principles and Practice

Authors: Fotios Petropoulos, Henk Akkermans, O. Zeynep Aksin, Imran Ali, Mohamed Zied Babai, Ana Barbosa-Povoa, Olga Battaïa, Maria Besiou, Nils Boysen, Stephen Brammer, Alistair Brandon-Jones, Dirk Briskorn, Tyson R. Browning, Paul Buijs, Piera Centobelli, Andrea Chiarini, Paul Cousins, Elizabeth A. Cudney, Andrew Davies, Steven J. Day, René de Koster, Rommert Dekker, Juliano Denicol, Mélanie Despeisse, Stephen M. Disney , et al. (68 additional authors not shown)

Abstract: Operations and Supply Chain Management (OSCM) has continually evolved, incorporating a broad array of strategies, frameworks, and technologies to address complex challenges across industries. This encyclopedic article provides a comprehensive overview of contemporary strategies, tools, methods, principles, and best practices that define the field's cutting-edge advancements. It also explores the d… ▽ More Operations and Supply Chain Management (OSCM) has continually evolved, incorporating a broad array of strategies, frameworks, and technologies to address complex challenges across industries. This encyclopedic article provides a comprehensive overview of contemporary strategies, tools, methods, principles, and best practices that define the field's cutting-edge advancements. It also explores the diverse environments where OSCM principles have been effectively implemented. The article is meant to be read in a nonlinear fashion. It should be used as a point of reference or first-port-of-call for a diverse pool of readers: academics, researchers, students, and practitioners. △ Less

Submitted 22 June, 2025; v1 submitted 20 February, 2025; originally announced March 2025.

FC-Datalog as a Framework for Efficient String Querying

Authors: Owen M. Bell, Joel D. Day, Dominik D. Freydenberger

Abstract: Core spanners are a class of document spanners that capture the core functionality of IBM's AQL. FC is a logic on strings built around word equations that when extended with constraints for regular languages can be seen as a logic for core spanners. The recently introduced FC-Datalog extends FC with recursion, which allows us to define recursive relations for core spanners. Additionally, as FC-Dat… ▽ More Core spanners are a class of document spanners that capture the core functionality of IBM's AQL. FC is a logic on strings built around word equations that when extended with constraints for regular languages can be seen as a logic for core spanners. The recently introduced FC-Datalog extends FC with recursion, which allows us to define recursive relations for core spanners. Additionally, as FC-Datalog captures P, it is also a tractable version of Datalog on strings. This presents an opportunity for optimization. We propose a series of FC-Datalog fragments with desirable properties in terms of complexity of model checking, expressive power, and efficiency of checking membership in the fragment. This leads to a range of fragments that all capture LOGSPACE, which we further restrict to obtain linear combined complexity. This gives us a framework to tailor fragments for particular applications. To showcase this, we simulate deterministic regex in a tailored fragment of FC-Datalog. △ Less

Submitted 17 January, 2025; originally announced January 2025.

Learning 3D object-centric representation through prediction

Authors: John Day, Tushar Arora, Jirui Liu, Li Erran Li, Ming Bo Cai

Abstract: As part of human core knowledge, the representation of objects is the building block of mental representation that supports high-level concepts and symbolic reasoning. While humans develop the ability of perceiving objects situated in 3D environments without supervision, models that learn the same set of abilities with similar constraints faced by human infants are lacking. Towards this end, we de… ▽ More As part of human core knowledge, the representation of objects is the building block of mental representation that supports high-level concepts and symbolic reasoning. While humans develop the ability of perceiving objects situated in 3D environments without supervision, models that learn the same set of abilities with similar constraints faced by human infants are lacking. Towards this end, we developed a novel network architecture that simultaneously learns to 1) segment objects from discrete images, 2) infer their 3D locations, and 3) perceive depth, all while using only information directly available to the brain as training data, namely: sequences of images and self-motion. The core idea is treating objects as latent causes of visual input which the brain uses to make efficient predictions of future scenes. This results in object representations being learned as an essential byproduct of learning to predict. △ Less

Submitted 6 March, 2024; originally announced March 2024.

Comments: 21 pages, 11 figures. Project webpage can be found at https://jday54.github.io/opple_site/

ACM Class: I.2.10; I.4.8; I.4.6; I.4.10; I.2.6

Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

Authors: Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel Day, Florin Manea, Vijay Ganesh

Abstract: Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor solving strategies for their unique set of instances, thus dramatically enhancing solver performance for their use case. However, this approach of strategy customization presents a significant challenge: handcrafting an optimized strategy for a class of SMT instances remains a complex and demanding task fo… ▽ More Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor solving strategies for their unique set of instances, thus dramatically enhancing solver performance for their use case. However, this approach of strategy customization presents a significant challenge: handcrafting an optimized strategy for a class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address this problem of automatic SMT strategy synthesis via a novel Monte Carlo Tree Search (MCTS) based method. Our method treats strategy synthesis as a sequential decision-making process, whose search tree corresponds to the strategy space, and employs MCTS to navigate this vast search space. The key innovations that enable our method to identify effective strategies, while keeping costs low, are the ideas of layered and staged MCTS search. These novel heuristics allow for a deeper and more efficient exploration of the strategy space, enabling us to synthesize more effective strategies than the default ones in state-of-the-art (SOTA) SMT solvers. We implement our method, dubbed Z3alpha, as part of the Z3 SMT solver. Through extensive evaluations across six important SMT logics, Z3alpha demonstrates superior performance compared to the SOTA synthesis tool FastSMT, the default Z3 solver, and the CVC5 solver on most benchmarks. Remarkably, on a challenging QF_BV benchmark set, Z3alpha solves 42.7% more instances than the default strategy in the Z3 SMT solver. △ Less

Submitted 30 April, 2024; v1 submitted 30 January, 2024; originally announced January 2024.

Comments: Accepted at IJCAI 2024

Knowledge Engineering for Wind Energy

Authors: Yuriy Marykovskiy, Thomas Clark, Justin Day, Marcus Wiens, Charles Henderson, Julian Quick, Imad Abdallah, Anna Maria Sempreviva, Jean-Paul Calbimonte, Eleni Chatzi, Sarah Barber

Abstract: With the rapid evolution of the wind energy sector, there is an ever-increasing need to create value from the vast amounts of data made available both from within the domain, as well as from other sectors. This article addresses the challenges faced by wind energy domain experts in converting data into domain knowledge, connecting and integrating it with other sources of knowledge, and making it a… ▽ More With the rapid evolution of the wind energy sector, there is an ever-increasing need to create value from the vast amounts of data made available both from within the domain, as well as from other sectors. This article addresses the challenges faced by wind energy domain experts in converting data into domain knowledge, connecting and integrating it with other sources of knowledge, and making it available for use in next generation artificially intelligent systems. To this end, this article highlights the role that knowledge engineering can play in the process of digital transformation of the wind energy sector. It presents the main concepts underpinning Knowledge-Based Systems and summarises previous work in the areas of knowledge engineering and knowledge representation in a manner that is relevant and accessible to domain experts. A systematic analysis of the current state-of-the-art on knowledge engineering in the wind energy domain is performed, with available tools put into perspective by establishing the main domain actors and their needs and identifying key problematic areas. Finally, guidelines for further development and improvement are provided. △ Less

Submitted 1 October, 2023; originally announced October 2023.

Journal ref: Wind Energ. Sci. 9 (2024) 883-917

Denoising neural networks for magnetic resonance spectroscopy

Authors: Natalie Klein, Amber J. Day, Harris Mason, Michael W. Malone, Sinead A. Williamson

Abstract: In many scientific applications, measured time series are corrupted by noise or distortions. Traditional denoising techniques often fail to recover the signal of interest, particularly when the signal-to-noise ratio is low or when certain assumptions on the signal and noise are violated. In this work, we demonstrate that deep learning-based denoising methods can outperform traditional techniques w… ▽ More In many scientific applications, measured time series are corrupted by noise or distortions. Traditional denoising techniques often fail to recover the signal of interest, particularly when the signal-to-noise ratio is low or when certain assumptions on the signal and noise are violated. In this work, we demonstrate that deep learning-based denoising methods can outperform traditional techniques while exhibiting greater robustness to variation in noise and signal characteristics. Our motivating example is magnetic resonance spectroscopy, in which a primary goal is to detect the presence of short-duration, low-amplitude radio frequency signals that are often obscured by strong interference that can be difficult to separate from the signal using traditional methods. We explore various deep learning architecture choices to capture the inherently complex-valued nature of magnetic resonance signals. On both synthetic and experimental data, we show that our deep learning-based approaches can exceed performance of traditional techniques, providing a powerful new class of methods for analysis of scientific time series data. △ Less

Submitted 31 October, 2022; originally announced November 2022.

Comments: 5 pages with appendix

A Generic Information Extraction System for String Constraints

Authors: Joel D. Day, Adrian Kröger, Mitja Kulczynski, Florin Manea, Dirk Nowotka, Danny Bøgsted Poulsen

Abstract: String constraint solving, and the underlying theory of word equations, are highly interesting research topics both for practitioners and theoreticians working in the wide area of satisfiability modulo theories. As string constraint solving algorithms, a.k.a. string solvers, gained a more prominent role in the formal analysis of string-heavy programs, especially in connection to symbolic code exec… ▽ More String constraint solving, and the underlying theory of word equations, are highly interesting research topics both for practitioners and theoreticians working in the wide area of satisfiability modulo theories. As string constraint solving algorithms, a.k.a. string solvers, gained a more prominent role in the formal analysis of string-heavy programs, especially in connection to symbolic code execution and security protocol verification, we can witness an ever-growing number of benchmarks collecting string solving instances from real-world applications as well as an ever-growing need for more efficient and reliable solvers, especially for the aforementioned real-world instances. Thus, it seems that the string solving area (and the developers, theoreticians, and end-users active in it) could greatly benefit from a better understanding and processing of the existing string solving benchmarks. In this context, we propose SMTQUERY: an SMT-LIB benchmark analysis tool for string constraints. SMTQUERY is implemented in Python 3, and offers a collection of analysis and information extraction tools for a comprehensive data base of string benchmarks (presented in SMT-LIB format), based on an SQL-centred language called QLANG. △ Less

Submitted 18 August, 2022; originally announced August 2022.

Subsequences With Gap Constraints: Complexity Bounds for Matching and Analysis Problems

Authors: Joel D. Day, Maria Kosche, Florin Manea, Markus L. Schmid

Abstract: We consider subsequences with gap constraints, i.e., length-k subsequences p that can be embedded into a string w such that the induced gaps (i.e., the factors of w between the positions to which p is mapped to) satisfy given gap constraints $gc = (C_1, C_2, ..., C_{k-1})$; we call p a gc-subsequence of w. In the case where the gap constraints gc are defined by lower and upper length bounds… ▽ More We consider subsequences with gap constraints, i.e., length-k subsequences p that can be embedded into a string w such that the induced gaps (i.e., the factors of w between the positions to which p is mapped to) satisfy given gap constraints $gc = (C_1, C_2, ..., C_{k-1})$; we call p a gc-subsequence of w. In the case where the gap constraints gc are defined by lower and upper length bounds $C_i = (L^-_i, L^+_i) \in \mathbb{N}^2$ and/or regular languages $C_i \in REG$, we prove tight (conditional on the orthogonal vectors (OV) hypothesis) complexity bounds for checking whether a given p is a gc-subsequence of a string w. We also consider the whole set of all gc-subsequences of a string, and investigate the complexity of the universality, equivalence and containment problems for these sets of gc-subsequences. △ Less

Submitted 28 June, 2022; originally announced June 2022.

Formal Languages via Theories over Strings

Authors: Joel D. Day, Vijay Ganesh, Nathan Grewal, Florin Manea

Abstract: We investigate the properties of formal languages expressible in terms of formulas over quantifier-free theories of word equations, arithmetic over length constraints, and language membership predicates for the classes of regular, visibly pushdown, and deterministic context-free languages. In total, we consider 20 distinct theories and decidability questions for problems such as emptiness and univ… ▽ More We investigate the properties of formal languages expressible in terms of formulas over quantifier-free theories of word equations, arithmetic over length constraints, and language membership predicates for the classes of regular, visibly pushdown, and deterministic context-free languages. In total, we consider 20 distinct theories and decidability questions for problems such as emptiness and universality for formal languages over them. First, we discuss their relative expressive power and observe a rough division into two hierarchies based on whether or not word equations are present. Second, we consider the decidability status of several important decision problems, such as emptiness and universality. Note that the emptiness problem is equivalent to the satisfiability problem over the corresponding theory. Third, we consider the problem of whether a language in one theory is expressible in another and show several negative results in which this problem is undecidable. These results are particularly relevant in the context of normal forms in both practical and theoretical aspects of string solving. △ Less

Submitted 1 May, 2022; originally announced May 2022.

String Theories involving Regular Membership Predicates: From Practice to Theory and Back

Authors: Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, Dirk Nowotka

Abstract: Widespread use of string solvers in formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context, especially for real-world cases. Designing an algorithm for the (generally undecidable) satisfiability problem for systems of string constraints requires a thorough understanding of the structure of constraints pre… ▽ More Widespread use of string solvers in formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context, especially for real-world cases. Designing an algorithm for the (generally undecidable) satisfiability problem for systems of string constraints requires a thorough understanding of the structure of constraints present in the targeted cases. In this paper, we investigate benchmarks presented in the literature containing regular expression membership predicates, extract different first order logic theories, and prove their decidability, resp. undecidability. Notably, the most common theories in real-world benchmarks are PSPACE-complete and directly lead to the implementation of a more efficient algorithm to solving string constraints. △ Less

Submitted 15 May, 2021; originally announced May 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:2010.07253

An SMT Solver for Regular Expressions and Linear Arithmetic over String Length

Authors: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, Vijay Ganesh

Abstract: We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. A crucial insight that underpins our algorithm is that real-world instances contain a wealth of information about upper and lower bounds on len… ▽ More We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. A crucial insight that underpins our algorithm is that real-world instances contain a wealth of information about upper and lower bounds on lengths of strings under constraints, and such information can be used very effectively to simplify operations on automata representing regular expressions. Additionally, we present a number of novel general heuristics, such as the prefix/suffix method, that can be used in conjunction with a variety of regex solving algorithms, making them more efficient. We showcase the power of our algorithm and heuristics via an extensive empirical evaluation over a large and diverse benchmark of 57256 regex-heavy instances, almost 75% of which are derived from industrial applications or contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this benchmark, in particular achieving a 2.4x speedup over CVC4, 4.4x speedup over Z3seq, 6.4x speedup over Z3-Trau, 9.1x speedup over Z3str3, and 13x speedup over OSTRICH. △ Less

Submitted 7 May, 2021; v1 submitted 14 October, 2020; originally announced October 2020.

Comments: 25 pages (main body 21 pages). 7 figures, 6 tables

Advancing the Scientific Frontier with Increasingly Autonomous Systems

Authors: Rashied Amini, Abigail Azari, Shyam Bhaskaran, Patricia Beauchamp, Julie Castillo-Rogez, Rebecca Castano, Seung Chung, John Day, Richard Doyle, Martin Feather, Lorraine Fesq, Jeremy Frank, P. Michael Furlong, Michel Ingham, Brian Kennedy, Ksenia Kolcio, Issa Nesnas, Robert Rasmussen, Glenn Reeves, Cristina Sorice, Bethany Theiling, Jay Wyatt

Abstract: A close partnership between people and partially autonomous machines has enabled decades of space exploration. But to further expand our horizons, our systems must become more capable. Increasing the nature and degree of autonomy - allowing our systems to make and act on their own decisions as directed by mission teams - enables new science capabilities and enhances science return. The 2011 Planet… ▽ More A close partnership between people and partially autonomous machines has enabled decades of space exploration. But to further expand our horizons, our systems must become more capable. Increasing the nature and degree of autonomy - allowing our systems to make and act on their own decisions as directed by mission teams - enables new science capabilities and enhances science return. The 2011 Planetary Science Decadal Survey (PSDS) and on-going pre-Decadal mission studies have identified increased autonomy as a core technology required for future missions. However, even as scientific discovery has necessitated the development of autonomous systems and past flight demonstrations have been successful, institutional barriers have limited its maturation and infusion on existing planetary missions. Consequently, the authors and endorsers of this paper recommend that new programmatic pathways be developed to infuse autonomy, infrastructure for support autonomous systems be invested in, new practices be adopted, and the cost-saving value of autonomy for operations be studied. △ Less

Submitted 15 September, 2020; originally announced September 2020.

Comments: 10 pages (compared to 8 submitted to PSADS), 2 figures, submitted to National Academy of Sciences Planetary Science and Astrobiology Decadal Survey 2023-2032

Calculating Great Britains half-hourly electrical demand from publicly available data

Authors: IA Grant Wilson, Shivangi Sharma, Joseph Day, Noah Godfrey

Abstract: Here we present a method to combine half-hourly publicly available electrical generation and interconnector operational data for Great Britain to create a timeseries that approximates its electrical demand. We term the calculated electrical demand ESPENI that is an acronym for Elexon Sum Plus Embedded Net Imports. The method adds value to the original data by combining both transmission and distri… ▽ More Here we present a method to combine half-hourly publicly available electrical generation and interconnector operational data for Great Britain to create a timeseries that approximates its electrical demand. We term the calculated electrical demand ESPENI that is an acronym for Elexon Sum Plus Embedded Net Imports. The method adds value to the original data by combining both transmission and distribution generation data into a single dataset and adding ISO 8601 compatible datetimes to increase interoperability with other timeseries data. Data cleansing is undertaken by visually flagging data errors and then using simple linear interpolation to impute values to replace the flagged data. Publishing the method allows it to be further enhanced or adapted and to be considered and critiqued by a wider community. In addition, the published raw and cleaned data is a valuable resource that saves researchers considerable time in repeating the steps presented in the method to prepare the data for further analysis. The data is a public record of the decarbonisation of Great Britains electrical system since late 2008, widely seen as an example of rapid decarbonisation of an electrical system away from fossil fuel generation to lower carbon sources. △ Less

Submitted 15 September, 2021; v1 submitted 28 June, 2020; originally announced June 2020.

Comments: 33 pages, 3 Figures, 6 tables

On Solving Word Equations Using SAT

Authors: Joel D. Day, Thorsten Ehlers, Mitja Kulczynski, Florin Manea, Dirk Nowotka, Danny Bøgsted Poulsen

Abstract: We present Woorpje, a string solver for bounded word equations (i.e., equations where the length of each variable is upper bounded by a given integer). Our algorithm works by reformulating the satisfiability of bounded word equations as a reachability problem for nondeterministic finite automata, and then carefully encoding this as a propositional satisfiability problem, which we then solve using… ▽ More We present Woorpje, a string solver for bounded word equations (i.e., equations where the length of each variable is upper bounded by a given integer). Our algorithm works by reformulating the satisfiability of bounded word equations as a reachability problem for nondeterministic finite automata, and then carefully encoding this as a propositional satisfiability problem, which we then solve using the well-known Glucose SAT-solver. This approach has the advantage of allowing for the natural inclusion of additional linear length constraints. Our solver obtains reliable and competitive results and, remarkably, discovered several cases where state-of-the-art solvers exhibit a faulty behaviour. △ Less

Submitted 27 June, 2019; originally announced June 2019.

k-Spectra of weakly-c-Balanced Words

Authors: Joel D. Day, Pamela Fleischmann, Florin Manea, Dirk Nowotka

Abstract: A word $u$ is a scattered factor of $w$ if $u$ can be obtained from $w$ by deleting some of its letters. That is, there exist the (potentially empty) words $u_1,u_2,..., u_n$, and $v_0,v_1,..,v_n$ such that $u = u_1u_2...u_n$ and $w = v_0u_1v_1u_2v_2...u_nv_n$. We consider the set of length-$k$ scattered factors of a given word w, called here $k$-spectrum and denoted $\ScatFact_k(w)$. We prove a s… ▽ More A word $u$ is a scattered factor of $w$ if $u$ can be obtained from $w$ by deleting some of its letters. That is, there exist the (potentially empty) words $u_1,u_2,..., u_n$, and $v_0,v_1,..,v_n$ such that $u = u_1u_2...u_n$ and $w = v_0u_1v_1u_2v_2...u_nv_n$. We consider the set of length-$k$ scattered factors of a given word w, called here $k$-spectrum and denoted $\ScatFact_k(w)$. We prove a series of properties of the sets $\ScatFact_k(w)$ for binary strictly balanced and, respectively, $c$-balanced words $w$, i.e., words over a two-letter alphabet where the number of occurrences of each letter is the same, or, respectively, one letter has $c$-more occurrences than the other. In particular, we consider the question which cardinalities $n= |\ScatFact_k(w)|$ are obtainable, for a positive integer $k$, when $w$ is either a strictly balanced binary word of length $2k$, or a $c$-balanced binary word of length $2k-c$. We also consider the problem of reconstructing words from their $k$-spectra. △ Less

Submitted 24 May, 2019; v1 submitted 19 April, 2019; originally announced April 2019.

Graph and String Parameters: Connections Between Pathwidth, Cutwidth and the Locality Number

Authors: Katrin Casel, Joel D. Day, Pamela Fleischmann, Tomasz Kociumaka, Florin Manea, Markus L. Schmid

Abstract: We investigate the locality number, a recently introduced structural parameter for strings (with applications in pattern matching with variables), and its connection to two important graph-parameters, cutwidth and pathwidth. These connections allow us to show that computing the locality number is NP-hard, but fixed-parameter tractable, if parameterised by the locality number or by the alphabet siz… ▽ More We investigate the locality number, a recently introduced structural parameter for strings (with applications in pattern matching with variables), and its connection to two important graph-parameters, cutwidth and pathwidth. These connections allow us to show that computing the locality number is NP-hard, but fixed-parameter tractable, if parameterised by the locality number or by the alphabet size, which has been formulated as open problems in the literature. Moreover, the locality number can be approximated with ratio O(sqrt(log(opt)) log(n)). An important aspect of our work -- that is relevant in its own right and of independent interest -- is that we identify connections between the string parameter of the locality number on the one hand, and the famous graph parameters of cutwidth and pathwidth, on the other hand. These two parameters have been jointly investigated in the literature and are arguably among the most central graph parameters that are based on "linearisations" of graphs. In this way, we also identify a direct approximation preserving reduction from cutwidth to pathwidth, which shows that any polynomial f(opt,|V|)-approximation algorithm for pathwidth yields a polynomial 2f(2 opt,h)-approximation algorithm for cutwidth on multigraphs (where h is the number of edges). In particular, this translates known approximation ratios for pathwidth into new approximation ratios for cutwidth, namely O(sqrt(log(opt)) log(h)) and O(sqrt(log(opt)) opt) for (multi) graphs with h edges. △ Less

Submitted 25 April, 2024; v1 submitted 28 February, 2019; originally announced February 2019.

PaPaS: A Portable, Lightweight, and Generic Framework for Parallel Parameter Studies

Authors: Eduardo Ponce, Brittany Stephenson, Suzanne Lenhart, Judy Day, Gregory D. Peterson

Abstract: The current landscape of scientific research is widely based on modeling and simulation, typically with complexity in the simulation's flow of execution and parameterization properties. Execution flows are not necessarily straightforward since they may need multiple processing tasks and iterations. Furthermore, parameter and performance studies are common approaches used to characterize a simulati… ▽ More The current landscape of scientific research is widely based on modeling and simulation, typically with complexity in the simulation's flow of execution and parameterization properties. Execution flows are not necessarily straightforward since they may need multiple processing tasks and iterations. Furthermore, parameter and performance studies are common approaches used to characterize a simulation, often requiring traversal of a large parameter space. High-performance computers offer practical resources at the expense of users handling the setup, submission, and management of jobs. This work presents the design of PaPaS, a portable, lightweight, and generic workflow framework for conducting parallel parameter and performance studies. Workflows are defined using parameter files based on keyword-value pairs syntax, thus removing from the user the overhead of creating complex scripts to manage the workflow. A parameter set consists of any combination of environment variables, files, partial file contents, and command line arguments. PaPaS is being developed in Python 3 with support for distributed parallelization using SSH, batch systems, and C++ MPI. The PaPaS framework will run as user processes, and can be used in single/multi-node and multi-tenant computing systems. An example simulation using the BehaviorSpace tool from NetLogo and a matrix multiply using OpenMP are presented as parameter and performance studies, respectively. The results demonstrate that the PaPaS framework offers a simple method for defining and managing parameter studies, while increasing resource utilization. △ Less

Submitted 25 July, 2018; originally announced July 2018.

Comments: 8 pages, 6 figures, PEARC '18: Practice and Experience in Advanced Research Computing, July 22--26, 2018, Pittsburgh, PA, USA

The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability

Authors: Joel Day, Vijay Ganesh, Paul He, Florin Manea, Dirk Nowotka

Abstract: The study of word equations (or the existential theory of equations over free monoids) is a central topic in mathematics and theoretical computer science. The problem of deciding whether a given word equation has a solution was shown to be decidable by Makanin in the late 1970s, and since then considerable work has been done on this topic. In recent years, this decidability question has gained cri… ▽ More The study of word equations (or the existential theory of equations over free monoids) is a central topic in mathematics and theoretical computer science. The problem of deciding whether a given word equation has a solution was shown to be decidable by Makanin in the late 1970s, and since then considerable work has been done on this topic. In recent years, this decidability question has gained critical importance in the context of string SMT solvers for security analysis. Further, many extensions (e.g., quantifier-free word equations with linear arithmetic over the length function) and fragments (e.g., restrictions on the number of variables) of this theory are important from a theoretical point of view, as well as for program analysis applications. Motivated by these considerations, we prove several new results and thus shed light on the boundary between decidability and undecidability for many fragments and extensions of the first order theory of word equations. △ Less

Submitted 1 February, 2018; originally announced February 2018.

The Hardness of Solving Simple Word Equations

Authors: Joel D. Day, Florin Manea, Dirk Nowotka

Abstract: We investigate the class of regular-ordered word equations. In such equations, each variable occurs at most once in each side and the order of the variables occurring in both sides is the preserved (the variables can be, however, separated by potentially distinct constant factors). Surprisingly, we obtain that solving such simple equations, even when the sides contain exactly the same variables, i… ▽ More We investigate the class of regular-ordered word equations. In such equations, each variable occurs at most once in each side and the order of the variables occurring in both sides is the preserved (the variables can be, however, separated by potentially distinct constant factors). Surprisingly, we obtain that solving such simple equations, even when the sides contain exactly the same variables, is NP-hard. By considerations regarding the combinatorial structure of the minimal solutions of the more general quadratic equations we obtain that the satisfiability problem for regular-ordered equations is in NP. Finally, we also show that a related class of simple word equations, that generalises one-variable equations, is in P. △ Less

Submitted 28 February, 2017; v1 submitted 25 February, 2017; originally announced February 2017.

Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA

Authors: Andrew Currin, Konstantin Korovin, Maria Ababi, Katherine Roper, Douglas B. Kell, Philip J. Day, Ross D. King

Abstract: The theory of computer science is based around Universal Turing Machines (UTMs): abstract machines able to execute all possible algorithms. Modern digital computers are physical embodiments of UTMs. The nondeterministic polynomial (NP) time complexity class of problems is the most significant in computer science, and an efficient (i.e. polynomial P) way to solve such problems would be of profound… ▽ More The theory of computer science is based around Universal Turing Machines (UTMs): abstract machines able to execute all possible algorithms. Modern digital computers are physical embodiments of UTMs. The nondeterministic polynomial (NP) time complexity class of problems is the most significant in computer science, and an efficient (i.e. polynomial P) way to solve such problems would be of profound economic and social importance. By definition nondeterministic UTMs (NUTMs) solve NP complete problems in P time. However, NUTMs have previously been believed to be physically impossible to construct. Thue string rewriting systems are computationally equivalent to UTMs, and are naturally nondeterministic. Here we describe the physical design for a NUTM that implements a universal Thue system. The design exploits the ability of DNA to replicate to execute an exponential number of computational paths in P time. Each Thue rewriting step is embodied in a DNA edit implemented using a novel combination of polymerase chain reactions and site-directed mutagenesis. We demonstrate that this design works using both computational modelling and in vitro molecular biology experimentation. The current design has limitations, such as restricted error-correction. However, it opens up the prospect of engineering NUTM based computers able to outperform all standard computers on important practical problems. △ Less

Submitted 27 July, 2016; originally announced July 2016.

MSC Class: 68Q10; 68Q12; 68Q15; 68Q17 ACM Class: B.0; C.1.m; F.1.1; F.4.2; F.4.3

A Fast and Effective Local Search Algorithm for Optimizing the Placement of Wind Turbines

Authors: Markus Wagner, Jareth Day, Frank Neumann

Abstract: The placement of wind turbines on a given area of land such that the wind farm produces a maximum amount of energy is a challenging optimization problem. In this article, we tackle this problem, taking into account wake effects that are produced by the different turbines on the wind farm. We significantly improve upon existing results for the minimization of wake effects by developing a new proble… ▽ More The placement of wind turbines on a given area of land such that the wind farm produces a maximum amount of energy is a challenging optimization problem. In this article, we tackle this problem, taking into account wake effects that are produced by the different turbines on the wind farm. We significantly improve upon existing results for the minimization of wake effects by developing a new problem-specific local search algorithm. One key step in the speed-up of our algorithm is the reduction in computation time needed to assess a given wind farm layout compared to previous approaches. Our new method allows the optimization of large real-world scenarios within a single night on a standard computer, whereas weeks on specialized computing servers were required for previous approaches. △ Less

Submitted 20 April, 2012; originally announced April 2012.

Comments: 16 pages, 2 algorithms, 4 figures, 1 table

Evolving Pacing Strategies for Team Pursuit Track Cycling

Authors: Markus Wagner, Jareth Day, Diora Jordan, Trent Kroeger, Frank Neumann

Abstract: Team pursuit track cycling is a bicycle racing sport held on velodromes and is part of the Summer Olympics. It involves the use of strategies to minimize the overall time that a team of cyclists needs to complete a race. We present an optimisation framework for team pursuit track cycling and show how to evolve strategies using metaheuristics for this interesting real-world problem. Our experimenta… ▽ More Team pursuit track cycling is a bicycle racing sport held on velodromes and is part of the Summer Olympics. It involves the use of strategies to minimize the overall time that a team of cyclists needs to complete a race. We present an optimisation framework for team pursuit track cycling and show how to evolve strategies using metaheuristics for this interesting real-world problem. Our experimental results show that these heuristics lead to significantly better strategies than state-of-art strategies that are currently used by teams of cyclists. △ Less

Submitted 16 June, 2011; v1 submitted 5 April, 2011; originally announced April 2011.