Showing 1–50 of 83 results for author: Stuckey, P

Temporal Planning via Interval Logic Satisfiability for Autonomous Systems

Authors: Miquel Ramirez, Anubhav Singh, Peter Stuckey, Chris Manzie

Abstract: Many automated planning methods and formulations rely on suitably designed abstractions or simplifications of the constrained dynamics associated with agents to attain computational scalability. We consider formulations of temporal planning where intervals are associated with both action and fluent atoms, and relations between these are given as sentences in Allen's Interval Logic. We propose a no… ▽ More Many automated planning methods and formulations rely on suitably designed abstractions or simplifications of the constrained dynamics associated with agents to attain computational scalability. We consider formulations of temporal planning where intervals are associated with both action and fluent atoms, and relations between these are given as sentences in Allen's Interval Logic. We propose a notion of planning graphs that can account for complex concurrency relations between actions and fluents as a Constraint Programming (CP) model. We test an implementation of our algorithm on a state-of-the-art framework for CP and compare it with PDDL 2.1 planners that capture plans requiring complex concurrent interactions between agents. We demonstrate our algorithm outperforms existing PDDL 2.1 planners in the case studies. Still, scalability remains challenging when plans must comply with intricate concurrent interactions and the sequencing of actions. △ Less

Submitted 13 June, 2024; originally announced June 2024.

Comments: This publication is an extended version of a manuscript submitted to ICAPS-24 (and rejected). Please contact the first author for queries, comments or discussion of the paper

GeckoGraph: A Visual Language for Polymorphic Types

Authors: Shuai Fu, Tim Dwyer, Peter J. Stuckey

Abstract: Polymorphic types are an important feature in most strongly typed programming languages. They allow functions to be written in a way that can be used with different data types, while still enforcing the relationship and constraints between the values. However, programmers often find polymorphic types difficult to use and understand and tend to reason using concrete types. We propose GeckoGraph, a… ▽ More Polymorphic types are an important feature in most strongly typed programming languages. They allow functions to be written in a way that can be used with different data types, while still enforcing the relationship and constraints between the values. However, programmers often find polymorphic types difficult to use and understand and tend to reason using concrete types. We propose GeckoGraph, a graphical notation for types. GeckoGraph aims to accompany traditional text-based type notation and to make reading, understanding, and comparing types easier. We conducted a large-scale human study using GeckoGraph compared to text-based type notation. To our knowledge, this is the largest controlled user study on functional programming ever conducted. The results of the study show that GeckoGraph helps improve programmers' ability to succeed in the programming tasks we designed, especially for novice programmers. △ Less

Submitted 21 May, 2024; originally announced May 2024.

Goanna: Resolving Haskell Type Errors With Minimal Correction Subsets

Authors: Shuai Fu, Tim Dwyer, Peter J. Stuckey, John Grundy

Abstract: Statically typed languages offer significant advantages, such as bug prevention, enhanced code quality, and reduced maintenance costs. However, these benefits often come at the expense of a steep learning curve and a slower development pace. Haskell, known for its expressive and strict type system, poses challenges for inexperienced programmers in learning and using its type system, especially in… ▽ More Statically typed languages offer significant advantages, such as bug prevention, enhanced code quality, and reduced maintenance costs. However, these benefits often come at the expense of a steep learning curve and a slower development pace. Haskell, known for its expressive and strict type system, poses challenges for inexperienced programmers in learning and using its type system, especially in debugging type errors. We introduce Goanna, a novel tool that serves as a type checker and an interactive type error debugging tool for Haskell. When encountering type errors, Goanna identifies a comprehensive list of potential causes and resolutions based on the minimum correction subsets (MCS) enumeration. We evaluated Goanna's effectiveness using 86 diverse Haskell programs from online discourse, demonstrating its ability to accurately identify and resolve type errors. Additionally, we present a collection of techniques and heuristics to enhance Goanna's suggestion-based error diagnosis and show their effectiveness from our evaluation. △ Less

Submitted 21 May, 2024; originally announced May 2024.

Efficient Weighting Schemes for Auditing Instant-Runoff Voting Elections

Authors: Alexander Ek, Philip B. Stark, Peter J. Stuckey, Damjan Vukcevic

Abstract: Various risk-limiting audit (RLA) methods have been developed for instant-runoff voting (IRV) elections. A recent method, AWAIRE, is the first efficient approach that can take advantage of but does not require cast vote records (CVRs). AWAIRE involves adaptively weighted averages of test statistics, essentially "learning" an effective set of hypotheses to test. However, the initial paper on AWAIRE… ▽ More Various risk-limiting audit (RLA) methods have been developed for instant-runoff voting (IRV) elections. A recent method, AWAIRE, is the first efficient approach that can take advantage of but does not require cast vote records (CVRs). AWAIRE involves adaptively weighted averages of test statistics, essentially "learning" an effective set of hypotheses to test. However, the initial paper on AWAIRE only examined a few weighting schemes and parameter settings. We explore schemes and settings more extensively, to identify and recommend efficient choices for practice. We focus on the case where CVRs are not available, assessing performance using simulations based on real election data. The most effective schemes are often those that place most or all of the weight on the apparent "best" hypotheses based on already seen data. Conversely, the optimal tuning parameters tended to vary based on the election margin. Nonetheless, we quantify the performance trade-offs for different choices across varying election margins, aiding in selecting the most desirable trade-off if a default option is needed. A limitation of the current AWAIRE implementation is its restriction to a small number of candidates -- up to six in previous implementations. One path to a more computationally efficient implementation would be to use lazy evaluation and avoid considering all possible hypotheses. Our findings suggest that such an approach could be done without substantially compromising statistical performance. △ Less

Submitted 6 May, 2024; v1 submitted 18 February, 2024; originally announced March 2024.

Comments: 15 pages, 4, figures, presented at Voting'24. The current version includes some improved wording and fixes a few errors

RLAs for 2-Seat STV Elections: Revisited

Authors: Michelle Blom, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: Single Transferable Vote (STV) elections are a principled approach to electing multiple candidates in a single election. Each ballot has a starting value of 1, and a candidate is elected if they gather a total vote value more than a defined quota. Votes over the quota have their value reduced by a transfer value so as to remove the quota, and are passed to the next candidate on the ballot. Risk-li… ▽ More Single Transferable Vote (STV) elections are a principled approach to electing multiple candidates in a single election. Each ballot has a starting value of 1, and a candidate is elected if they gather a total vote value more than a defined quota. Votes over the quota have their value reduced by a transfer value so as to remove the quota, and are passed to the next candidate on the ballot. Risk-limiting audits (RLAs) are a statistically sound approach to election auditing which guarantees that failure to detect an error in the result is bounded by a limit. A first approach to RLAs for 2-seat STV elections has been defined. In this paper we show how we can improve this approach by reasoning about lower bounds on transfer values, and how we can extend the approach to partially audit an election, if the method does not support a full audit. △ Less

Submitted 6 February, 2024; originally announced February 2024.

Anytime Approximate Formal Feature Attribution

Authors: **qiang Yu, Graham Farr, Alexey Ignatiev, Peter J. Stuckey

Abstract: Widespread use of artificial intelligence (AI) algorithms and machine learning (ML) models on the one hand and a number of crucial issues pertaining to them warrant the need for explainable artificial intelligence (XAI). A key explainability question is: given this decision was made, what are the input features which contributed to the decision? Although a range of XAI approaches exist to tackle t… ▽ More Widespread use of artificial intelligence (AI) algorithms and machine learning (ML) models on the one hand and a number of crucial issues pertaining to them warrant the need for explainable artificial intelligence (XAI). A key explainability question is: given this decision was made, what are the input features which contributed to the decision? Although a range of XAI approaches exist to tackle this problem, most of them have significant limitations. Heuristic XAI approaches suffer from the lack of quality guarantees, and often try to approximate Shapley values, which is not the same as explaining which features contribute to a decision. A recent alternative is so-called formal feature attribution (FFA), which defines feature importance as the fraction of formal abductive explanations (AXp's) containing the given feature. This measures feature importance from the view of formally reasoning about the model's behavior. It is challenging to compute FFA using its definition because that involves counting AXp's, although one can approximate it. Based on these results, this paper makes several contributions. First, it gives compelling evidence that computing FFA is intractable, even if the set of contrastive formal explanations (CXp's) is provided, by proving that the problem is #P-hard. Second, by using the duality between AXp's and CXp's, it proposes an efficient heuristic to switch from CXp enumeration to AXp enumeration on-the-fly resulting in an adaptive explanation enumeration algorithm effectively approximating FFA in an anytime fashion. Finally, experimental results obtained on a range of widely used datasets demonstrate the effectiveness of the proposed FFA approximation approach in terms of the error of FFA approximation as well as the number of explanations computed and their diversity given a fixed time limit. △ Less

Submitted 11 December, 2023; originally announced December 2023.

Traffic Flow Optimisation for Lifelong Multi-Agent Path Finding

Authors: Zhe Chen, Daniel Harabor, Jiaoyang Li, Peter J. Stuckey

Abstract: Multi-Agent Path Finding (MAPF) is a fundamental problem in robotics that asks us to compute collision-free paths for a team of agents, all moving across a shared map. Although many works appear on this topic, all current algorithms struggle as the number of agents grows. The principal reason is that existing approaches typically plan free-flow optimal paths, which creates congestion. To tackle th… ▽ More Multi-Agent Path Finding (MAPF) is a fundamental problem in robotics that asks us to compute collision-free paths for a team of agents, all moving across a shared map. Although many works appear on this topic, all current algorithms struggle as the number of agents grows. The principal reason is that existing approaches typically plan free-flow optimal paths, which creates congestion. To tackle this issue, we propose a new approach for MAPF where agents are guided to their destination by following congestion-avoiding paths. We evaluate the idea in two large-scale settings: one-shot MAPF, where each agent has a single destination, and lifelong MAPF, where agents are continuously assigned new destinations. Empirically, we report large improvements in solution quality for one-short MAPF and in overall throughput for lifelong MAPF. △ Less

Submitted 31 January, 2024; v1 submitted 22 August, 2023; originally announced August 2023.

Comments: The paper was accepted for publication at AAAI 2024

The divergence time of protein structures modelled by Markov matrices and its relation to the divergence of sequences

Authors: Sandun Rajapaksa, Lloyd Allison, Peter J. Stuckey, Maria Garcia de la Banda, Arun S. Konagurthu

Abstract: A complete time-parameterized statistical model quantifying the divergent evolution of protein structures in terms of the patterns of conservation of their secondary structures is inferred from a large collection of protein 3D structure alignments. This provides a better alternative to time-parameterized sequence-based models of protein relatedness, that have clear limitations dealing with twiligh… ▽ More A complete time-parameterized statistical model quantifying the divergent evolution of protein structures in terms of the patterns of conservation of their secondary structures is inferred from a large collection of protein 3D structure alignments. This provides a better alternative to time-parameterized sequence-based models of protein relatedness, that have clear limitations dealing with twilight and midnight zones of sequence relationships. Since protein structures are far more conserved due to the selection pressure directly placed on their function, divergence time estimates can be more accurate when inferred from structures. We use the Bayesian and information-theoretic framework of Minimum Message Length to infer a time-parameterized stochastic matrix (accounting for perturbed structural states of related residues) and associated Dirichlet models (accounting for insertions and deletions during the evolution of protein domains). These are used in concert to estimate the Markov time of divergence of tertiary structures, a task previously only possible using proxies (like RMSD). By analyzing one million pairs of homologous structures, we yield a relationship between the Markov divergence time of structures and of sequences. Using these inferred models and the relationship between the divergence of sequences and structures, we demonstrate a competitive performance in secondary structure prediction against neural network architectures commonly employed for this task. The source code and supplementary information are downloadable from \url{http://lcb.infotech.monash.edu.au/sstsum}. △ Less

Submitted 10 August, 2023; originally announced August 2023.

Comments: 12 pages, 6 figures

Adaptively Weighted Audits of Instant-Runoff Voting Elections: AWAIRE

Authors: Alexander Ek, Philip B. Stark, Peter J. Stuckey, Damjan Vukcevic

Abstract: An election audit is risk-limiting if the audit limits (to a pre-specified threshold) the chance that an erroneous electoral outcome will be certified. Extant methods for auditing instant-runoff voting (IRV) elections are either not risk-limiting or require cast vote records (CVRs), the voting system's electronic record of the votes on each ballot. CVRs are not always available, for instance, in j… ▽ More An election audit is risk-limiting if the audit limits (to a pre-specified threshold) the chance that an erroneous electoral outcome will be certified. Extant methods for auditing instant-runoff voting (IRV) elections are either not risk-limiting or require cast vote records (CVRs), the voting system's electronic record of the votes on each ballot. CVRs are not always available, for instance, in jurisdictions that tabulate IRV contests manually. We develop an RLA method (AWAIRE) that uses adaptively weighted averages of test supermartingales to efficiently audit IRV elections when CVRs are not available. The adaptive weighting 'learns' an efficient set of hypotheses to test to confirm the election outcome. When accurate CVRs are available, AWAIRE can use them to increase the efficiency to match the performance of existing methods that require CVRs. We provide an open-source prototype implementation that can handle elections with up to six candidates. Simulations using data from real elections show that AWAIRE is likely to be efficient in practice. We discuss how to extend the computational approach to handle elections with more candidates. Adaptively weighted averages of test supermartingales are a general tool, useful beyond election audits to test collections of hypotheses sequentially while rigorously controlling the familywise error rate. △ Less

Submitted 5 October, 2023; v1 submitted 20 July, 2023; originally announced July 2023.

Comments: 16 pages, 3 figures. Presented at E-Vote-ID 2023. This version contains minor corrections to match the final published version

Journal ref: Electronic Voting, E-Vote-ID 2023, Lecture Notes in Computer Science 14230 (2023) 35-51

Lifted Sequential Planning with Lazy Constraint Generation Solvers

Authors: Anubhav Singh, Miquel Ramirez, Nir Lipovetzky, Peter J. Stuckey

Abstract: This paper studies the possibilities made open by the use of Lazy Clause Generation (LCG) based approaches to Constraint Programming (CP) for tackling sequential classical planning. We propose a novel CP model based on seminal ideas on so-called lifted causal encodings for planning as satisfiability, that does not require grounding, as choosing groundings for functions and action schemas becomes a… ▽ More This paper studies the possibilities made open by the use of Lazy Clause Generation (LCG) based approaches to Constraint Programming (CP) for tackling sequential classical planning. We propose a novel CP model based on seminal ideas on so-called lifted causal encodings for planning as satisfiability, that does not require grounding, as choosing groundings for functions and action schemas becomes an integral part of the problem of designing valid plans. This encoding does not require encoding frame axioms, and does not explicitly represent states as decision variables for every plan step. We also present a propagator procedure that illustrates the possibilities of LCG to widen the kind of inference methods considered to be feasible in planning as (iterated) CSP solving. We test encodings and propagators over classic IPC and recently proposed benchmarks for lifted planning, and report that for planning problem instances requiring fewer plan steps our methods compare very well with the state-of-the-art in optimal sequential planning. △ Less

Submitted 17 July, 2023; originally announced July 2023.

ACM Class: I.2.8; I.2.4

On Formal Feature Attribution and Its Approximation

Authors: **qiang Yu, Alexey Ignatiev, Peter J. Stuckey

Abstract: Recent years have witnessed the widespread use of artificial intelligence (AI) algorithms and machine learning (ML) models. Despite their tremendous success, a number of vital problems like ML model brittleness, their fairness, and the lack of interpretability warrant the need for the active developments in explainable artificial intelligence (XAI) and formal ML model verification. The two major l… ▽ More Recent years have witnessed the widespread use of artificial intelligence (AI) algorithms and machine learning (ML) models. Despite their tremendous success, a number of vital problems like ML model brittleness, their fairness, and the lack of interpretability warrant the need for the active developments in explainable artificial intelligence (XAI) and formal ML model verification. The two major lines of work in XAI include feature selection methods, e.g. Anchors, and feature attribution techniques, e.g. LIME and SHAP. Despite their promise, most of the existing feature selection and attribution approaches are susceptible to a range of critical issues, including explanation unsoundness and out-of-distribution sampling. A recent formal approach to XAI (FXAI) although serving as an alternative to the above and free of these issues suffers from a few other limitations. For instance and besides the scalability limitation, the formal approach is unable to tackle the feature attribution problem. Additionally, a formal explanation despite being formally sound is typically quite large, which hampers its applicability in practical settings. Motivated by the above, this paper proposes a way to apply the apparatus of formal XAI to the case of feature attribution based on formal explanation enumeration. Formal feature attribution (FFA) is argued to be advantageous over the existing methods, both formal and non-formal. Given the practical complexity of the problem, the paper then proposes an efficient technique for approximating exact FFA. Finally, it offers experimental evidence of the effectiveness of the proposed approximate FFA in comparison to the existing feature attribution algorithms not only in terms of feature importance and but also in terms of their relative order. △ Less

Submitted 28 August, 2023; v1 submitted 7 July, 2023; originally announced July 2023.

Reducing Redundant Work in Jump Point Search

Authors: Shizhe Zhao, Daniel Harabor, Peter J. Stuckey

Abstract: JPS (Jump Point Search) is a state-of-the-art optimal algorithm for online grid-based pathfinding. Widely used in games and other navigation scenarios, JPS nevertheless can exhibit pathological behaviours which are not well studied: (i) it may repeatedly scan the same area of the map to find successors; (ii) it may generate and expand suboptimal search nodes. In this work, we examine the source of… ▽ More JPS (Jump Point Search) is a state-of-the-art optimal algorithm for online grid-based pathfinding. Widely used in games and other navigation scenarios, JPS nevertheless can exhibit pathological behaviours which are not well studied: (i) it may repeatedly scan the same area of the map to find successors; (ii) it may generate and expand suboptimal search nodes. In this work, we examine the source of these pathological behaviours, show how they can occur in practice, and propose a purely online approach, called Constrained JPS (CJPS), to tackle them efficiently. Experimental results show that CJPS has low overheads and is often faster than JPS in dynamically changing grid environments: by up to 7x in large game maps and up to 14x in pathological scenarios. △ Less

Submitted 28 June, 2023; originally announced June 2023.

Delivering Inflated Explanations

Authors: Yacine Izza, Alexey Ignatiev, Peter Stuckey, Joao Marques-Silva

Abstract: In the quest for Explainable Artificial Intelligence (XAI) one of the questions that frequently arises given a decision made by an AI system is, ``why was the decision made in this way?'' Formal approaches to explainability build a formal model of the AI system and use this to reason about the properties of the system. Given a set of feature values for an instance to be explained, and a resulting… ▽ More In the quest for Explainable Artificial Intelligence (XAI) one of the questions that frequently arises given a decision made by an AI system is, ``why was the decision made in this way?'' Formal approaches to explainability build a formal model of the AI system and use this to reason about the properties of the system. Given a set of feature values for an instance to be explained, and a resulting decision, a formal abductive explanation is a set of features, such that if they take the given value will always lead to the same decision. This explanation is useful, it shows that only some features were used in making the final decision. But it is narrow, it only shows that if the selected features take their given values the decision is unchanged. It's possible that some features may change values and still lead to the same decision. In this paper we formally define inflated explanations which is a set of features, and for each feature of set of values (always including the value of the instance being explained), such that the decision will remain unchanged. Inflated explanations are more informative than abductive explanations since e.g they allow us to see if the exact value of a feature is important, or it could be any nearby value. Overall they allow us to better understand the role of each feature in the decision. We show that we can compute inflated explanations for not that much greater cost than abductive explanations, and that we can extend duality results for abductive explanations also to inflated explanations. △ Less

Submitted 27 June, 2023; originally announced June 2023.

Scalable Rail Planning and Replanning with Soft Deadlines

Authors: Zhe Chen, Jiaoyang Li, Daniel Harabor, Peter J. Stuckey

Abstract: The Flatland Challenge, which was first held in 2019 and reported in NeurIPS 2020, is designed to answer the question: How to efficiently manage dense traffic on complex rail networks? Considering the significance of punctuality in real-world railway network operation and the fact that fast passenger trains share the network with slow freight trains, Flatland version 3 introduces trains with diffe… ▽ More The Flatland Challenge, which was first held in 2019 and reported in NeurIPS 2020, is designed to answer the question: How to efficiently manage dense traffic on complex rail networks? Considering the significance of punctuality in real-world railway network operation and the fact that fast passenger trains share the network with slow freight trains, Flatland version 3 introduces trains with different speeds and scheduling time windows. This paper introduces the Flatland 3 problem definitions and extends an award-winning MAPF-based software, which won the NeurIPS 2020 competition, to efficiently solve Flatland 3 problems. The resulting system won the Flatland 3 competition. We designed a new priority ordering for initial planning, a new neighbourhood selection strategy for efficient solution quality improvement with Multi-Agent Path Finding via Large Neighborhood Search(MAPF-LNS), and use MAPF-LNS for partially replanning the trains influenced by malfunction. △ Less

Submitted 10 June, 2023; originally announced June 2023.

Tracking Progress in Multi-Agent Path Finding

Authors: Bojie Shen, Zhe Chen, Muhammad Aamir Cheema, Daniel D. Harabor, Peter J. Stuckey

Abstract: Multi-Agent Path Finding (MAPF) is an important core problem for many new and emerging industrial applications. Many works appear on this topic each year, and a large number of substantial advancements and performance improvements have been reported. Yet measuring overall progress in MAPF is difficult: there are many potential competitors, and the computational burden for comprehensive experimenta… ▽ More Multi-Agent Path Finding (MAPF) is an important core problem for many new and emerging industrial applications. Many works appear on this topic each year, and a large number of substantial advancements and performance improvements have been reported. Yet measuring overall progress in MAPF is difficult: there are many potential competitors, and the computational burden for comprehensive experimentation is prohibitively large. Moreover, detailed data from past experimentation is usually unavailable. In this work, we introduce a set of methodological and visualisation tools which can help the community establish clear indicators for state-of-the-art MAPF performance and which can facilitate large-scale comparisons between MAPF solvers. Our objectives are to lower the barrier of entry for new researchers and to further promote the study of MAPF, since progress in the area and the main challenges are made much clearer. △ Less

Submitted 15 May, 2023; originally announced May 2023.

Risk-Limiting Audits for Condorcet Elections

Authors: Michelle Blom, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: Elections where electors rank the candidates (or a subset of the candidates) in order of preference allow the collection of more information about the electors' intent. The most widely used election of this type is Instant-Runoff Voting (IRV), where candidates are eliminated one by one, until a single candidate holds the majority of the remaining ballots. Condorcet elections treat the election as… ▽ More Elections where electors rank the candidates (or a subset of the candidates) in order of preference allow the collection of more information about the electors' intent. The most widely used election of this type is Instant-Runoff Voting (IRV), where candidates are eliminated one by one, until a single candidate holds the majority of the remaining ballots. Condorcet elections treat the election as a set of simultaneous decisions about each pair of candidates. The Condorcet winner is the candidate who beats all others in these pairwise contests. There are various proposals to determine a winner if no Condorcet winner exists. In this paper we show how we can efficiently audit Condorcet elections for a number of variations. We also compare the audit efficiency (how many ballots we expect to sample) of IRV and Condorcet elections. △ Less

Submitted 19 April, 2023; v1 submitted 18 March, 2023; originally announced March 2023.

Comments: 15 pages, accepted for Voting'23. This version fixes some errors in one of the examples

Journal ref: FC 2023 Workshops, Lecture Notes in Computer Science 13953 (2024) 79-94

ChameleonIDE: Untangling Type Errors Through Interactive Visualization and Exploration

Authors: Shuai Fu, Tim Dwyer, Peter J. Stuckey, Jackson Wain, Jesse Linossier

Abstract: Dynamically typed programming languages are popular in education and the software industry. While presenting a low barrier to entry, they suffer from run-time type errors and longer-term problems in code quality and maintainability. Statically typed languages, while showing strength in these aspects, lack in learnability and ease of use. In particular, fixing type errors poses challenges to both n… ▽ More Dynamically typed programming languages are popular in education and the software industry. While presenting a low barrier to entry, they suffer from run-time type errors and longer-term problems in code quality and maintainability. Statically typed languages, while showing strength in these aspects, lack in learnability and ease of use. In particular, fixing type errors poses challenges to both novice users and experts. Further, compiler-type error messages are presented in a static way that is biased toward the first occurrence of the error in the program code. To help users resolve such type errors, we introduce ChameleonIDE, a type debugging tool that presents type errors to the user in an unbiased way, allowing them to explore the full context of where the errors could occur. Programmers can interactively verify the steps of reasoning against their intention. Through three studies involving real programmers, we showed that ChameleonIDE is more effective in fixing type errors than traditional text-based error messages. This difference is more significant in harder tasks. Further, programmers actively using ChameleonIDE's interactive features are shown to be more efficient in fixing type errors than passively reading the type error output. △ Less

Submitted 17 March, 2023; originally announced March 2023.

Comparison and Evaluation of Methods for a Predict+Optimize Problem in Renewable Energy

Authors: Christoph Bergmeir, Frits de Nijs, Abishek Sriramulu, Mahdi Abolghasemi, Richard Bean, John Betts, Quang Bui, Nam Trong Dinh, Nils Einecke, Rasul Esmaeilbeigi, Scott Ferraro, Priya Galketiya, Evgenii Genov, Robert Glasgow, Rakshitha Godahewa, Yanfei Kang, Steffen Limmer, Luis Magdalena, Pablo Montero-Manso, Daniel Peralta, Yogesh Pipada Sunil Kumar, Alejandro Rosales-Pérez, Julian Ruddick, Akylas Stratigakos, Peter Stuckey , et al. (3 additional authors not shown)

Abstract: Algorithms that involve both forecasting and optimization are at the core of solutions to many difficult real-world problems, such as in supply chains (inventory optimization), traffic, and in the transition towards carbon-free energy generation in battery/load/production scheduling in sustainable energy systems. Typically, in these scenarios we want to solve an optimization problem that depends o… ▽ More Algorithms that involve both forecasting and optimization are at the core of solutions to many difficult real-world problems, such as in supply chains (inventory optimization), traffic, and in the transition towards carbon-free energy generation in battery/load/production scheduling in sustainable energy systems. Typically, in these scenarios we want to solve an optimization problem that depends on unknown future values, which therefore need to be forecast. As both forecasting and optimization are difficult problems in their own right, relatively few research has been done in this area. This paper presents the findings of the ``IEEE-CIS Technical Challenge on Predict+Optimize for Renewable Energy Scheduling," held in 2021. We present a comparison and evaluation of the seven highest-ranked solutions in the competition, to provide researchers with a benchmark problem and to establish the state of the art for this benchmark, with the aim to foster and facilitate research in this area. The competition used data from the Monash Microgrid, as well as weather data and energy market data. It then focused on two main challenges: forecasting renewable energy production and demand, and obtaining an optimal schedule for the activities (lectures) and on-site batteries that lead to the lowest cost of energy. The most accurate forecasts were obtained by gradient-boosted tree and random forest models, and optimization was mostly performed using mixed integer linear and quadratic programming. The winning method predicted different scenarios and optimized over all scenarios jointly using a sample average approximation method. △ Less

Submitted 20 December, 2022; originally announced December 2022.

Ballot-Polling Audits of Instant-Runoff Voting Elections with a Dirichlet-Tree Model

Authors: Floyd Everest, Michelle Blom, Philip B. Stark, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: Instant-runoff voting (IRV) is used in several countries around the world. It requires voters to rank candidates in order of preference, and uses a counting algorithm that is more complex than systems such as first-past-the-post or scoring rules. An even more complex system, the single transferable vote (STV), is used when multiple candidates need to be elected. The complexity of these systems has… ▽ More Instant-runoff voting (IRV) is used in several countries around the world. It requires voters to rank candidates in order of preference, and uses a counting algorithm that is more complex than systems such as first-past-the-post or scoring rules. An even more complex system, the single transferable vote (STV), is used when multiple candidates need to be elected. The complexity of these systems has made it difficult to audit the election outcomes. There is currently no known risk-limiting audit (RLA) method for STV, other than a full manual count of the ballots. A new approach to auditing these systems was recently proposed, based on a Dirichlet-tree model. We present a detailed analysis of this approach for ballot-polling Bayesian audits of IRV elections. We compared several choices for the prior distribution, including some approaches using a Bayesian bootstrap (equivalent to an improper prior). Our findings include that the bootstrap-based approaches can be adapted to perform similarly to a full Bayesian model in practice, and that an overly informative prior can give counter-intuitive results. Via carefully chosen examples, we show why creating an RLA with this model is challenging, but we also suggest ways to overcome this. As well as providing a practical and computationally feasible implementation of a Bayesian IRV audit, our work is important in laying the foundation for an RLA for STV elections. △ Less

Submitted 23 February, 2023; v1 submitted 8 September, 2022; originally announced September 2022.

Comments: 17 pages, 6 figures. Presented at EIS 2022. This version contains minor corrections to match the final published version

Journal ref: ESORICS 2022 Workshops, EIS 2022, Lecture Notes in Computer Science 13785 (2023) 525-540

Multi-Target Search in Euclidean Space with Ray Shooting (Full Version)

Authors: Ryan Hechenberger, Daniel Harabor, Muhammad Aamir Cheema, Peter J Stuckey, Pierre Le Bodic

Abstract: The Euclidean shortest path problem (ESPP) is a well studied problem with many practical applications. Recently a new efficient online approach to this problem, RayScan, has been developed, based on ray shooting and polygon scanning. In this paper we show how we can improve RayScan by carefully reasoning about polygon scans. We also look into how RayScan could be applied in the single-source multi… ▽ More The Euclidean shortest path problem (ESPP) is a well studied problem with many practical applications. Recently a new efficient online approach to this problem, RayScan, has been developed, based on ray shooting and polygon scanning. In this paper we show how we can improve RayScan by carefully reasoning about polygon scans. We also look into how RayScan could be applied in the single-source multi-target scenario, where logic during scanning is used to reduce the number of rays shots required. This improvement also helps in the single target case. We compare the improved RayScan+ against the state-of-the-art ESPP algorithm, illustrating the situations where it is better. △ Less

Submitted 6 July, 2022; originally announced July 2022.

Comments: submitted on SoCS 2021 (as extended abstract)

Auditing Ranked Voting Elections with Dirichlet-Tree Models: First Steps

Authors: Floyd Everest, Michelle Blom, Philip B. Stark, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: Ranked voting systems, such as instant-runoff voting (IRV) and single transferable vote (STV), are used in many places around the world. They are more complex than plurality and scoring rules, presenting a challenge for auditing their outcomes: there is no known risk-limiting audit (RLA) method for STV other than a full hand count. We present a new approach to auditing ranked systems that uses a… ▽ More Ranked voting systems, such as instant-runoff voting (IRV) and single transferable vote (STV), are used in many places around the world. They are more complex than plurality and scoring rules, presenting a challenge for auditing their outcomes: there is no known risk-limiting audit (RLA) method for STV other than a full hand count. We present a new approach to auditing ranked systems that uses a statistical model, a Dirichlet-tree, that can cope with high-dimensional parameters in a computationally efficient manner. We demonstrate this approach with a ballot-polling Bayesian audit for IRV elections. Although the technique is not known to be risk-limiting, we suggest some strategies that might allow it to be calibrated to limit risk. △ Less

Submitted 8 September, 2022; v1 submitted 29 June, 2022; originally announced June 2022.

Comments: 5 pages, 2 figures, accepted for E-Vote-ID 2022. This version has an updated URL for the software package

Journal ref: E-Vote-ID 2022, Conference Proceedings, UT Press, pages 76-80

Eliminating The Impossible, Whatever Remains Must Be True

Authors: **qiang Yu, Alexey Ignatiev, Peter J. Stuckey, Nina Narodytska, Joao Marques-Silva

Abstract: The rise of AI methods to make predictions and decisions has led to a pressing need for more explainable artificial intelligence (XAI) methods. One common approach for XAI is to produce a post-hoc explanation, explaining why a black box ML model made a certain prediction. Formal approaches to post-hoc explanations provide succinct reasons for why a prediction was made, as well as why not another p… ▽ More The rise of AI methods to make predictions and decisions has led to a pressing need for more explainable artificial intelligence (XAI) methods. One common approach for XAI is to produce a post-hoc explanation, explaining why a black box ML model made a certain prediction. Formal approaches to post-hoc explanations provide succinct reasons for why a prediction was made, as well as why not another prediction was made. But these approaches assume that features are independent and uniformly distributed. While this means that "why" explanations are correct, they may be longer than required. It also means the "why not" explanations may be suspect as the counterexamples they rely on may not be meaningful. In this paper, we show how one can apply background knowledge to give more succinct "why" formal explanations, that are presumably easier to interpret by humans, and give more accurate "why not" explanations. In addition, we show how to use existing rule induction techniques to efficiently extract background information from a dataset, and also how to report which background information was used to make an explanation, allowing a human to examine it if they doubt the correctness of the explanation. △ Less

Submitted 30 November, 2022; v1 submitted 19 June, 2022; originally announced June 2022.

Assessing the accuracy of the Australian Senate count: Key steps for a rigorous and transparent audit

Authors: Michelle Blom, Philip B. Stark, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: This paper explains the main principles and some of the technical details for auditing the scanning and digitisation of the Australian Senate ballot papers. We give a short summary of the motivation for auditing paper ballots, explain the necessary supporting steps for a rigorous and transparent audit, and suggest some statistical methods that would be appropriate for the Australian Senate. 22 J… ▽ More This paper explains the main principles and some of the technical details for auditing the scanning and digitisation of the Australian Senate ballot papers. We give a short summary of the motivation for auditing paper ballots, explain the necessary supporting steps for a rigorous and transparent audit, and suggest some statistical methods that would be appropriate for the Australian Senate. 22 June 2022 Update: The update includes analysis of Senate preference data from the 2022 Australian election. △ Less

Submitted 22 June, 2022; v1 submitted 29 May, 2022; originally announced May 2022.

A First Approach to Risk-Limiting Audits for Single Transferable Vote Elections

Authors: Michelle Blom, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: Risk-limiting audits (RLAs) are an increasingly important method for checking that the reported outcome of an election is, in fact, correct. Indeed, their use is increasingly being legislated. While effective methods for RLAs have been developed for many forms of election -- for example: first-past-the-post, instant-runoff voting, and D'Hondt elections -- auditing methods for single transferable v… ▽ More Risk-limiting audits (RLAs) are an increasingly important method for checking that the reported outcome of an election is, in fact, correct. Indeed, their use is increasingly being legislated. While effective methods for RLAs have been developed for many forms of election -- for example: first-past-the-post, instant-runoff voting, and D'Hondt elections -- auditing methods for single transferable vote (STV) elections have yet to be developed. STV elections are notoriously hard to reason about since there is a complex interaction of votes that change their value throughout the process. In this paper we present the first approach to risk-limiting audits for STV elections, restricted to the case of 2-seat STV elections. △ Less

Submitted 18 December, 2021; originally announced December 2021.

Comments: 16 pages

Journal ref: FC 2022 Workshops, Lecture Notes in Computer Science 13412 (2023) 366-380

Integrated Task Assignment and Path Planning for Capacitated Multi-Agent Pickup and Delivery

Authors: Zhe Chen, Javier Alonso-Mora, Xiaoshan Bai, Daniel D. Harabor, Peter J. Stuckey

Abstract: Multi-agent Pickup and Delivery (MAPD) is a challenging industrial problem where a team of robots is tasked with transporting a set of tasks, each from an initial location and each to a specified target location. Appearing in the context of automated warehouse logistics and automated mail sortation, MAPD requires first deciding which robot is assigned what task (i.e., Task Assignment or TA) follow… ▽ More Multi-agent Pickup and Delivery (MAPD) is a challenging industrial problem where a team of robots is tasked with transporting a set of tasks, each from an initial location and each to a specified target location. Appearing in the context of automated warehouse logistics and automated mail sortation, MAPD requires first deciding which robot is assigned what task (i.e., Task Assignment or TA) followed by a subsequent coordination problem where each robot must be assigned collision-free paths so as to successfully complete its assignment (i.e., Multi-Agent Path Finding or MAPF). Leading methods in this area solve MAPD sequentially: first assigning tasks, then assigning paths. In this work we propose a new coupled method where task assignment choices are informed by actual delivery costs instead of by lower-bound estimates. The main ingredients of our approach are a marginal-cost assignment heuristic and a meta-heuristic improvement strategy based on Large Neighbourhood Search. As a further contribution, we also consider a variant of the MAPD problem where each robot can carry multiple tasks instead of just one. Numerical simulations show that our approach yields efficient and timely solutions and we report significant improvement compared with other recent methods from the literature. △ Less

Submitted 28 October, 2021; originally announced October 2021.

Journal ref: IEEE Robotics and Automation Letters, vol. 6, no. 3, pp. 5816-5823, July 2021

Transformation-Enabled Precondition Inference

Authors: Bishoksan Kafle, Graeme Gange, Peter J. Stuckey, Peter Schachte, Harald Sondergaard

Abstract: Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration maintains over-approximations of the set of safe and unsafe initial states; which are used to partition the program's initial states into those known to… ▽ More Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration maintains over-approximations of the set of safe and unsafe initial states; which are used to partition the program's initial states into those known to be safe, known to be unsafe and unknown. We then construct revised programs with those unknown initial states and iterate the procedure until the approximations are disjoint or some termination criteria are met. An experimental evaluation of the method on a set of software verification benchmarks shows that it can infer precise preconditions (sometimes optimal) that are not possible using previous methods. △ Less

Submitted 6 August, 2021; originally announced August 2021.

Comments: Paper presented at the 37th InternationalConference on Logic Programming (ICLP 2021), 16 pages. arXiv admin note: substantial text overlap with arXiv:1811.06771

Journal ref: Theory and Practice of Logic Programming 21 (2021) 700-716

Planning with Learned Binarized Neural Networks Benchmarks for MaxSAT Evaluation 2021

Authors: Buser Say, Scott Sanner, Jo Devriendt, Jakob Nordström, Peter J. Stuckey

Abstract: This document provides a brief introduction to learned automated planning problem where the state transition function is in the form of a binarized neural network (BNN), presents a general MaxSAT encoding for this problem, and describes the four domains, namely: Navigation, Inventory Control, System Administrator and Cellda, that are submitted as benchmarks for MaxSAT Evaluation 2021. This document provides a brief introduction to learned automated planning problem where the state transition function is in the form of a binarized neural network (BNN), presents a general MaxSAT encoding for this problem, and describes the four domains, namely: Navigation, Inventory Control, System Administrator and Cellda, that are submitted as benchmarks for MaxSAT Evaluation 2021. △ Less

Submitted 2 August, 2021; originally announced August 2021.

Assertion-Based Approaches to Auditing Complex Elections, with Application to Party-List Proportional Elections

Authors: Michelle Blom, Jurlind Budurushi, Ronald L. Rivest, Philip B. Stark, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: Risk-limiting audits (RLAs), an ingredient in evidence-based elections, are increasingly common. They are a rigorous statistical means of ensuring that electoral results are correct, usually without having to perform an expensive full recount -- at the cost of some controlled probability of error. A recently developed approach for conducting RLAs, SHANGRLA, provides a flexible framework that can e… ▽ More Risk-limiting audits (RLAs), an ingredient in evidence-based elections, are increasingly common. They are a rigorous statistical means of ensuring that electoral results are correct, usually without having to perform an expensive full recount -- at the cost of some controlled probability of error. A recently developed approach for conducting RLAs, SHANGRLA, provides a flexible framework that can encompass a wide variety of social choice functions and audit strategies. Its flexibility comes from reducing sufficient conditions for outcomes to be correct to canonical `assertions' that have a simple mathematical form. Assertions have been developed for auditing various social choice functions including plurality, multi-winner plurality, super-majority, Hamiltonian methods, and instant runoff voting. However, there is no systematic approach to building assertions. Here, we show that assertions with linear dependence on transformations of the votes can easily be transformed to canonical form for SHANGRLA. We illustrate the approach by constructing assertions for party-list elections such as Hamiltonian free list elections and elections using the D'Hondt method, expanding the set of social choice functions to which SHANGRLA applies directly. △ Less

Submitted 2 October, 2021; v1 submitted 25 July, 2021; originally announced July 2021.

Comments: 16 pages

Journal ref: Electronic Voting, E-Vote-ID 2021, Lecture Notes in Computer Science 12900 (2021) 47-62

Pairwise Symmetry Reasoning for Multi-Agent Path Finding Search

Authors: Jiaoyang Li, Daniel Harabor, Peter J. Stuckey, Sven Koenig

Abstract: Multi-Agent Path Finding (MAPF) is a challenging combinatorial problem that asks us to plan collision-free paths for a team of cooperative agents. In this work, we show that one of the reasons why MAPF is so hard to solve is due to a phenomenon called pairwise symmetry, which occurs when two agents have many different paths to their target locations, all of which appear promising, but every combin… ▽ More Multi-Agent Path Finding (MAPF) is a challenging combinatorial problem that asks us to plan collision-free paths for a team of cooperative agents. In this work, we show that one of the reasons why MAPF is so hard to solve is due to a phenomenon called pairwise symmetry, which occurs when two agents have many different paths to their target locations, all of which appear promising, but every combination of them results in a collision. We identify several classes of pairwise symmetries and show that each one arises commonly in practice and can produce an exponential explosion in the space of possible collision resolutions, leading to unacceptable runtimes for current state-of-the-art (bounded-sub)optimal MAPF algorithms. We propose a variety of reasoning techniques that detect the symmetries efficiently as they arise and resolve them by using specialized constraints to eliminate all permutations of pairwise colliding paths in a single branching step. We implement these ideas in the context of the leading optimal MAPF algorithm CBS and show that the addition of the symmetry reasoning techniques can have a dramatic positive effect on its performance - we report a reduction in the number of node expansions by up to four orders of magnitude and an increase in scalability by up to thirty times. These gains allow us to solve to optimality a variety of challenging MAPF instances previously considered out of reach for CBS. △ Less

Submitted 12 March, 2021; originally announced March 2021.

Symmetry Breaking for k-Robust Multi-Agent Path Finding

Authors: Zhe Chen, Daniel Harabor, Jiaoyang Li, Peter J. Stuckey

Abstract: During Multi-Agent Path Finding (MAPF) problems, agents can be delayed by unexpected events. To address such situations recent work describes k-Robust Conflict-BasedSearch (k-CBS): an algorithm that produces coordinated and collision-free plan that is robust for up to k delays. In this work we introducing a variety of pairwise symmetry breaking constraints, specific to k-robust planning, that can… ▽ More During Multi-Agent Path Finding (MAPF) problems, agents can be delayed by unexpected events. To address such situations recent work describes k-Robust Conflict-BasedSearch (k-CBS): an algorithm that produces coordinated and collision-free plan that is robust for up to k delays. In this work we introducing a variety of pairwise symmetry breaking constraints, specific to k-robust planning, that can efficiently find compatible and optimal paths for pairs of conflicting agents. We give a thorough description of the new constraints and report large improvements to success rate ina range of domains including: (i) classic MAPF benchmarks;(ii) automated warehouse domains and; (iii) on maps from the 2019 Flatland Challenge, a recently introduced railway domain where k-robust planning can be fruitfully applied to schedule trains. △ Less

Submitted 28 October, 2021; v1 submitted 17 February, 2021; originally announced February 2021.

Comments: 8 pages. Accepted by Thirty-Fifth AAAI Conference on Artificial Intelligence

Journal ref: Proceedings of the AAAI Conference on Artificial Intelligence, 35(14), 12267-12274 (2021)

Auditing Hamiltonian Elections

Authors: Michelle Blom, Philip B. Stark, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: Presidential primaries are a critical part of the United States Presidential electoral process, since they are used to select the candidates in the Presidential election. While methods differ by state and party, many primaries involve proportional delegate allocation using the so-called Hamilton method. In this paper we show how to conduct risk-limiting audits for delegate allocation elections usi… ▽ More Presidential primaries are a critical part of the United States Presidential electoral process, since they are used to select the candidates in the Presidential election. While methods differ by state and party, many primaries involve proportional delegate allocation using the so-called Hamilton method. In this paper we show how to conduct risk-limiting audits for delegate allocation elections using variants of the Hamilton method where the viability of candidates is determined either by a plurality vote or using instant runoff voting. Experiments on real-world elections show that we can audit primary elections to high confidence (small risk limits) usually at low cost. △ Less

Submitted 29 June, 2021; v1 submitted 16 February, 2021; originally announced February 2021.

Comments: 16 pages

Journal ref: FC 2021 Workshops, Lecture Notes in Computer Science 12676 (2021) 235-250

A Scalable Two Stage Approach to Computing Optimal Decision Sets

Authors: Alexey Ignatiev, Edward Lam, Peter J. Stuckey, Joao Marques-Silva

Abstract: Machine learning (ML) is ubiquitous in modern life. Since it is being deployed in technologies that affect our privacy and safety, it is often crucial to understand the reasoning behind its decisions, warranting the need for explainable AI. Rule-based models, such as decision trees, decision lists, and decision sets, are conventionally deemed to be the most interpretable. Recent work uses proposit… ▽ More Machine learning (ML) is ubiquitous in modern life. Since it is being deployed in technologies that affect our privacy and safety, it is often crucial to understand the reasoning behind its decisions, warranting the need for explainable AI. Rule-based models, such as decision trees, decision lists, and decision sets, are conventionally deemed to be the most interpretable. Recent work uses propositional satisfiability (SAT) solving (and its optimization variants) to generate minimum-size decision sets. Motivated by limited practical scalability of these earlier methods, this paper proposes a novel approach to learn minimum-size decision sets by enumerating individual rules of the target decision set independently of each other, and then solving a set cover problem to select a subset of rules. The approach makes use of modern maximum satisfiability and integer linear programming technologies. Experiments on a wide range of publicly available datasets demonstrate the advantage of the new approach over the state of the art in SAT-based decision set learning. △ Less

Submitted 3 February, 2021; originally announced February 2021.

Divide and Learn: A Divide and Conquer Approach for Predict+Optimize

Authors: Ali Ugur Guler, Emir Demirovic, Jeffrey Chan, James Bailey, Christopher Leckie, Peter J. Stuckey

Abstract: The predict+optimize problem combines machine learning ofproblem coefficients with a combinatorial optimization prob-lem that uses the predicted coefficients. While this problemcan be solved in two separate stages, it is better to directlyminimize the optimization loss. However, this requires dif-ferentiating through a discrete, non-differentiable combina-torial function. Most existing approaches… ▽ More The predict+optimize problem combines machine learning ofproblem coefficients with a combinatorial optimization prob-lem that uses the predicted coefficients. While this problemcan be solved in two separate stages, it is better to directlyminimize the optimization loss. However, this requires dif-ferentiating through a discrete, non-differentiable combina-torial function. Most existing approaches use some form ofsurrogate gradient. Demirovicet alshowed how to directlyexpress the loss of the optimization problem in terms of thepredicted coefficients as a piece-wise linear function. How-ever, their approach is restricted to optimization problemswith a dynamic programming formulation. In this work wepropose a novel divide and conquer algorithm to tackle op-timization problems without this restriction and predict itscoefficients using the optimization loss. We also introduce agreedy version of this approach, which achieves similar re-sults with less computation. We compare our approach withother approaches to the predict+optimize problem and showwe can successfully tackle some hard combinatorial problemsbetter than other predict+optimize methods. △ Less

Submitted 3 December, 2020; originally announced December 2020.

Optimal Decision Lists using SAT

Authors: **qiang Yu, Alexey Ignatiev, Pierre Le Bodic, Peter J. Stuckey

Abstract: Decision lists are one of the most easily explainable machine learning models. Given the renewed emphasis on explainable machine learning decisions, this machine learning model is increasingly attractive, combining small size and clear explainability. In this paper, we show for the first time how to construct optimal "perfect" decision lists which are perfectly accurate on the training data, and m… ▽ More Decision lists are one of the most easily explainable machine learning models. Given the renewed emphasis on explainable machine learning decisions, this machine learning model is increasingly attractive, combining small size and clear explainability. In this paper, we show for the first time how to construct optimal "perfect" decision lists which are perfectly accurate on the training data, and minimal in size, making use of modern SAT solving technology. We also give a new method for determining optimal sparse decision lists, which trade off size and accuracy. We contrast the size and test accuracy of optimal decisions lists versus optimal decision sets, as well as other state-of-the-art methods for determining optimal decision lists. We also examine the size of average explanations generated by decision sets and decision lists. △ Less

Submitted 19 October, 2020; originally announced October 2020.

Optimal Decision Trees for Nonlinear Metrics

Authors: Emir Demirović, Peter J. Stuckey

Abstract: Nonlinear metrics, such as the F1-score, Matthews correlation coefficient, and Fowlkes-Mallows index, are often used to evaluate the performance of machine learning models, in particular, when facing imbalanced datasets that contain more samples of one class than the other. Recent optimal decision tree algorithms have shown remarkable progress in producing trees that are optimal with respect to li… ▽ More Nonlinear metrics, such as the F1-score, Matthews correlation coefficient, and Fowlkes-Mallows index, are often used to evaluate the performance of machine learning models, in particular, when facing imbalanced datasets that contain more samples of one class than the other. Recent optimal decision tree algorithms have shown remarkable progress in producing trees that are optimal with respect to linear criteria, such as accuracy, but unfortunately nonlinear metrics remain a challenge. To address this gap, we propose a novel algorithm based on bi-objective optimisation, which treats misclassifications of each binary class as a separate objective. We show that, for a large class of metrics, the optimal tree lies on the Pareto frontier. Consequently, we obtain the optimal tree by using our method to generate the set of all nondominated trees. To the best of our knowledge, this is the first method to compute provably optimal decision trees for nonlinear metrics. Our approach leads to a trade-off when compared to optimising linear metrics: the resulting trees may be more desirable according to the given nonlinear metric at the expense of higher runtimes. Nevertheless, the experiments illustrate that runtimes are reasonable for majority of the tested datasets. △ Less

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

Journal ref: AAAI 2021

Computing Optimal Decision Sets with SAT

Authors: **qiang Yu, Alexey Ignatiev, Peter J. Stuckey, Pierre Le Bodic

Abstract: As machine learning is increasingly used to help make decisions, there is a demand for these decisions to be explainable. Arguably, the most explainable machine learning models use decision rules. This paper focuses on decision sets, a type of model with unordered rules, which explains each prediction with a single rule. In order to be easy for humans to understand, these rules must be concise. Ea… ▽ More As machine learning is increasingly used to help make decisions, there is a demand for these decisions to be explainable. Arguably, the most explainable machine learning models use decision rules. This paper focuses on decision sets, a type of model with unordered rules, which explains each prediction with a single rule. In order to be easy for humans to understand, these rules must be concise. Earlier work on generating optimal decision sets first minimizes the number of rules, and then minimizes the number of literals, but the resulting rules can often be very large. Here we consider a better measure, namely the total size of the decision set in terms of literals. So we are not driven to a small set of rules which require a large number of literals. We provide the first approach to determine minimum-size decision sets that achieve minimum empirical risk and then investigate sparse alternatives where we trade accuracy for size. By finding optimal solutions we show we can build decision set classifiers that are almost as accurate as the best heuristic methods, but far more concise, and hence more explainable. △ Less

Submitted 29 July, 2020; originally announced July 2020.

MurTree: Optimal Classification Trees via Dynamic Programming and Search

Authors: Emir Demirović, Anna Lukina, Emmanuel Hebrard, Jeffrey Chan, James Bailey, Christopher Leckie, Kotagiri Ramamohanarao, Peter J. Stuckey

Abstract: Decision tree learning is a widely used approach in machine learning, favoured in applications that require concise and interpretable models. Heuristic methods are traditionally used to quickly produce models with reasonably high accuracy. A commonly criticised point, however, is that the resulting trees may not necessarily be the best representation of the data in terms of accuracy and size. In r… ▽ More Decision tree learning is a widely used approach in machine learning, favoured in applications that require concise and interpretable models. Heuristic methods are traditionally used to quickly produce models with reasonably high accuracy. A commonly criticised point, however, is that the resulting trees may not necessarily be the best representation of the data in terms of accuracy and size. In recent years, this motivated the development of optimal classification tree algorithms that globally optimise the decision tree in contrast to heuristic methods that perform a sequence of locally optimal decisions. We follow this line of work and provide a novel algorithm for learning optimal classification trees based on dynamic programming and search. Our algorithm supports constraints on the depth of the tree and number of nodes. The success of our approach is attributed to a series of specialised techniques that exploit properties unique to classification trees. Whereas algorithms for optimal classification trees have traditionally been plagued by high runtimes and limited scalability, we show in a detailed experimental study that our approach uses only a fraction of the time required by the state-of-the-art and can handle datasets with tens of thousands of instances, providing several orders of magnitude improvements and notably contributing towards the practical realisation of optimal decision trees. △ Less

Submitted 28 June, 2022; v1 submitted 24 July, 2020; originally announced July 2020.

Journal ref: Journal of Machine Learning Research 2022

Random errors are not necessarily politically neutral

Authors: Michelle Blom, Andrew Conway, Peter J. Stuckey, Vanessa Teague, Damjan Vukcevic

Abstract: Errors are inevitable in the implementation of any complex process. Here we examine the effect of random errors on Single Transferable Vote (STV) elections, a common approach to deciding multi-seat elections. It is usually expected that random errors should have nearly equal effects on all candidates, and thus be fair. We find to the contrary that random errors can introduce systematic bias into e… ▽ More Errors are inevitable in the implementation of any complex process. Here we examine the effect of random errors on Single Transferable Vote (STV) elections, a common approach to deciding multi-seat elections. It is usually expected that random errors should have nearly equal effects on all candidates, and thus be fair. We find to the contrary that random errors can introduce systematic bias into election results. This is because, even if the errors are random, votes for different candidates occur in different patterns that are affected differently by random errors. In the STV context, the most important effect of random errors is to invalidate the ballot. This removes far more votes for those candidates whose supporters tend to list a lot of preferences, because their ballots are much more likely to be invalidated by random error. Different validity rules for different voting styles mean that errors are much more likely to penalise some types of votes than others. For close elections this systematic bias can change the result of the election. △ Less

Submitted 28 September, 2020; v1 submitted 1 July, 2020; originally announced July 2020.

Journal ref: Electronic Voting, E-Vote-ID 2020, Lecture Notes in Computer Science 12455 (2020) 19-35

Encoding Linear Constraints into SAT

Authors: Ignasi Abío, Valentin Mayer-Eichberger, Peter Stuckey

Abstract: Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of conjunctive normal form perform poorly in problems with these constraints in comparison with SAT modulo theories (SMT), lazy clause generation (LCG) or mixed integer programming (M… ▽ More Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of conjunctive normal form perform poorly in problems with these constraints in comparison with SAT modulo theories (SMT), lazy clause generation (LCG) or mixed integer programming (MIP) solvers. In this paper we explore and categorize SAT encodings for linear integer constraints. We define new SAT encodings based on multi-valued decision diagrams, and sorting networks. We compare different SAT encodings of linear constraints and demonstrate where one may be preferable to another. We also compare SAT encodings against other solving methods and show they can be better than linear integer (MIP) solvers and sometimes better than LCG or SMT solvers on appropriate problems. Combining the new encoding with lazy decomposition, which during runtime only encodes constraints that are important to the solving process that occurs, gives the best option for many highly combinatorial problems involving linear constraints. △ Less

Submitted 5 May, 2020; originally announced May 2020.

You can do RLAs for IRV

Authors: Michelle Blom, Andrew Conway, Dan King, Laurent Sandrolini, Philip B. Stark, Peter J. Stuckey, Vanessa Teague

Abstract: The City and County of San Francisco, CA, has used Instant Runoff Voting (IRV) for some elections since 2004. This report describes the first ever process pilot of Risk Limiting Audits for IRV, for the San Francisco District Attorney's race in November, 2019. We found that the vote-by-mail outcome could be efficiently audited to well under the 0.05 risk limit given a sample of only 200 ballots. Al… ▽ More The City and County of San Francisco, CA, has used Instant Runoff Voting (IRV) for some elections since 2004. This report describes the first ever process pilot of Risk Limiting Audits for IRV, for the San Francisco District Attorney's race in November, 2019. We found that the vote-by-mail outcome could be efficiently audited to well under the 0.05 risk limit given a sample of only 200 ballots. All the software we developed for the pilot is open source. △ Less

Submitted 1 April, 2020; originally announced April 2020.

Smart Predict-and-Optimize for Hard Combinatorial Optimization Problems

Authors: Jaynta Mandi, Emir Demirović, Peter. J Stuckey, Tias Guns

Abstract: Combinatorial optimization assumes that all parameters of the optimization problem, e.g. the weights in the objective function is fixed. Often, these weights are mere estimates and increasingly machine learning techniques are used to for their estimation. Recently, Smart Predict and Optimize (SPO) has been proposed for problems with a linear objective function over the predictions, more specifical… ▽ More Combinatorial optimization assumes that all parameters of the optimization problem, e.g. the weights in the objective function is fixed. Often, these weights are mere estimates and increasingly machine learning techniques are used to for their estimation. Recently, Smart Predict and Optimize (SPO) has been proposed for problems with a linear objective function over the predictions, more specifically linear programming problems. It takes the regret of the predictions on the linear problem into account, by repeatedly solving it during learning. We investigate the use of SPO to solve more realistic discrete optimization problems. The main challenge is the repeated solving of the optimization problem. To this end, we investigate ways to relax the problem as well as warmstarting the learning and the solving. Our results show that even for discrete problems it often suffices to train by solving the relaxation in the SPO loss. Furthermore, this approach outperforms, for most instances, the state-of-the-art approach of Wilder, Dilkina, and Tambe. We experiment with weighted knapsack problems as well as complex scheduling problems and show for the first time that a predict-and-optimize approach can successfully be used on large-scale combinatorial optimization problems. △ Less

Submitted 22 November, 2019; originally announced November 2019.

RAIRE: Risk-Limiting Audits for IRV Elections

Authors: Michelle Blom, Peter J. Stuckey, Vanessa Teague

Abstract: Risk-limiting post election audits guarantee a high probability of correcting incorrect election results, independent of why the result was incorrect. Ballot-polling audits select ballots at random and interpret those ballots as evidence for and against the reported result, continuing this process until either they support the recorded result, or they fall back to a full manual recount. For electi… ▽ More Risk-limiting post election audits guarantee a high probability of correcting incorrect election results, independent of why the result was incorrect. Ballot-polling audits select ballots at random and interpret those ballots as evidence for and against the reported result, continuing this process until either they support the recorded result, or they fall back to a full manual recount. For elections with digitised scanning and counting of ballots, a comparison audit compares randomly selected digital ballots with their paper versions. Discrepancies are referred to as errors, and are used to build evidence against or in support of the recorded result. Risk-limiting audits for first-past-the-post elections are well understood, and used in some US elections. We define a number of approaches to ballot-polling and comparison risk-limiting audits for Instant Runoff Voting (IRV) elections. We show that for almost all real elections we found, we can perform a risk-limiting audit by looking at only a small fraction of the total ballots (assuming no errors were made in the tallying and distribution of votes). △ Less

Submitted 29 October, 2019; v1 submitted 20 March, 2019; originally announced March 2019.

Solution Dominance over Constraint Satisfaction Problems

Authors: Tias Guns, Peter J. Stuckey, Guido Tack

Abstract: Constraint Satisfaction Problems (CSPs) typically have many solutions that satisfy all constraints. Often though, some solutions are preferred over others, that is, some solutions dominate other solutions. We present solution dominance as a formal framework to reason about such settings. We define Constraint Dominance Problems (CDPs) as CSPs with a dominance relation, that is, a preorder over the… ▽ More Constraint Satisfaction Problems (CSPs) typically have many solutions that satisfy all constraints. Often though, some solutions are preferred over others, that is, some solutions dominate other solutions. We present solution dominance as a formal framework to reason about such settings. We define Constraint Dominance Problems (CDPs) as CSPs with a dominance relation, that is, a preorder over the solutions of the CSP. This framework captures many well-known variants of constraint satisfaction, including optimization, multi-objective optimization, Max-CSP, minimal models, minimum correction subsets as well as optimization over CP-nets and arbitrary dominance relations. We extend MiniZinc, a declarative language for modeling CSPs, to CDPs by introducing dominance nogoods; these can be derived from dominance relations in a principled way. A generic method for solving arbitrary CDPs incrementally calls a CSP solver and is compatible with any existing solver that supports MiniZinc. This encourages experimenting with different solution dominance relations for a problem, as well as comparing different solvers without having to modify their implementations. △ Less

Submitted 21 December, 2018; originally announced December 2018.

Comments: Presented at the ModRef18 workshop at CP18

ACM Class: I.2.8

Searching with Consistent Prioritization for Multi-Agent Path Finding

Authors: Hang Ma, Daniel Harabor, Peter J. Stuckey, Jiaoyang Li, Sven Koenig

Abstract: We study prioritized planning for Multi-Agent Path Finding (MAPF). Existing prioritized MAPF algorithms depend on rule-of-thumb heuristics and random assignment to determine a fixed total priority ordering of all agents a priori. We instead explore the space of all possible partial priority orderings as part of a novel systematic and conflict-driven combinatorial search framework. In a variety of… ▽ More We study prioritized planning for Multi-Agent Path Finding (MAPF). Existing prioritized MAPF algorithms depend on rule-of-thumb heuristics and random assignment to determine a fixed total priority ordering of all agents a priori. We instead explore the space of all possible partial priority orderings as part of a novel systematic and conflict-driven combinatorial search framework. In a variety of empirical comparisons, we demonstrate state-of-the-art solution qualities and success rates, often with similar runtimes to existing algorithms. We also develop new theoretical results that explore the limitations of prioritized planning, in terms of completeness and optimality, for the first time. △ Less

Submitted 15 December, 2018; originally announced December 2018.

Comments: AAAI 2019

Precondition Inference via Partitioning of Initial States

Authors: Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J. Stuckey

Abstract: Precondition inference is a non-trivial task with several applications in program analysis and verification. We present a novel iterative method for automatically deriving sufficient preconditions for safety and unsafety of programs which introduces a new dimension of modularity. Each iteration maintains over-approximations of the set of \emph{safe} and \emph{unsafe} \emph{initial} states. Then we… ▽ More Precondition inference is a non-trivial task with several applications in program analysis and verification. We present a novel iterative method for automatically deriving sufficient preconditions for safety and unsafety of programs which introduces a new dimension of modularity. Each iteration maintains over-approximations of the set of \emph{safe} and \emph{unsafe} \emph{initial} states. Then we repeatedly use the current abstractions to partition the program's \emph{initial} states into those known to be safe, known to be unsafe and unknown, and construct a revised program focusing on those initial states that are not yet known to be safe or unsafe. An experimental evaluation of the method on a set of software verification benchmarks shows that it can solve problems which are not solvable using previous methods. △ Less

Submitted 16 November, 2018; originally announced November 2018.

Comments: 19 pages, 8 figures

Pre-proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018)

Authors: Fred Mesnard, Peter J. Stuckey

Abstract: This volume constitutes the pre-proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), held on 4-6th September 2018 in Frankfurt am Main, Germany and co-located with the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018) and the 26th International Workshop on Functional and Logic Programming (WF… ▽ More This volume constitutes the pre-proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), held on 4-6th September 2018 in Frankfurt am Main, Germany and co-located with the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018) and the 26th International Workshop on Functional and Logic Programming (WFLP 2018). △ Less

Submitted 11 September, 2018; v1 submitted 2 August, 2018; originally announced August 2018.

Comments: Corrected typos

An iterative approach to precondition inference using constrained Horn clauses

Authors: Bishoksan Kafle, John P. Gallagher, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J. Stuckey

Abstract: We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then i… ▽ More We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from the loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions. △ Less

Submitted 16 April, 2018; originally announced April 2018.

Comments: Paper presented at the 34nd International Conference on Logic Programming (ICLP 2018), Oxford, UK, July 14 to July 17, 2018 18 pages, LaTeX

Computing the Margin of Victory in Preferential Parliamentary Elections

Authors: Michelle Blom, Peter J. Stuckey, Vanessa Teague

Abstract: We show how to use automated computation of election margins to assess the number of votes that would need to change in order to alter a parliamentary outcome for single-member preferential electorates. In the context of increasing automation of Australian electoral processes, and accusations of deliberate interference in elections in Europe and the USA, this work forms the basis of a rigorous sta… ▽ More We show how to use automated computation of election margins to assess the number of votes that would need to change in order to alter a parliamentary outcome for single-member preferential electorates. In the context of increasing automation of Australian electoral processes, and accusations of deliberate interference in elections in Europe and the USA, this work forms the basis of a rigorous statistical audit of the parliamentary election outcome. Our example is the New South Wales Legislative Council election of 2015, but the same process could be used for any similar parliament for which data was available, such as the Australian House of Representatives given the proposed automatic scanning of ballots. △ Less

Submitted 31 July, 2017; originally announced August 2017.

Towards Computing Victory Margins in STV Elections

Authors: Michelle Blom, Peter J. Stuckey, Vanessa J. Teague

Abstract: The Single Transferable Vote (STV) is a system of preferential voting employed in multi-seat elections. Each vote cast by a voter is a (potentially partial) ranking over a set of candidates. No techniques currently exist for computing the margin of victory (MOV) in STV elections. The MOV is the smallest number of vote manipulations (changes, additions, and deletions) required to bring about a chan… ▽ More The Single Transferable Vote (STV) is a system of preferential voting employed in multi-seat elections. Each vote cast by a voter is a (potentially partial) ranking over a set of candidates. No techniques currently exist for computing the margin of victory (MOV) in STV elections. The MOV is the smallest number of vote manipulations (changes, additions, and deletions) required to bring about a change in the set of elected candidates. Knowledge of the MOV of an election gives greater insight into both how much time and money should be spent on the auditing of the election, and whether uncovered mistakes (such as ballot box losses) throw the election result into doubt---requiring a costly repeat election---or can be safely ignored. In this paper, we present algorithms for computing lower and upper bounds on the MOV in STV elections. In small instances, these algorithms are able to compute exact margins. △ Less

Submitted 16 August, 2017; v1 submitted 9 March, 2017; originally announced March 2017.

Comments: 24 pages, 4 figures, 9 tables

MiniZinc with Strings

Authors: Roberto Amadini, Pierre Flener, Justin Pearson, Joseph D. Scott, Peter J. Stuckey, Guido Tack

Abstract: Strings are extensively used in modern programming languages and constraints over strings of unknown length occur in a wide range of real-world applications such as software analysis and verification, testing, model checking, and web security. Nevertheless, practically no CP solver natively supports string constraints. We introduce string variables and a suitable set of string constraints as built… ▽ More Strings are extensively used in modern programming languages and constraints over strings of unknown length occur in a wide range of real-world applications such as software analysis and verification, testing, model checking, and web security. Nevertheless, practically no CP solver natively supports string constraints. We introduce string variables and a suitable set of string constraints as builtin features of the MiniZinc modelling language. Furthermore, we define an interpreter for converting a MiniZinc model with strings into a FlatZinc instance relying on only integer variables. This provides a user-friendly interface for modelling combinatorial problems with strings, and enables both string and non-string solvers to actually solve such problems. △ Less

Submitted 11 August, 2016; originally announced August 2016.

Comments: Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)

Report number: LOPSTR/2016/7