Computing and Information Systems - Research Publications
Permanent URI for this collection
Search Results
1 - 10 of 12
-
ItemNo Preview AvailableA Decomposition-Based Algorithm for the Scheduling of Open-Pit Networks over Multiple Time Periods(INFORMS (Institute for Operations Research and Management Sciences), 2016)We consider the multiple-time-period, short-term production scheduling problem for a network of multiple open-pit mines and ports. Ore produced at each mine, in each period, is transported by rail to a set of ports and blended into products for shipping. Each port forms these blends to a specification, as stipulated in contracts with downstream customers. This problem belongs to a class of multiple producer/consumer scheduling problems in which producers are able to generate a range of products, a combination of which are required by consumers to meet specified demands. In practice, short-term schedules are formed independently at each mine, tasked with achieving a grade and quality target outlined in a medium-term plan. Because of uncertainty in the data available to a medium-term planner and the dynamics of the mining environment, such targets may not be feasible in the short term. In this paper, we present an algorithm in which the grade and quality targets assigned to each mine are iteratively adapted, ensuring the satisfaction of blending constraints at each port while generating schedules for each mine that maximise resource utilisation. This paper was accepted by Yinyu Ye, optimization.
-
ItemNo Preview AvailableMulti-objective short-term production scheduling for open-pit mines: a hierarchical decomposition-based algorithm(TAYLOR & FRANCIS LTD, 2018-12-02)This article presents a novel algorithm for solving a short-term open-pit production-scheduling problem in which several objectives, of varying priority, characterize the quality of each solution. A popular approach employs receding horizon control, dividing the horizon into N period-aggregates of increasing size (number of periods or span). An N-period mixed integer program (MIP) is solved for each period in the original horizon to incrementally construct a production schedule one period at a time. This article presents a new algorithm that, in contrast, decomposes the horizon into N period-aggregates of equal size. Given a schedule for these N periods, obtained by solving an N-period MIP, the first of these aggregates is itself decomposed into an N-period scheduling problem with guidance provided on what regions of the mine should be extracted. The performance of this hierarchical decomposition-based approach is compared with that of receding horizon control on a suite of data sets generated from an operating mine producing millions of tons of ore annually. As the number of objectives being optimized increases, the hierarchical decomposition-based algorithm outperforms receding horizon control, in a majority of instances.
-
ItemNo Preview AvailableShort-term planning for open pit mines: a review(TAYLOR & FRANCIS LTD, 2019-07-04)This review examines the current state-of-the-art in short-term planning for open-pit mines, with a granularity that spans days, weeks or months, and a horizon of less than one to two years. In the academic literature, the short-term planning problem for open-pit mines has not been as widely considered as that for the medium- and long-term horizons. We highlight the differences between short- and longer term planning in terms of both the level of detail to which a mine site is modelled, and the objectives that are optimised when making decisions. We summarise the range of techniques that have been developed for generating short-term plans, capturing both mathematical programming-based methods and heuristic approaches using local-search and decomposition. We identify key challenges and future directions in which to advance the state-of-the-art in short-term planning for open-pit mines.
-
ItemExplaining circuit propagation(SPRINGER, 2014-01)
-
ItemSymmetries, almost symmetries, and lazy clause generation(SPRINGER, 2014-10)
-
ItemThe future of optimization technology(SPRINGER, 2014-04)
-
ItemSynthesizing Optimal Switching Lattices(Association for Computing Machinery, 2014-11)The use of nanoscale technologies to create electronic devices has revived interest in the use of regular structures for defining complex logic functions. One such structure is the switching lattice, a two-dimensional lattice of four-terminal switches. We show how to directly construct switching lattices of polynomial size from arbitrary logic functions; we also show how to synthesize minimal-sized lattices by translating the problem to the satisfiability problem for a restricted class of quantified Boolean formulas. The synthesis method is an anytime algorithm that uses modern SAT solving technology and dichotomic search. It improves considerably on an earlier proposal for creating switching lattices for arbitrary logic functions.
-
ItemA complete refinement procedure for regular separability of context-free languages(ELSEVIER SCIENCE BV, 2016-04-25)Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present a class of semi-decision procedures for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two effective instances of this approach, one that is complete but relatively expensive, and one that is inexpensive and sound, but for which we do not have a completeness proof. The complete method will prove disjointness whenever the input languages are regularly separable. Both methods will terminate whenever the input languages overlap. We provide an experimental evaluation of these procedures, and demonstrate their practicality on a range of verification and language-theoretic instances.
-
ItemReference Abstract Domains and Applications to String Analysis(IOS Press, 2018-02-09)Abstract interpretation is a well established theory that supports reasoning about the run-time behaviour of programs. It achieves tractable reasoning by considering abstractions of run-time states, rather than the states themselves. The chosen set of abstractions is referred to as the abstract domain. We develop a novel framework for combining (a possibly large number of) abstract domains. It achieves the effect of the so-called reduced product without requiring a quadratic number of functions to translate information among abstract domains. A central notion is a reference domain, a medium for information exchange. Our approach suggests a novel and simpler way to manage the integration of large numbers of abstract domains. We instantiate our framework in the context of string analysis. Browser-embedded dynamic programming languages such as JavaScript and PHP encourage the use of strings as a universal data type for both code and data values. The ensuing vulnerabilities have made string analysis a focus of much recent research. String analysis tends to combine many elementary string abstract domains, each designed to capture a specific aspect of strings. For this instance the set of regular languages, while too expensive to use directly for analysis, provides an attractive reference domain, enabling the efficient simulation of reduced products of multiple string abstract domains.
-
ItemWombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation(Springer Netherlands, 2019-10-15)We develop an idea originally proposed by Michel and Van Hentenryck of how to perform bit-vector constraint propagation on the word level. Most operations are propagated in constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by (ultimately) bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. Bit-blasting generates intermediate variables which can be an advantage, as these can be searched on and learnt about. As each approach has advantages, it makes sense to try to combine them. In this paper, we describe an approach to bit-vector solving using word-level propagation with learning. We have designed alternative word-level propagators to Michel and Van Hentenryck’s, and evaluated different variants of the approach. We have also experimented with different approaches to learning and back-jumping in the solver. Based on the insights gained, we have built a portfolio solver, Wombit, which essentially extends the STP bit-vector solver. Using machine learning techniques, the solver makes a judicious up-front decision about whether to use word-level propagation or fall back on bit-blasting.