Global constraints are a central concept in Constraint Programming (CP), which allow modellers to compactly express complex relations, and which allow solvers to efficiently handle them. Table constraints have especially been well-studied as they can express arbitrary finite relations, and are extensively used in CP benchmarks. In this paper we study how to best deal with table constraints when using Integer Linear Programming (ILP) solvers. We study two paradigms: linear encodings, and a lazy cut generation approach. For the encoding we propose a novel MDD-based flow encoding. For the cut generation, in which lazy constraints are generated on-demand during branch-and-cut search, we investigate different ways of generating such integer and fractional cuts as well as how to strengthen them through shrinking and cut lifting. We experimentally compare the different approaches on CP competition instances with a wide variety of table constraints, showing clear benefits over the standard integer encoding.

As a field of AI, Machine Reasoning (MR) uses largely symbolic means to formalize and emulate abstract reasoning. Studies in early MR have notably started inquiries into Explainable AI (XAI) -- arguably one of the biggest concerns today for the AI community. Work on explainable MR as well as on MR approaches to explainability in other areas of AI has continued ever since. It is especially potent in modern MR branches, such as argumentation, constraint and logic programming, planning. We hereby aim to provide a selective overview of MR explainability techniques and studies in hopes that insights from this long track of research will complement well the current XAI landscape. This document reports our work in-progress on MR explainability.

Inspired by concepts of constraint-based local search, we present a novel scheme for automatically relaxing a given high-level model into an optimisation model that is better suited for large neighbourhood search (LNS). By exploiting the variable sharing and semantics of the constraints in a model, our scheme (1) identifies constraints that can easily be satisfied simultaneously and can thus constrain the neighbourhood, and (2) relaxes the remaining constraints. As a side effect, our scheme enables the LNS solving of a constraint satisfaction problem, by transforming it into an optimisation problem, and the faster solving of a difficult-to-satisfy constrained optimisation problem, by finding the initial incumbent faster. This scheme can be used with any CP-based LNS solver. We tested a portfolio of CP-based LNS variants running in parallel, with a multi-armed bandit to select which LNS variant to run. Our results show that this approach is very competitive.

This abstract presents a simulated annealing based approach that constructs hyper-spectral images from the frequency spectrums of a distributed acoustic sensing system and iteratively improves them through the training of learnable filters. The aim is to construct an image that represents features of signals from events while repressing noise. Hyper-spectral images are specifically created for downstream computer vision tasks such as object detection. Hyper-spectral images are images with more than three channels that are derived from a frequency spectrum to obtain the spectrum for each image pixel. Simulated annealing is used to train the filters to automatically select frequencies and bin them into frequency bands. Each frequency band is mapped into an image channel. We fully integrate our filtering method with an object detection network so that filters are trained in conjunction with the neural network. The detection model serves as both the measure and the selector. Our simulated annealing approach significantly outperforms current state-of-the-art methods by a margin of 22%. Limitations include a dependency on randomness and excluding parts of the search space prematuraly due to the design of the local moves.

We study the problem of optimizing a guidance policy capable of dynamically guiding the agents for lifelong Multi-Agent Path Finding based on real-time traffic patterns. Multi-Agent Path Finding (MAPF) focuses on moving multiple agents from their starts to goals without collisions. Its lifelong variant, LMAPF, continuously assigns new goals to agents. In this work, we focus on improving the solution quality of PIBT, a state-of-the-art rule-based LMAPF algorithm, by optimizing a policy to generate adaptive guidance. We design two pipelines to incorporate guidance in PIBT in two different ways. We demonstrate the superiority of the optimized policy over both static guidance and human-designed policies. Additionally, we explore scenarios where task distribution changes over time, a challenging yet common situation in real-world applications that is rarely explored in the literature.

In multi-agent systems, when we account for the possibility of delays during execution, online planning becomes more complicated, as both execution and planning should be able to handle delays when agents are moving. Lifelong Multi-Agent Path Finding (LMAPF) is the problem of (re)planning the collision-free moves of agents to their goals in a shared space, while agents continuously receive new goals. PIE (Planning and Improving while Executing) is a recent approach to LMAPF which concurrently replans later parts of agents' trajectories while execution occurs. However, the execution is assumed to be perfect. Existing approaches either use policy-based methods to quickly coordinate agents every timestep with instant delay feedback, or deploy an execution policy to adjust a solution for delays on the fly. These approaches may introduce large amounts of unnecessary delays to agents due to their planner guarantees or simple delay-handling policies. In this paper, we extend PIE to define a framework for solving the lifelong MAPF problem with execution delays. We instantiate our framework with different execution and replanning strategies, and experimentally evaluate them. Overall, we find that this framework can substantially improve the throughput by up to a factor 3 for lifelong MAPF, compared to approaches that handle delays with simple execution policies.

Visual Grounding (VG) tasks, such as referring expression detection and segmentation tasks are important for linking visual entities to context, especially in complex reasoning tasks that require detailed query interpretation. This paper explores VG beyond basic perception, highlighting challenges for methods that require reasoning like human cognition. Recent advances in large language methods (LLMs) and Vision-Language methods (VLMs) have improved abilities for visual comprehension, contextual understanding, and reasoning. These methods are mainly split into end-to-end and compositional methods, with the latter offering more flexibility. Compositional approaches that integrate LLMs and foundation models show promising performance but still struggle with complex reasoning with language-based logical representations. To address these limitations, we propose NAVER, a compositional visual grounding method that integrates explicit probabilistic logic reasoning within a finite-state automaton, equipped with a self-correcting mechanism. This design improves robustness and interpretability in inference through explicit logic reasoning. Our results show that NAVER achieves SoTA performance comparing to recent end-to-end and compositional baselines. The code is available at https://github.com/ControlNet/NAVER .

We present a novel solution for multimodal pathfinding in cities, which enables scenarios involving unlimited transfers at customized transfer speeds, requiring minimal preprocessing and storage efforts. We show that in this problem, classical variations of the TD-Dijkstra algorithm have better performance in terms of query runtime and memory usage than state-of-the-art algorithms, such as Connection Scan Algorithm [1] or Round-Based Public Transit Routing [2], since these do not require computing the transitive closure of the transfer graph. By incorporating techniques widely used in the field of computational geometry, we outperform the classical TD-Dijkstra approach, which saves all departure times for a node in a Balanced Search Tree (BST) structure [3]. We generalize the approach of storing departure times for each node and call it Timetable Nodes (TTN) [4], proposing two new versions of it: one using a Combined Search Tree (TTN-CST) and the other employing Fractional Cascading [5] (TTN-FC). Both modifications require minimal preprocessing efforts to store information about the public transport schedule, enabling them to function potentially on mobile devices and perform better than BST. We show theoretical and practical benefits of the TTN-FC over other approaches. TTN-FC accelerates pathfinding and reduces memory usage by a factor of$k$compared to TTN-CST and TTN-BST, where$k$is the number of outgoing edges from a node.

Delays in public transport are common, often impacting users through prolonged travel times and missed transfers. Existing solutions for handling delays remain limited; backup plans based on historical data miss opportunities for earlier arrivals, while snapshot planning accounts for current delays but not future ones. With the growing availability of live delay data, users can adjust their journeys in real-time. However, the literature lacks a framework that fully exploits this advantage for system-scale dynamic replanning. To address this, we formalise the dynamic replanning problem in public transport routing and propose two solutions: a "pull" approach, where users manually request replanning, and a novel "push" approach, where the server proactively monitors and adjusts journeys. Our experiments show that the push approach outperforms the pull approach, achieving significant speedups. The results also reveal substantial arrival time savings enabled by dynamic replanning.

Explainable Artificial Intelligence (XAI) is critical for attaining trust in the operation of AI systems. A key question of an AI system is ``why was this decision made this way''. Formal approaches to XAI use a formal model of the AI system to identify abductive explanations. While abductive explanations may be applicable to a large number of inputs sharing the same concrete values, more general explanations may be preferred for numeric inputs. So-called inflated abductive explanations give intervals for each feature ensuring that any input whose values fall withing these intervals is still guaranteed to make the same prediction. Inflated explanations cover a larger portion of the input space, and hence are deemed more general explanations. But there can be many (inflated) abductive explanations for an instance. Which is the best? In this paper, we show how to find a most general abductive explanation for an AI decision. This explanation covers as much of the input space as possible, while still being a correct formal explanation of the model's behaviour. Given that we only want to give a human one explanation for a decision, the most general explanation gives us the explanation with the broadest applicability, and hence the one most likely to seem sensible.

Tree Cache is a lightweight pre-processing approach to grid path finding which works by generating a shortest path tree: from a root cell to all cells in the map. During online search Tree Cache simply follows the tree: from start and target towards the root, stopping at the first common cell. Although Tree Cache is fast, the resulting paths have no solution quality guarantees. In this paper we improve Tree Cache, in terms of speed and solution quality, by combining symmetry breaking ideas from Jump Point Search. Our new algorithm, Jump Spanning Tree Search (JSTS), can usually generate paths with low average sub-optimality in under one microsecond -- up to two orders of magnitude faster than Tree Cache. We then extend JSTS to derive a new and very fast bounded suboptimal search, which guarantees solution quality in single-digit microseconds on average. Our results establish a remarkable new level of performance in the area. In particular, we show JSTS approaches and often improves upon the output complexity of an idealised oracle, which simply reads off and returns a corresponding but optimal solution path.

Multi-agent path finding is the problem of navigating a set of agents from their starting locations to their target locations while avoiding collisions. A leading method for optimal multi-agent path finding is branch-and-cut-and-price, a framework based on mathematical optimization. The reference implementation, named BCP-MAPF, shows highly competitive results against AI-based search. This paper presents BCP2-MAPF, a new implementation of branch-and-cut-and-price paired with a novel low-level path finder based on time intervals. Experimental results demonstrate that BCP2-MAPF significantly outperforms the other state-of-the-art optimal algorithms BCP-MAPF, Lazy CBS and CBSH2-RTC.

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.

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 is 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 a set of values (always including the value of the instance being explained), such that the decision will remain unchanged, for any of the values allowed for any of the features in the (inflated) abductive explanation. Inflated formal explanations are more informative than common 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.

In applications of Multi-Agent Path Finding (MAPF), it is often the sum of planning and execution times that needs to be minimised (i.e., the Goal Achievement Time). Yet current methods seldom optimise for this objective. Optimal algorithms reduce execution time, but may require exponential planning time. Non-optimal algorithms reduce planning time, but at the expense of increased path length. To address these limitations we introduce PIE (Planning and Improving while Executing), a new framework for concurrent planning and execution in MAPF. We show how different instantiations of PIE affect practical performance, including initial planning time, action commitment time and concurrent vs. sequential planning and execution. We then adapt PIE to Lifelong MAPF, a popular application setting where agents are continuously assigned new goals and where additional decisions are required to ensure feasibility. We examine a variety of different approaches to overcome these challenges and we conduct comparative experiments vs. recently proposed alternatives. Results show that PIE substantially outperforms existing methods for One-shot and Lifelong MAPF.

The recently-proposed framework of Predict+Optimize tackles optimization problems with parameters that are unknown at solving time, in a supervised learning setting. Prior frameworks consider only the scenario where all unknown parameters are (eventually) revealed simultaneously. In this work, we propose Multi-Stage Predict+Optimize, a novel extension catering to applications where unknown parameters are revealed in sequential stages, with optimization decisions made in between. We further develop three training algorithms for neural networks (NNs) for our framework as proof of concept, both of which handle all mixed integer linear programs. The first baseline algorithm is a natural extension of prior work, training a single NN which makes a single prediction of unknown parameters. The second and third algorithms instead leverage the possibility of updating parameter predictions between stages, and trains one NN per stage. To handle the interdependency between the neural networks, we adopt sequential and parallelized versions of coordinate descent for training. Experimentation on three benchmarks demonstrates the superior learning performance of our methods over classical approaches.

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. Existing scalable approaches struggle as the number of agents grows, as they 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. Empirically, we report large improvements in overall throughput for lifelong MAPF while coordinating more than ten thousand agents.

Symmetry breaking and weighted-suboptimal search are two popular speed up techniques used in pathfinding search. It is a commonly held assumption that they are orthogonal and easily combined. In this paper we illustrate that this is not necessarily the case when combining a number of symmetry breaking methods, based on Jump Point Search, with Weighted A*, a bounded suboptimal search approach which does not require node re-expansions. Surprisingly, the combination of these two methods can cause search to fail, finding no path to a target node when clearly such paths exist. We demonstrate this phenomena and show how we can modify the combination to always succeed with low overhead.

Facility Location Problems (FLPs) arise while serving multiple customers in a shared environment, minimizing transportation and other costs. Hence, they involve the optimal placement of facilities. They are defined on graphs as well as in Euclidean spaces with or without obstacles; and they are typically NP-hard to solve optimally. There are many heuristic algorithms tailored to different kinds of FLPs. However, FLPs defined in Euclidean spaces without obstacles are the most amenable to efficient and effective heuristic algorithms. This motivates the idea of quickly reformulating FLPs on graphs and in Euclidean spaces with obstacles to FLPs in Euclidean spaces without obstacles. Towards this end, we propose a new approach that uses FastMap and Locality Sensitive Hashing. FastMap is a near-linear-time algorithm that embeds the vertices of a graph in a Euclidean space while approximately preserving graph-based distances as Euclidean distances for all pairs of vertices. Through extensive experiments, we show that our approach significantly outperforms other state-of-the-art competing algorithms on a variety of FLPs: the Multi-Agent Meeting, Vertex K-Median (VKM), Weighted VKM, and the Capacitated VKM problems.

In applications of Multi-Agent Path Finding (MAPF), it is often the sum of planning and execution times that needs to be minimised (i.e., the Goal Achievement Time). Yet current methods seldom optimise for this objective. Optimal algorithms reduce execution time, but may require exponential planning time. Non-optimal algorithms reduce planning time, but at the expense of increased path length. To address these limitations we introduce PIE (Planning and Improving while Executing), a new framework for concurrent planning and execution in MAPF. We first show how PIE for one-shot MAPF improves practical performance compared to sequential planning and execution.We then adapt PIE to Lifelong MAPF, a popular application setting where agents are continuously assigned new goals and where additional decisions are required to ensure feasibility. We examine a variety of different approaches to overcome these challenges and we conduct comparative experiments vs. recently proposed alternatives. Results show that PIE substantially outperforms existing methods for One-shot and Lifelong MAPF.

Given a loop-free sequence of instructions, superoptimization techniques use a constraint solver to search for an equivalent sequence that is optimal for a desired objective. The complexity of the search grows exponentially with the length of the solution being constructed and the problem becomes intractable for large sequences of instructions. This paper presents a new approach to superoptimizing stack-bytecode via three novel components: (1) a greedy algorithm to refine the bound on the length of the optimal solution; (2) a new representation of the optimization problem as a set of weighted soft clauses in MaxSAT; (3) a series of domain-specific dominance and redundant constraints to reduce the search space for optimal solutions. We have developed a tool, named S uper S tack , which can be used to find optimal code translations of modern stack-based bytecode, namely WebAssembly or Ethereum bytecode. Experimental evaluation on more than 500,000 sequences shows the proposed greedy, constraint-based and SAT combination is able to greatly increase optimization gains achieved by existing superoptimizers and reduce to at least a fourth the optimization time.

Just-in-Tim e (JIT) defect prediction has been proposed to help teams prioritize the limited resources on the most risky commits (or pull requests), yet it remains largely a black box, whose predictions are not explainable or actionable to practitioners. Thus, prior studies have applied various model-agnostic techniques to explain the predictions of JIT models. Yet, explanations generated from existing model-agnostic techniques are still not formally sound, robust, and actionable. In this article, we propose FoX , a Fo rmal e X plainer for JIT Defect Prediction, which builds on formal reasoning about the behavior of JIT defect prediction models and hence is able to provide provably correct explanations, which are additionally guaranteed to be minimal. Our experimental results show that FoX is able to efficiently generate provably correct, robust, and actionable explanations, while existing model-agnostic techniques cannot. Our survey study with 54 software practitioners provides valuable insights into the usefulness and trustworthiness of our FoX approach; 86% of participants agreed that our approach is useful, while 74% of participants found it trustworthy. Thus, this article serves as an important stepping stone towards trustable explanations for JIT models to help domain experts and practitioners better understand why a commit is predicted as defective and what to do to mitigate the risk.

In many computer games up to hundreds of agents navigate in real-time across a dynamically changing weighted grid map. Pathfinding in these situations is challenging because the grids are large, traversal costs are not uniform, and because each shortest path has many symmetric permutations, all of which must be considered by an optimal online search. In this work we introduce Weighted Jump Point Search (JPSW), a new type of pathfinding algorithm which breaks weighted grid symmetries by introducing a tiebreaking policy that allows us to apply effective pruning rules in symmetric regions. We show that these pruning rules preserve at least one optimal path to every grid cell and that their application can yield large performance improvements for optimal pathfinding. We give a complete theoretical description of the new algorithm, including pseudo-code. We also conduct a wide-ranging experimental evaluation, including data from real games. Results indicate JPSW is up to orders of magnitude faster than the nearest baseline, online search using A*.

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.

The rapid rise of Artificial Intelligence (AI) and Machine Learning (ML) has invoked the need for explainable AI (XAI). One of the most prominent approaches to XAI is to train rule-based ML models, e.g. decision trees, lists and sets, that are deemed interpretable due to their transparent nature. Recent years have witnessed a large body of work in the area of constraints- and reasoning-based approaches to the inference of interpretable models, in particular decision sets (DSes). Despite being shown to outperform heuristic approaches in terms of accuracy, most of them suffer from scalability issues and often fail to handle large training data, in which case no solution is offered. Motivated by this limitation and the success of gradient boosted trees, we propose a novel anytime approach to producing DSes that are both accurate and interpretable. The approach makes use of the concept of a generalized formal explanation and builds on the recent advances in formal explainability of gradient boosted trees. Experimental results obtained on a wide range of datasets, demonstrate that our approach produces DSes that more accurate than those of the state-of-the-art algorithms and comparable with them in terms of explanation size.

The assignment of products to storage locations significantly impacts the efficiency of warehouse operations. We propose a multi-phase optimizer for a Storage Location Assignment Problem (SLAP) where solution quality is based on a distance estimate of future-forecasted order picking. Candidate assignments are first sampled using a Markov Chain accept/reject method. Future-forecasted pick-rounds are then modified according to the candidate assignments and solved as Traveling Salesman Problems (TSP). The model is graph-based and generalizes to any obstacle layout in 2D. Due to the intractability of the SLAP, methods are proposed to speed up search for strong solution candidates. These include usage of fast function approximation to find potentially strong samples, as well as restarts from local minima. Results show that these methods improve performance and that total travel distance can be reduced by as much as 30% within 8 hours of CPU-time. We share a public repository with SLAP instances and corresponding benchmark results on the generalizable TSPLIB format.

Using a regular language as a pattern for string matching is nowadays a common -and sometimes unsafe- operation, provided as a built-in feature by most programming languages. A proper constraint solver over string variables should support most of the operations over regular expressions and related constructs. However, state-of-the-art string solvers natively support only the membership relation of a string variable to a regular language. Here we take a step forward by defining a specialised propagator for the match operation, returning the leftmost position where a pattern can match a given string. Empirical evidences show the effectiveness of our approach, implemented within the constraint programming framework, and tested against state-of-the-art string solvers.

Dynamically typed programming languages are popular in education and the software industry. While presenting a low barrier to entry, they suffer from runtime 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 actual 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.

Current approaches for real-world Multi-Agent Path Finding (MAPF) usually start with a simplified MAPF model and modify the resulting plans so they are kinematically feasible. We investigate one such problem, called MAPF with turn actions MAPF_T, and show that ignoring the kinematic constraints significantly increases solution cost. A first modification of the popular Conflict-Based Search algorithm to MAPF_T yields significantly better plans but comes at the cost of substantial decreases in scalability. We then introduce several techniques that can improve the performance of CBS for MAPF_T, including stronger and generalised versions of existing symmetry-breaking constraints and a novel pruning technique that eliminates redundant branches in the CBS constraint tree. Experimental results on six popular MAPF domains show convincing improvements for CBS success rate and substantial reductions in node expansions and runtime.

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.

The tendency of an amino acid to adopt certain configurations in folded proteins is treated here as a statistical estimation problem. We model the joint distribution of the observed mainchain and sidechain dihedral angles (〈ϕ,ψ,χ1,χ2,…〉) of any amino acid by a mixture of a product of von Mises probability distributions. This mixture model maps any vector of dihedral angles to a point on a multi-dimensional torus. The continuous space it uses to specify the dihedral angles provides an alternative to the commonly used rotamer libraries. These rotamer libraries discretize the space of dihedral angles into coarse angular bins, and cluster combinations of sidechain dihedral angles (〈χ1,χ2,…〉) as a function of backbone 〈ϕ,ψ〉 conformations. A 'good' model is one that is both concise and explains (compresses) observed data. Competing models can be compared directly and in particular our model is shown to outperform the Dunbrack rotamer library in terms of model complexity (by three orders of magnitude) and its fidelity (on average 20% more compression) when losslessly explaining the observed dihedral angle data across experimental resolutions of structures. Our method is unsupervised (with parameters estimated automatically) and uses information theory to determine the optimal complexity of the statistical model, thus avoiding under/over-fitting, a common pitfall in model selection problems. Our models are computationally inexpensive to sample from and are geared to support a number of downstream studies, ranging from experimental structure refinement, de novo protein design, and protein structure prediction. We call our collection of mixture models as PhiSiCal (ϕψχal). AVAILABILITY AND IMPLEMENTATION: PhiSiCal mixture models and programs to sample from them are available for download at http://lcb.infotech.monash.edu.au/phisical.

Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking of concurrent programs to avoid the exploration of equivalent execution sequences. In order to detect equivalence, DPOR relies on the notion of independence between execution steps. As this notion must be approximated, it can lose precision and thus treat execution steps as interfering when they are not. Our work is inspired by recent progress in the area that has introduced more accurate ways to exploit conditional notions of independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p⋅t and t⋅p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. This article introduces a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. The implementation of our algorithm has been undertaken within the Nidhugg model checking tool. Our experimental evaluation, using benchmarks from the previous works, shows that our algorithm is able to effectively combine the benefits of both context-sensitive and observers-based independence and that it can produce exponential reductions over both of them.

Multi-Agent Path Finding (MAPF) is the problem of planning collision-free paths for multiple agents in a shared environment. In this paper, we propose a novel algorithm MAPF-LNS2 based on large neighborhood search for solving MAPF efficiently. Starting from a set of paths that contain collisions, MAPF-LNS2 repeatedly selects a subset of colliding agents and replans their paths to reduce the number of collisions until the paths become collision-free. We compare MAPF-LNS2 against a variety of state-of-the-art MAPF algorithms, including Prioritized Planning with random restarts, EECBS, and PPS, and show that MAPF-LNS2 runs significantly faster than them while still providing near-optimal solutions in most cases. MAPF-LNS2 solves 80% of the random-scenario instances with the largest number of agents from the MAPF benchmark suite with a runtime limit of just 5 minutes, which, to our knowledge, has not been achieved by any existing algorithms.

Multi-Agent Path Finding (MAPF) is the problem of finding collision-free paths for multiple agents that minimize the sum of path costs. EECBS is a leading two-level algorithm that solves MAPF bounded-suboptimally, that is, within some factor w of the minimum sum of path costs C*. It uses focal search to find bounded-suboptimal paths on the low level and Explicit Estimation Search (EES) to resolve collisions on the high level. EES keeps track of a lower bound LB on C* to find paths whose sum of path costs is at most w LB in order to solve MAPF bounded-suboptimally. However, the costs of many paths are often much smaller than w times their minimum path costs, meaning that the sum of path costs is much smaller than w C*. In this paper, we therefore propose Flexible EECBS (FEECBS), which uses a flex(ible) distribution of the path costs (that relaxes the requirement to find bounded-suboptimal paths on the low level) in order to reduce the number of collisions that need to be resolved on the high level while still guaranteeing to solve MAPF bounded suboptimally. We address the drawbacks of flex distribution via techniques such as restrictions on the flex distribution, restarts of the high-level search with EECBS, and low-level focal-A* search. Our empirical evaluation shows that FEECBS substantially improves the efficiency of EECBS on MAPF instances with large maps and large numbers of agents.

The predict+optimize problem combines machine learning and combinatorial optimization by predicting the problem coefficients first and then using these coefficients to solve the optimization problem. While this problem can be solved in two separate stages, recent research shows end to end models can achieve better results. This requires differentiating through a discrete combinatorial function. Models that use differentiable surrogates are prone to approximation errors, while existing exact models are limited to dynamic programming, or they do not generalize well with scarce data. In this work we propose a novel divide and conquer algorithm based on transition points to reason over exact optimization problems and predict the coefficients using the optimization loss. Moreover, our model is not limited to dynamic programming problems. We also introduce a greedy version, which achieves similar results with less computation. In comparison with other predict+optimize frameworks, we show our method outperforms existing exact frameworks and can reason over hard combinatorial problems better than surrogate methods.

Tree ensembles (TEs) denote a prevalent machine learning model that do not offer guarantees of interpretability, that represent a challenge from the perspective of explainable artificial intelligence. Besides model agnostic approaches, recent work proposed to explain TEs with formally-defined explanations, which are computed with oracles for propositional satisfiability (SAT) and satisfiability modulo theories. The computation of explanations for TEs involves linear constraints to express the prediction. In practice, this deteriorates scalability of the underlying reasoners. Motivated by the inherent propositional nature of TEs, this paper proposes to circumvent the need for linear constraints and instead employ an optimization engine for pure propositional logic to efficiently handle the prediction. Concretely, the paper proposes to use a MaxSAT solver and exploit the objective function to determine a winning class. This is achieved by devising a propositional encoding for computing explanations of TEs. Furthermore, the paper proposes additional heuristics to improve the underlying MaxSAT solving procedure. Experimental results obtained on a wide range of publicly available datasets demonstrate that the proposed MaxSAT-based approach is either on par or outperforms the existing reasoning-based explainers, thus representing a robust and efficient alternative for computing formal explanations for TEs.

In optimisation problems involving multiple agents (stakeholders) we often want to make sure that the solution is balanced and fair. That is, we want to maximise total utility subject to an upper bound on the statistical dispersion (e.g., spread or the Gini coefficient) of the utility given to different agents, or minimise dispersion subject to some lower bounds on utility. These needs arise in, for example, balancing tardiness in scheduling, unwanted shifts in rostering, and desired resources in resource allocation, or minimising deviation from a baseline in schedule repair, to name a few. These problems are often quite challenging. To solve them efficiently we want to effectively reason about dispersion. Previous work has studied the case where the mean is fixed, but this may not be possible for many problems, e.g., scheduling where total utility depends on the final schedule. In this paper we introduce two log-linear-time dispersion propagators – (a) spread (variance, and indirectly standard deviation) and (b) the Gini coefficient – capable of explaining their propagations, thus allowing effective clause learning solvers to be applied to these problems. Propagators for (a) exist in the literature but do not explain themselves, while propagators for (b) have not been previously studied. We avoid introducing floating-point variables, which are usually not supported by learning solvers, by reasoning about scaled, integer versions of the constraints. We show through experimentation that clause learning can substantially improve the solving of problems where we want to bound dispersion and optimise total utility and vice versa.

Multi-Train Path Finding (MTPF) is a coordination problem that asks us to plan collision-free paths for a team of moving agents, where each agent occupies a sequence of locations at any given time. MTPF is useful for planning a range of real-world vehicles, including rail trains and road convoys. MTPF is closely related to another coordination problem known as k-Robust Multi-Agent Path Finding (kR-MAPF). Although similar in principle, the performance of optimal MTPF algorithms in practice lags far behind that of optimal kR-MAPF algorithms. In this work, we revisit the connection between them and reduce the performance gap. First, we show that, in many cases, a valid kR-MAPF plan is also a valid MTPF plan, which leads to a new and faster approach for collision resolution. We also show that many recently introduced improvements for kR-MAPF, such as lower-bounding heuristics and symmetry reasoning, can be extended to MTPF. Finally, we explore a new type of pairwise symmetry specific to MTPF. Our experiments show that these improvements yield large efficiency gains for optimal MTPF.

The Euclidean Shortest Path Problem (ESPP) asks us to find a minimum length path between two points on a 2D plane while avoiding a set of polygonal obstacles. Existing approaches for ESPP, based on Dijkstra or A* search, are primal methods that gradually build up longer and longer valid paths until they reach the target. In this paper we define an alternative algorithm for ESPP which can avoid this problem. Our approach starts from a path that ignores all obstacles, and generates longer and longer paths, each avoiding more obstacles, until eventually the search finds an optimal valid path.

MOTIVATION: Alignments are correspondences between sequences. How reliable are alignments of amino acid sequences of proteins, and what inferences about protein relationships can be drawn? Using techniques not previously applied to these questions, by weighting every possible sequence alignment by its posterior probability we derive a formal mathematical expectation, and develop an efficient algorithm for computation of the distance between alternative alignments allowing quantitative comparisons of sequence-based alignments with corresponding reference structure alignments. RESULTS: By analyzing the sequences and structures of 1 million protein domain pairs, we report the variation of the expected distance between sequence-based and structure-based alignments, as a function of (Markov time of) sequence divergence. Our results clearly demarcate the 'daylight', 'twilight' and 'midnight' zones for interpreting residue-residue correspondences from sequence information alone. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

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 use of optimal decision trees.

Conflict-Based Search (CBS) is a leading two-level algorithm for optimal Multi-Agent Path Finding (MAPF). The main step of CBS is to expand nodes by resolving conflicts (where two agents collide). Choosing the ‘right’ conflict to resolve can greatly speed up the search. CBS first resolves conflicts where the costs (g-values) of the resulting child nodes are larger than the cost of the node to be split. However, the recent addition of high-level heuristics to CBS and expanding nodes according to f=g+h reduces the relevance of this conflict prioritization method. Therefore, we introduce an expanded categorization of conflicts, which first resolves conflicts where the f-values of the child nodes are larger than the f-value of the node to be split, and present a method for identifying such conflicts. We also enhance all known heuristics for CBS by using information about the cost of resolving certain conflicts, and with only a small computational overhead. Finally, we experimentally demonstrate that both the expanded categorization of conflicts and the improved heuristics contribute to making CBS even more efficient.

During Multi-Agent Path Finding (MAPF) problems, agentscan be delayed by unexpected events. To address suchsituations recent work describes k-Robust Conflict-BasedSearch (k-CBS): an algorithm that produces coordinated andcollision-free plan that is robust for up tokdelays. In thiswork we introducing a variety of pairwise symmetry break-ing constraints, specific tok-robust planning, that can effi-ciently find compatible and optimal paths for pairs of con-flicting agents. We give a thorough description of the newconstraints and report large improvements to success rate ina range of domains including: (i) classic MAPF benchmarks;(ii) automated warehouse domains and; (iii) on maps fromthe 2019 Flatland Challenge, a recently introduced railwaydomain wherek-robust planning can be fruitfully applied toschedule trains.

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.

Core-guided techniques have revolutionized Boolean satisfiability approaches to optimization problems (MaxSAT), but the process at the heart of these methods, strengthening bounds on solutions by repeatedly adding cardinality constraints, remains a bottleneck. Cardinality constraints require significant work to be re-encoded to SAT, and SAT solvers are notoriously weak at cardinality reasoning. In this work, we lift core-guided search to pseudo-Boolean (PB) solvers, which deal with more general PB optimization problems and operate natively with cardinality constraints. The cutting planes method used in such solvers allows us to derive stronger cardinality constraints, which yield better updates to solution bounds, and the increased efficiency of objective function reformulation also makes it feasible to switch repeatedly between lower-bounding and upper- bounding search. A thorough evaluation on applied and crafted benchmarks shows that our core-guided PB solver significantly improves on the state of the art in pseudo-Boolean optimization.

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.

This paper presents a framework to characterize and identify local sequences of proteins that are statistically redundant under the measure of Shannon information content while accounting for variations in their occurrences over evolutionary insertions, deletions, and substitutions of amino acids. The identification of such local sequences provides insights for downstream studies on proteins. Here, we have applied our methods to amino acid sequence data sets derived from a database corresponding to 935,552 substructural regions of varying sizes, covering 113,724 proteins from the protein data bank. The results identify, among others, a surjective mapping between 110,598 local sequences (with an average length of 82 amino acids per sequence) and 1,493 topological shapes. The C++ source code and supporting material are available from https://lcb.infotech.monash.edu.au/bibm2021.

We study the problem of training a roster of engineers, who are scheduled to respond to service calls that require a set of skills, and where engineers and calls have different locations. Both training an engineer in a skill and sending an engineer to respond a non-local service call incur a cost. Alternatively, a local contractor can be hired. The problem consists in training engineers in skills so that the quality of service (i.e. response time) is maximised and costs are minimised. The problem is hard to solve in practice partly because (1) the value of training an engineer in one skill depends on other training decisions, (2) evaluating training decisions means evaluating the schedules that are now made possible by the new skills, and (3) these schedules must be computed over a long time horizon, otherwise training may not pay off. We show that a monolithic approach to this problem is not practical. Instead, we decompose it into three subproblems, modelled with MiniZinc. This allows us to pick the approach that works best for each subproblem (MIP or CP) and provide good solutions to the problem. Data is provided by a multinational company.

Multi-Agent Path Finding (MAPF) is the challenging problem of computing collision-free paths for multiple agents. Algorithms for solving MAPF can be categorized on a spectrum. At one end are (bounded-sub)optimal algorithms that can find high-quality solutions for small problems. At the other end are unbounded-suboptimal algorithms that can solve large problems but usually find low-quality solutions. In this paper, we consider a third approach that combines the best of both worlds: anytime algorithms that quickly find an initial solution using efficient MAPF algorithms from the literature, even for large problems, and that subsequently improve the solution quality to near-optimal as time progresses by replanning subgroups of agents using Large Neighborhood Search. We compare our algorithm MAPF-LNS against a range of existing work and report significant gains in scalability, runtime to the initial solution, and speed of improving the solution.

Artificial Intelligence (AI) is widely used in decision making procedures in myriads of real-world applications across important practical areas such as finance, healthcare, education, and safety critical systems. Due to its ubiquitous use in safety and privacy critical domains, it is often vital to understand the reasoning behind the AI decisions, which motivates the need for explainable AI (XAI). One of the major approaches to XAI is represented by computing so-called interpretable machine learning (ML) models, such as decision trees (DT), decision lists (DL) and decision sets (DS). These models build on the use of if-then rules and are thus deemed to be easily understandable by humans. A number of approaches have been proposed in the recent past to devising all kinds of interpretable ML models, the most prominent of which involve encoding the problem into a logic formalism, which is then tackled by invoking a reasoning or discrete optimization procedure. This paper overviews the recent advances of the reasoning and constraints based approaches to learning interpretable ML models and discusses their advantages and limitations.

Multi-Agent Path Finding (MAPF) is the combinatorial problem of finding collision-free paths for multiple agents on a graph. This paper describes MAPF-based software for solving train planning and replanning problems on large-scale railway networks under uncertainty. The software recently won the 2020 Flatland Challenge, a NeurIPS competition trying to determine how to efficiently manage dense traffic on rail networks. The software incorporates many state-of-the-art MAPF, or in general, optimization technologies, such as prioritized planning, large neighborhood search, safe interval path planning, minimum communication policies, parallel computing, and simulated annealing. It can plan collision-free paths for thousands of trains within a few minutes and deliver deadlock-free actions in real-time during execution.

Conflict-Based Search (CBS) is a leading two-level algorithm for optimal Multi-Agent Path Finding (MAPF). At its high level, CBS expands nodes by resolving conflicts. In recent years, admissible heuristics were added to the high level of CBS. We enhance all known heuristic functions for CBS by using information about the cost of resolving certain conflicts, with only a small computational overhead. We experimentally demonstrate that the improved heuristics contribute to making CBS even more efficient.

Multi-Agent Path Finding (MAPF) is the problem of finding collision-free paths for multiple agents. CBS is a leading optimal two-level MAPF solver whose low level plans optimal paths for single agents and whose high level runs a best-first search on a Constraint Tree (CT) to resolve the collisions between the paths. ECBS, a bounded-suboptimal variant of CBS, speeds up CBS by reducing the number of collisions that need to be resolved on the high level. It achieves this by generating bounded-suboptimal paths with fewer collisions with the paths of the other agents on the low level and expanding bounded-suboptimal CT nodes that contain fewer collisions on the high level. In this paper, we propose Flexible ECBS (FECBS) that further reduces the number of collisions that need to be resolved on the high level by using looser suboptimal bounds on the low level while still providing bounded-suboptimal solutions. Instead of requiring the cost of each path to be bounded-suboptimal, FECBS requires only the overall cost of the paths to be bounded-suboptimal, which gives us the freedom to distribute the cost leeway among different agents according to their needs. Our empirical results show that FECBS can solve more MAPF instances than state-of-the-art ECBS variants within 5 minutes.

The shortest path problem (SPP) asks us to find a minimum length path between two points, usually on a graph. In a Euclidean environment the points are in a 2D plane and here the path must avoid a set of polygonal obstacles. Solution methods for this Euclidean SPP (ESPP) typically convert the continuous 2D map into a discretised representation, like a graph or navigation mesh. RayScan is a recent and fast ESPP algorithm which avoids the preprocessing step by using a combination of "ray shooting" and polygon scanning. In this paper we improve the performance of RayScan using spatial reasoning and ray caching techniques. We also extend the algorithm, from single-target search to a multi-target setting. Comparative game map experiments show a substantial speedup.

We consider the design and implementation of a centralised oracle that provides commuters with customised and congestion-aware driving directions. Computing directions for a single journey is straightforward, but doing so at city-scale, in real-time, and under changing conditions is extremely challenging. In this work we describe a new type of centralised oracle which combines fast database-driven path planning with a query management system that distributes work across a small commodity cluster of networked machines. Our system allows large-scale changes to the underlying graph metric, from one query to the next, and it supports a variety of query types including optimal, bounded suboptimal, time-budgeted and k-prefix. Simulated experiments show strong results: we can provide real-time routing for all peak-hour commuter trips in the city of Melbourne, Australia.

Decision sets and decision lists are two of the most easily explainable machine learning models. Given the renewed emphasis on explainable machine learning decisions, both of these machine learning models are becoming increasingly attractive, as they combine small size and clear explainability. In this paper, we define size as the total number of literals in the SAT encoding of these rule-based models as opposed to earlier work that concentrates on the number of rules. In this paper, we develop approaches to computing minimum-size “perfect” decision sets and decision lists, which are perfectly accurate on the training data, and minimal in size, making use of modern SAT solving technology. We also provide a new method for determining optimal sparse alternatives, which trade off size and accuracy. The experiments in this paper demonstrate that the optimal decision sets computed by the SAT-based approach are comparable with the best heuristic methods, but much more succinct, and thus, more explainable. 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. Finally, we examine the size of average explanations generated by decision sets and decision lists.

Zones and Octagons are popular abstract domains for static program analysis. They enable the automated discovery of simple numerical relations that hold between pairs of program variables. Both domains are well understood mathematically but the detailed implementation of static analyses based on these domains poses many interesting algorithmic challenges. In this article, we study the two abstract domains, their implementation and use. Utilizing improved data structures and algorithms for the manipulation of graphs that represent difference-bound constraints, we present fast implementations of both abstract domains, built around a common infrastructure. We compare the performance of these implementations against alternative approaches offering the same precision. We quantify the differences in performance by measuring their speed and precision on standard benchmarks. We also assess, in the context of software verification, the extent to which the improved precision translates to better verification outcomes. Experiments demonstrate that our new implementations improve the state of the art for both Zones and Octagons significantly.

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 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.

Mistakes made by humans, or machines, commonly arise when managing ballots cast in an election. In the 2013 Australian Federal Election, for example, 1,370 West Australian Senate ballots were lost, eventually leading to a costly re-run of the election. Other mistakes include ballots that are misrecorded by electronic voting systems, voters that cast invalid ballots, or vote multiple times at different polling locations. We present a method for assessing whether such problems could have made a difference to the outcome of a Single Transferable Vote (STV) election – a complex system of preferential voting for multi-seat elections. It is used widely in Australia, in Ireland, and in a range of local government elections in the United Kingdom and United States.

The paper presents the pedagogical innovations and experience of the co-development of three MOOCs on the subject of “Modeling and Solving Discrete Optimization Problems” by two universities. In a nutshell, the MOOCs feature the Fable-Based Learning approach, which is a form of problem-based learning encapsulated in a coherent story plot. Each lecture video begins with an animation that tells a story following a novel. The protagonists of the story encounter a problem requiring technical assistance from the two professors from modern time via a magical tablet granted to them by a fairy god. The new pedagogy aims at increasing learners' motivation and interests as well as situating the learners in a coherent learning context. In addition to scriptwriting, animation production and situating the teaching materials in the story plot, another challenge of the project is the remote distance between the two institutions as well as the need to produce all teaching materials in both (Mandarin) Chinese and English to cater for different geographic learning needs. The MOOCs have been running recurrently on Coursera since 2017. We present learner statistics and feedback, and discuss our experience with and preliminary observations of adopting the online materials in a Flipped Classroom setting.

We study the predict+optimise problem, where machine learning and combinatorial optimisation must interact to achieve a common goal. These problems are important when optimisation needs to be performed on input parameters that are not fully observed but must instead be estimated using machine learning. We provide a novel learning technique for predict+optimise to directly reason about the underlying combinatorial optimisation problem, offering a meaningful integration of machine learning and optimisation. This is done by representing the combinatorial problem as a piecewise linear function parameterised by the coefficients of the learning model and then iteratively performing coordinate descent on the learning coefficients. Our approach is applicable to linear learning functions and any optimisation problem solvable by dynamic programming. We illustrate the effectiveness of our approach on benchmarks from the literature.

Many optimisation problems are of an online—also called dynamic—nature, where new information is expected to arrive and the problem must be resolved in an ongoing fashion to (a) improve or revise previous decisions and (b) take new ones. Typically, building an online decision-making system requires substantial ad-hoc coding to ensure the offline version of the optimisation problem is continually adjusted and resolved. This paper defines a general framework for automatically solving online optimisation problems. This is achieved by extending a model of the offline optimisation problem, from which an online version is automatically constructed, thus requiring no further modelling effort. In doing so, it formalises many of the aspects that arise in online optimisation problems. The same framework can be applied for automatically creating sliding-window solving approaches for problems that have a large time horizon. Experiments show we can automatically create efficient online and sliding-window solutions to optimisation problems.

For many combinatorial problems, finding a single solution is not enough. This is clearly the case for multi-objective optimization problems, as they have no single “best solution” and, thus, it is useful to find a representation of the non-dominated solutions (the Pareto frontier). However, it also applies to single objective optimization problems, where one may be interested in finding several (close to) optimal solutions that illustrate some form of diversity. The same applies to satisfaction problems. This is because models usually idealize the problem in some way, and a diverse pool of solutions may provide a better choice with respect to considerations that are omitted or simplified in the model. This paper describes a general framework for finding k diverse solutions to a combinatorial problem (be it satisfaction, single-objective or multi-objective), various approaches to solve problems in the framework, their implementations, and an experimental evaluation of their practicality.

Combinatorial optimization assumes that all parameters of the optimization problem, e.g. the weights in the objective function, are 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 warm-starting 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 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.

The computation of string similarity measures has been thoroughly studied in the scientific literature and has applications in a wide variety of different areas. One of the most widely used measures is the so called string edit distance which captures the number of required edit operations to transform a string into another given string. Although polynomial time algorithms are known for calculating the edit distance between two strings, there also exist NP-hard problems from practical applications like scheduling or computational biology that constrain the minimum edit distance between arrays of decision variables. In this work, we propose a novel global constraint to formulate restrictions on the minimum edit distance for such problems. Furthermore, we describe a propagation algorithm and investigate an explanation strategy for an edit distance constraint propagator that can be incorporated into state of the art lazy clause generation solvers. Experimental results show that the proposed propagator is able to significantly improve the performance of existing exact methods regarding solution quality and computation speed for benchmark problems from the literature.

String constraint solving is an important emerging field, given the ubiquity of strings over different fields such as formal analysis, automated testing, database query processing, and cybersecurity. This paper highlights the current state-of-the-art for string constraint solving, and identifies future challenges in this field.

Conflict-Based Search (CBS) is a leading algorithm for optimal Multi-Agent Path Finding (MAPF). CBS variants typically compute MAPF solutions using some form of A* search. However, they often do so under strict time limits so as to avoid exhausting the available memory. In this paper, we present IDCBS, an iterative-deepening variant of CBS which can be executed without exhausting the memory and without strict time limits. IDCBS can be substantially faster than CBS due to incremental methods that it uses when processing CBS nodes.

We consider optimal and anytime algorithms for the Euclidean Shortest Path Problem (ESPP) in two dimensions. Our approach leverages ideas from two recent works: Polyanya, a mesh-based ESPP planner which we use to represent and reason about the environment, and Compressed Path Databases, a speedup technique for pathfinding on grids and spatial networks, which we exploit to compute fast candidate paths. In a range of experiments and empirical comparisons we show that: (i) the auxiliary data structures required by the new method are cheap to build and store; (ii) for optimal search, the new algorithm is faster than a range of recent ESPP planners, with speedups ranging from several factors to over one order of magnitude; (iii) for anytime search, where feasible solutions are needed fast, we report even better runtimes.

Blockmodelling is an important technique in social network analysis for discovering the latent structures and groupings in graphs. State-of-the-art approaches approximate the graph using matrix factorisation, which can discover both the latent graph structures and vertex groupings. However, factorisation is a one-way approximation, in that it only approximates the graph with a lossy model that removes the background noise. Traditional Blockmodelling methods rely on an alternating 2-step optimization that involves iteratively updating the matrix representing membership while fixing the matrix representing the graph's underlying structure, and then updating the structure matrix while keeping the membership matrix fixed. We propose a single step optimization method, which uses algebraic simplifi-cation to directly update the lower dimensional, latent structure representation. This helps improve both the convergence and accuracy of blockmodelling. We also show that this approach can solve multi-view blockmodelling problems, involving multiple graphs over the same vertices. We use real datasets to show that our approach has much higher accuracy and comparable running times to competing approaches.

We consider two new types of pairwise path symmetries which appear in the context of Multi-Agent Path Finding (MAPF). The first of them, corridor symmetry, arises when two agents attempt to pass through the same narrow passage but in opposite directions. The second, target symmetry, arises when the shortest path of one agent requires the target location of a second agent after the second agent has already arrived. These symmetries can produce an exponential blowup in the space of possible collision resolutions, leading to timeout failure even for state-of-the-art algorithms such as Conflict-Based Search. We propose to break symmetries using new reasoning techniques that: (1) detect each type of situation and, (2) resolve them by introducing specialized constraints. We implement our ideas in the context of Conflict-Based Search where, in a range of experiments, we report up to an order-of-magnitude improvement in runtime performance and, in some cases, more than a doubling in success rate.

Conflict-Based Search (CBS) is a leading algorithm for optimal Multi-Agent Path Finding (MAPF) which features strong performance. In CBS, one conflict in a high-level node is resolved to generate two child nodes, until a node with no conflicts is found. Choosing the right conflict to resolve can greatly speed up the search. It is currently recommended to resolve cardinal conflicts first, resolving them yields two child nodes with a higher cost than the cost of their parent. However, since the recent addition of high-level heuristics to CBS, when resolving cardinal conflicts, the h-value of high-level child nodes often decreases by the same amount as their cost increases. This diminishes the effectiveness of the cardinal conflicts distinction. We propose an expanded categorization of conflicts into f-cardinal, g-cardinal, and non-cardinal. F-cardinal conflicts should be resolved first. Resolving f-cardinal conflicts generates child nodes with an increased f-value relative to their parent. We propose two methods for identifying f-cardinal conflicts. Finally, we demonstrate on standard benchmarks that choosing conflicts according to this expanded categorization increases the effectiveness of modern CBS.

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.

We describe a new way of reasoning about symmetric collisions for Multi-Agent Path Finding (MAPF) on 4-neighbor grids. We also introduce a symmetry-breaking constraint to resolve these conflicts. This specialized technique allows us to identify and eliminate, in a single step, all permutations of two currently assigned but incompatible paths. Each such permutation has exactly the same cost as a current path, and each one results in a new collision between the same two agents. We show that the addition of symmetry-breaking techniques can lead to an exponential reduction in the size of the search space of CBS, a popular framework for MAPF, and report significant improvements in both runtime and success rate versus CBSH and EPEA* – two recent and state-of-the-art MAPF algorithms.

Reasoning about floating-point numbers is notoriously difficult, owing to the lack of convenient algebraic properties such as associativity. This poses a substantial challenge for program analysis and verification tools which rely on precise floating-point constraint solving. Currently, interval methods in this domain often exhibit slow convergence even on simple examples. We present a new theorem supporting efficient computation of exact bounds of the intersection of a rectangle with the preimage of an interval under floating-point addition, in any radix or rounding mode. We thus give an efficient method of deducing optimal bounds on the components of an addition, solving the convergence problem.

Compressed Path Databases (CPDs) are a leading technique for optimal pathfinding in graphs with static edge costs. In this work we investigate CPDs as admissible heuristic functions and we apply them in two distinct settings: problems where the graph is subject to dynamically changing costs, and anytime settings where deliberation time is limited. Conventional heuristics derive cost-to-go estimates by reasoning about a tentative and usually infeasible path, from the current node to the target. CPD-based heuristics derive cost-to-go estimates by computing a concrete and usually feasible path. We exploit such paths to bound the optimal solution, not just from below but also from above. We demonstrate the benefit of this approach in a range of experiments on standard gridmaps and in comparison to Landmarks, a popular alternative also developed for searching in explicit state-spaces.

We study the predict+optimise problem, where machine learning and combinatorial optimisation must interact to achieve a common goal. These problems are important when optimisation needs to be performed on input parameters that are not fully observed but must instead be estimated using machine learning. Our contributions are two-fold: 1) we provide theoretical insight into the properties and computational complexity of predict+optimise problems in general, and 2) develop a novel framework that, in contrast to related work, guarantees to compute the optimal parameters for a linear learning function given any ranking optimisation problem. We illustrate the applicability of our framework for the particular case of the unit-weighted knapsack predict+optimise problem and evaluate on benchmarks from the literature.

In this paper, we define Jump Point Graphs (JP), a preprocessing-based path-planning technique similar to Subgoal Graphs (SG). JP allows for the first time the combination of Jump Point Search style pruning in the context of abstraction-based speedup techniques, such as Contraction Hierarchies. We compare JP with SG and its variants and report new state-of-the-art results for grid-based pathfinding.

There are currently two broad strategies for optimal Multi-agent Pathfinding (MAPF): (1) search-based methods, which model and solve MAPF directly, and (2) compilation-based solvers, which reduce MAPF to instances of well-known combinatorial problems, and thus, can benefit from advances in solver techniques. In this work, we present an optimal algorithm, BCP, that hybridizes both approaches using Branch-and-Cut-and-Price, a decomposition framework developed for mathematical optimization. We formalize BCP and compare it empirically against CBSH and CBSH-RM, two leading search-based solvers. Conclusive results on standard benchmarks indicate that its performance exceeds the state-of-the-art: solving more instances on smaller grids and scaling reliably to 100 or more agents on larger game maps.

Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking to avoid the exploration of equivalent execution sequences. DPOR relies on the notion of independence between execution steps to detect equivalence. Recent progress in the area has introduced more accurate ways to detect independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p · t and t · p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. We introduce a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. Experimental evaluation shows that our gains increase exponentially with the size of the considered inputs.

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. This paper was published at AAAI 2019.

We describe a new way of reasoning about symmetric collisions for Multi-Agent Path Finding (MAPF) on 4-neighbor grids. We also introduce a symmetry-breaking constraint to resolve these conflicts. This specialized technique allows us to identify and eliminate, in a single step, all permutations of two currently assigned but incompatible paths. Each such permutation has exactly the same cost as a current path, and each one results in a new collision between the same two agents. We show that the addition of symmetry-breaking techniques can lead to an exponential reduction in the size of the search space of CBS, a popular framework for MAPF, and report significant improvements in both runtime and success rate versus CBSH and EPEA* – two recent and state-of-the-art MAPF algorithms.

The single transferable vote (STV) is a system of preferential voting for multiseat elections. Each ballot 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 ballot manipulations (changes, additions, and deletions) required to bring about a change in the set of elected candidates. Knowing the MOV gives insight into how much time and money should be spent on auditing 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. 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.

Solving constraints over strings is an emerging important field. Recently, a Constraint Programming approach based on dashed strings has been proposed to enable a compact domain representation for potentially large bounded-length string variables. In this paper, we present a more efficient algorithm for propagating equality (and related constraints) over dashed strings. We call this propagation sweep-based. Experimental evidences show that sweep-based propagation is able to significantly outperform state-of-the-art approaches for string constraint solving.

Semi-supervised or constrained community detection incorporates side information to findcommunities of interest in complex networks. The supervision is often represented as constraints such as known labels and pairwise constraints. Existing constrained community detection approaches often fail to fully benefit from the available side information. This results in poor performance for scenarios such as: when the constraints are required to be fully satisfied, when there is a high confidence about the correctness of the supervision information, and in situations where the side information is expensive or hard to achieve and is only available in a limited amount. In this paper, we propose a new constrained community detection algorithm based on Lagrangian multipliers to incorporate and fully satisfy the instance level supervisio nconstraints. Our proposed algorithm can more fully utilise available side information and find better quality solutions. Our experiments on real and synthetic data sets show our proposed LagCCD algorithm outperforms existing algorithms in terms of solution quality, ability to satisfy the constraints and noise resistance.

We present the first practical Integer Linear Programming model for Sankey Diagram layout. We show that this approach is viable in terms of running time for reasonably complex diagrams and also that the quality of the layout is measurably and visibly better than heuristic approaches in terms of crossing reduction. Finally, we demonstrate that the model is easily extensible through the addition of constraints, such as arbitrary grouping of nodes.

The aim of solver-independent modelling is to create a model of a satisfaction or optimisation problem independent of a particular technology. This avoids early commitment to a solving technology and allows easy comparison of technologies. MiniZinc is a solver-independent modelling language, supported by CP, MIP, SAT, SMT, and constraint-based local search (CBLS) backends. Some technologies, in particular CP and CBLS, require not only a model but also a search strategy. While backends for these technologies offer default search strategies, it is often beneficial to include in a model a user-specified search strategy for a particular technology, especially if the strategy can encapsulate knowledge about the problem structure. This is complex since a local-search strategy (comprising a neighbourhood, a heuristic, and a meta-heuristic) is often tightly tied to the model. Hence we wish to use the same language for specifying the model and the local search. We show how to extend MiniZinc so that one can attach a fully declarative neighbourhood specification to a model, while maintaining the solver-independence of the language. We explain how to integrate a model-specific declarative neighbourhood with an existing CBLS backend for MiniZinc.

The problem of integrating heterogeneous data sources into an ontology is highly relevant in the database field. Several techniques exist to approach the problem, but side constraints on the data cannot be easily implemented and thus the results may be inconsistent. In this paper we improve previous work by Taheriyan et al. [2016a] using Machine Learning (ML) to take into account inconsistencies in the data (unmatchable attributes) and encode the problem as a variation of the Steiner Tree, for which we use work by De Uña et al. [2016] in Constraint Programming (CP). Combining ML and CP achieves state-of-the-art precision, recall and speed, and provides a more flexible framework for variations of the problem.

Blockmodelling is an important technique for detecting underlying patterns in graphs. However, existing blockmodelling algorithms do not provide the user with any explicit control to specify which patterns might be of interest. Furthermore, existing algorithms focus on finding standard community structures in graphs, and are likely to overlook informative but more complex patterns, such as hierarchical or ring blockmodel structures. In this paper, we propose a generic constraint programming framework for blockmodelling, which allows a user to specify and search for complex blockmodel patterns in graphs. Our proposed framework can be incorporated into existing iterative blockmodelling algorithms, operating as a hybrid optimization scheme that provides high flexibility and expressiveness. We demonstrate the power of our framework for discovering complex patterns, via experiments over a range of synthetic and real data sets.

Contraction hierarchies are graph-based data structure developed to speed up shortest path search in road networks. Built during an offline pre-processing step, contraction hierarchies are always paired with an online query algorithm which is a variation on bi-directional Dijkstra search. Though effective and highly popular this combination can sometimes be difficult to extend, for example in order to leverage goal-directed heuristics or other forward-driven pruning techniques. In this paper we deconstruct the bi-directional query algorithm of contraction hierarchies and derive a new algorithmic schema which is compatible with standard uni-directional or bi-directional search. We then develop a variety of new uni-directional query algorithms to find optimal paths in contraction hierarchies. These are based on the combination of A* search and Geometric Containers, a well known and successful edge-pruning technique. Empirical results show that our approach can improve search times by an order of magnitude vs bi-directional Dijkstra, albeit at the cost of additional memory and pre-processing time.

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.

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 ofunsafeinitial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set ofsafeinitial 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.

Logic-based Benders decomposition (LBBD) is a powerful hybrid optimisation technique that can combine the strong dual bounds of mixed integer programming (MIP) with the combinatorial search strengths of constraint programming (CP). A major drawback of LBBD is that it is a far more involved process to implement an LBBD solution to a problem than the "model-and-run" approach provided by both CP and MIP. We propose an automated approach that accepts an arbitrary MiniZinc model and solves it using LBBD with no additional intervention on the part of the modeller. The design of this approach also reveals an interesting duality between LBBD and large neighborhood search (LNS). We compare our implementation of this approach to CP and MIP solvers on 4 different problem classes where LBBD has been applied before.

Computational analyses of the growing corpus of three-dimensional (3D) structures of proteins have revealed a limited set of recurrent substructural themes, termed super-secondary structures. Knowledge of super-secondary structures is important for the study of protein evolution and for the modeling of proteins with unknown structures. Characterizing a comprehensive dictionary of these super-secondary structures has been an unanswered computational challenge in protein structural studies. This paper presents an unsupervised method for learning such a comprehensive dictionary using the statistical framework of lossless compression on a database comprised of concise geometric representations of protein 3D folding patterns. The best dictionary is defined as the one that yields the most compression of the database. Here we describe the inference methodology and the statistical models used to estimate the encoding lengths. An interactive website for this dictionary is available at http://lcb.infotech.monash.edu.au/proteinConcepts/scop100/dictionary.html.

Motivation: Structural molecular biology depends crucially on computational techniques that compare protein three-dimensional structures and generate structural alignments (the assignment of one-to-one correspondences between subsets of amino acids based on atomic coordinates). Despite its importance, the structural alignment problem has not been formulated, much less solved, in a consistent and reliable way. To overcome these difficulties, we present here a statistical framework for the precise inference of structural alignments, built on the Bayesian and information-theoretic principle of Minimum Message Length (MML). The quality of any alignment is measured by its explanatory power-the amount of lossless compression achieved to explain the protein coordinates using that alignment. Results: We have implemented this approach in MMLigner , the first program able to infer statistically significant structural alignments. We also demonstrate the reliability of MMLigner 's alignment results when compared with the state of the art. Importantly, MMLigner can also discover different structural alignments of comparable quality, a challenging problem for oligomers and protein complexes. Availability and Implementation: Source code, binaries and an interactive web version are available at http://lcb.infotech.monash.edu.au/mmligner . Contact: [email protected]. Supplementary information: Supplementary data are available at Bioinformatics online.

The Steiner Tree Problem is a well know NP-complete problem that is well studied and for which fast algorithms are already available. Nonetheless, in the real world the Steiner Tree Problem is almost always accompanied by side constraints which means these approaches cannot be applied. For many problems with side constraints, only approximation algorithms are known. We introduce here a propagator for the tree constraint with explanations, as well as lower bounding techniques and a novel constraint programming approach for the Steiner Tree Problem and two of its variants. We find our propagators with explanations are highly advantageous when it comes to solving variants of this problem.

Computing the margin of victory (MOV) in an Instant Runoff Voting (IRV) election is NP-hard. In an IRV election with winning candidate w, the MOV defines the smallest number of cast votes that, if modified, result in the election of a candidate other than w. The ability to compute such margins has significant value. Arguments over the correctness of an election outcome usually rely on the size of the electoral margin. Risk-limiting audits use the size of this margin to determine how much post-election auditing is required. We present an efficient branch-and-bound algorithm for computing exact margins that substantially improves on the current best-known approach. Although exponential in the worst case, our algorithm runs efficiently in practice, computing margins in instances that could not be solved by the current state-of-the-art in a reasonable time frame.

Incorporating background knowledge in clustering problems has attracted wide interest. This knowledge can be represented as pairwise instance-level constraints. Existing techniques approach satisfaction of such constraints from a soft (discretionary) perspective, yet there exist scenarios for constrained clustering where satisfying as many constraints as possible. We present a new Lagrangian Constrained Clustering framework (LCC) for clustering in the presence of pairwise constraints which gives high priority to satisfying constraints. LCC is an iterative optimization procedure which incorporates dynamic penalties for violated constraints. Experiments show that LCC can outperform existing constrained clustering algorithms in scenarios which satisfying as many constraints as possible.

Model counting is the problem of computing the number of models that satisfy a given propositional theory. It has recently been applied to solving inference tasks in probabilistic logic programming, where the goal is to compute the probability of given queries being true provided a set of mutually independent random variables, a model (a logic program) and some evidence. The core of solving this inference task involves translating the logic program to a propositional theory and using a model counter. In this paper, we show that for some problems that involve inductive definitions like reachability in a graph, the translation of logic programs to SAT can be expensive for the purpose of solving inference tasks. For such problems, direct implementation of stable model semantics allows for more efficient solving. We present two implementation techniques, based on unfounded set detection, that extend a propositional model counter to a stable model counter. Our experiments show that for particular problems, our approach can outperform a state-of-the-art probabilistic logic programming solver by several orders of magnitude in terms of running time and space requirements, and can solve instances of significantly larger sizes on which the current solver runs out of time or memory.

Automatic layout of tables is useful in word processing applications and is required in online applications because of the need to tailor the layout to viewport width, choice of font, and dynamic content. However, if the table contains text, minimizing the height of the table for a given maximum width is a difficult combinatorial optimization problem because of the need to find the right choice of height/width configuration for each cell in the table. We investigate the modelling decisions involved in formulating this problem for use with standard combinatorial optimization techniques that are guaranteed to find the minimal-height table. To the best of our knowledge, we are the first to do so. We provide a detailed empirical evaluation of the resulting models using mixed integer programming and constraint programming with lazy clause generation.

Finding satisfying assignments for the variables involved in a set of constraints can be cast as a (bounded) model generation problem: search for (bounded) models of a theory in some logic. The state-of-the-art approach for bounded model generation for rich knowledge representation languages like ASP and FO(.) and a CSP modeling language such as Zinc, is ground-and-solve: reduce the theory to a ground or propositional one and apply a search algorithm to the resulting theory. An important bottleneck is the blow-up of the size of the theory caused by the grounding phase. Lazily grounding the theory during search is a way to overcome this bottleneck. We present a theoretical framework and an implementation in the context of the FO(.) knowledge representation language. Instead of grounding all parts of a theory, justifications are derived for some parts of it. Given a partial assignment for the grounded part of the theory and valid justifications for the formulas of the non-grounded part, the justifications provide a recipe to construct a complete assignment that satisfies the non-grounded part. When a justification for a particular formula becomes invalid during search, a new one is derived; if that fails, the formula is split in a part to be grounded and a part that can be justified. Experimental results illustrate the power and generality of this approach.

Abstract Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propose using logic programs as an intermediate program representation throughout the compilation process. With restrictions ensuring determinism and single-modedness, a logic program can easily be transformed to machine language or other low-level language, while maintaining the simple semantics that makes it suitable as a language for program analysis and transformation. We present a simple LP language that enforces determinism and single-modedness, and show that it makes a convenient program representation for analysis and transformation.

We consider the short-term production scheduling problem for a network of multiple open-pit mines and ports. Ore produced at each mine is transported by rail to a set of ports and blended into signature products for shipping. Consistency in the grade and quality of production over time is critical for customer satisfaction, whereas the maximal production of blended products is required to maximise profit. In practice, short-term schedules are formed independently at each mine, tasked with achieving the grade and quality targets outlined in a medium-term plan. However, 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. We present a decomposition-based heuristic for this short-term scheduling problem in which the grade and quality goals assigned to each mine are collaboratively adapted—ensuring the satisfaction of blending constraints at each port and exploiting opportunities to maximise production in the network that would otherwise be missed.

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.

The most commonly used integer types have fixed bit-width, making it possible for computations to “wrap around,” and many programs depend on this behaviour. Yet much work to date on program analysis and verification of integer computations treats integers as having infinite precision, and most analyses that do respect fixed width lose precision when overflow is possible. We present a novel integer interval abstract domain that correctly handles wrap-around. The analysis is signedness agnostic. By treating integers as strings of bits, only considering signedness for operations that treat them differently, we produce precise, correct results at a modest cost in execution time.

Proteins are biomolecules of life. They fold into a great variety of three-dimensional (3D) shapes. Underlying these folding patterns are many recurrent structural fragments or building blocks (analogous to 'LEGO® bricks'). This paper reports an innovative statistical inference approach to discover a comprehensive dictionary of protein structural building blocks from a large corpus of experimentally determined protein structures. Our approach is built on the Bayesian and information theoretic criterion of minimum message length. To the best of our knowledge, this work is the first systematic and rigorous treatment of a very important data mining problem that arises in the cross-disciplinary area of structural bioinformatics. The quality of the dictionary we find is demonstrated by its explanatory power - any protein within the corpus of known 3D structures can be dissected into successive regions assigned to fragments from this dictionary. This induces a novel one-dimensional representation of three-dimensional protein folding patterns, suitable for application of the rich repertoire of character-string processing algorithms, for rapid identification of folding patterns of newly determined structures. This paper presents the details of the methodology used to infer the dictionary of building blocks, and is supported by illustrative examples to demonstrate its effectiveness and utility.

Many problems are naturally modelled by extending an existing type with additional values. For example for modelling database problems with nulls natural models use booleans and integers with an additional null value. Similarly models involving integers may naturally be extended to handle -∞ and +∞. We extend the constraint modelling language MiniZinc to MiniZinc+ to allow modelling with extended types. The user can specify both the extension of a predefined type with new values, and the behavior of the operations with relation to the new types. The resulting MiniZinc+ model is transformed to a MiniZinc model which is equivalent to the original model. We illustrate the usage of MiniZinc+ to model SQL like problems with integer variables extended with NULL values.

Gene expression profiles can show significant changes when genetically diseased cells are compared with non-diseased cells. Biological networks are often used to identify active subnetworks (ASNs) of the diseases from the expression profiles to understand the reason behind the observed changes. Current methodologies for discovering ASNs mostly use undirected PPI networks and node centric approaches. This can limit their ability to find the meaningful ASNs when using integrated networks having comprehensive information than the traditional protein-protein interaction networks. Using appropriate scoring functions to assess both genes and their interactions may allow the discovery of better ASNs. In this paper, we present CASNet, which aims to identify better ASNs using (i) integrated interaction networks (mixed graphs), (ii) directions of regulations of genes, and (iii) combined node and edge scores. We simplify and extend previous methodologies to incorporate edge evaluations and lessen their sensitivity to significance thresholds. We formulate our objective functions using mixed integer programming (MIP) and show that optimal solutions may be obtained. We compare the ASNs obtained by CASNet and similar other approaches to show that CASNet can often discover more meaningful and stable regulatory ASNs. Our analysis of a breast cancer dataset finds that the positive feedback loops across 7 genes, AR, ESR1, MYC, E2F2, PGR, BCL2 and CCND1 are conserved across the basal/triple negative subtypes in multiple datasets that could potentially explain the aggressive nature of this cancer subtype. Furthermore, comparison of the basal subtype of breast cancer and the mesenchymal subtype of glioblastoma ASNs shows that an ASN in the vicinity of IL6 is conserved across the two subtypes. This result suggests that subtypes of different cancers can show molecular similarities indicating that the therapeutic approaches in different types of cancers may be shared.

We present an approach to propagation-based SAT encoding of combinatorial problems, Boolean equi-propagation, where constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. A key factor is that considering only a small fragment of a constraint model at one time enables us to apply stronger, and even complete, reasoning to detect equivalent literals in that fragment. Once detected, equivalences apply to simplify the entire constraint model and facilitate further reasoning on other fragments. Equi-propagation in combination with partial evaluation and constraint simplification provide the foundation for a powerful approach to SAT-based finite domain constraint solving. We introduce a tool called BEE (Ben-Gurion Equi-propagation Encoder) based on these ideas and demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times.

Abstract One of the main challenges to software testing today is to efficiently handle heap-manipulating programs. These programs often build complex, dynamically allocated data structures during execution and, to ensure reliability, the testing process needs to consider all possible shapes these data structures can take. This creates scalability issues since high (often exponential) numbers of shapes may be built due to the aliasing of references. This paper presents a novel CLP heap solver for the test case generation of heap-manipulating programs that is more scalable than previous proposals, thanks to the treatment of reference aliasing by means of disjunction, and to the use of advanced back-propagation of heap related constraints. In addition, the heap solver supports the use of heap assumptions to avoid aliasing of data that, though legal, should not be provided as input.

Abstract Answer Set Programming (ASP) is a powerful form of declarative programming used in areas such as planning or reasoning. ASP solvers enforce stable model semantics , which rule out solutions representing certain kinds of circular reasoning. Unfortunately, current ASP solvers are incapable of solving problems involving cyclic dependencies between multiple integer or continuous quantities effectively. In this paper, we generalize the notion of stable models to bound founded variables with arbitrary domains, where bounds on such variables need to be justified by some rule in the program in order for the model to be stable. We show how to handle significantly more general rule forms where bound founded variables can act as head or body variables, and where head and body variables can be related via complex constraints subject to certain monotonicity requirements. We describe a new unfounded set detection algorithm which allows us to enforce this generalization of the stable model semantics. We also show how these unfounded sets can be explained in order to allow effective conflict-directed clause learning. The new solver merges the best features of CP, SAT and ASP solvers and allows new types of problems to be solved very efficiently.

Abstract We present a new execution strategy for constraint logic programs called Failure Tabled CLP. Similarly to Tabled CLP our strategy records certain derivations in order to prune further derivations. However, our method only learns from failed derivations. This allows us to compute interpolants rather than constraint projection for generation of reuse conditions. As a result, our technique can be used where projection is too expensive or does not exist. Our experiments indicate that Failure Tabling can speed up the execution of programs with many redundant failed derivations as well as achieve termination in the presence of infinite executions.

Guillotine-based page layout is a method for document layout commonly used by newspapers and magazines, where each region of the page either contains a single article, or is recursively split either vertically or horizontally. Suprisingly there appears to be little research into algorithms for automatic guillotine-based document layout. In this paper we give efficient algorithms to find optimal solutions to guillotine layout problems of two forms. Fixed-cut layout is where the structure of the guillotining is given and we only have to determine the best configuration for each individual article to give the optimal total configuration. Free layout is where we also have to search for the optimal structure. We give bottom-up and top-down dynamic programming algorithms to solve these problems, and propose a novel interaction model for documents on electronic media. Experiments show that our algorithms are effective for realistic layout problems.

Automatic layout of tables is useful in word processing applications and is required in on-line applications because of the need to tailor the layout to the viewport width, choice of font and dynamic content. However, if the table contains text, minimizing the height of the table for a fixed maximum width is a difficult combinatorial optimization problem. We present three different approaches to finding the minimum height layout based on standard approaches for combinatorial optimization. All are guaranteed to find the optimal solution. The first is an A*-based approach that uses an admissible heuristic based on the area of the cell content. The second and third are constraint programming (CP) approaches using the same CP model. The second approach uses traditional CP search, while the third approach uses a hybrid CP/SAT approach, lazy clause generation, that uses learning to reduce the search required. We provide a detailed empirical evaluation of the three approaches and also compare them with two mixed integer programming (MIP) encodings due to Bilauca and Healy.

Lazy clause generation is a powerful approach to reducing search in constraint programming. This is achieved by recording sets of domain restrictions that previously led to failure as new clausal propagators. Symmetry breaking approaches are also powerful methods for reducing search by recognizing that parts of the search tree are symmetric and do not need to be explored. In this paper we show how we can successfully combine symmetry breaking methods with lazy clause generation. Further, we show that the more precise nogoods generated by a lazy clause solver allow our combined approach to exploit redundancies that cannot be exploited via any previous symmetry breaking method, be it static or dynamic.

UNLABELLED: Simple and concise representations of protein-folding patterns provide powerful abstractions for visualizations, comparisons, classifications, searching and aligning structural data. Structures are often abstracted by replacing standard secondary structural features-that is, helices and strands of sheet-by vectors or linear segments. Relying solely on standard secondary structure may result in a significant loss of structural information. Further, traditional methods of simplification crucially depend on the consistency and accuracy of external methods to assign secondary structures to protein coordinate data. Although many methods exist automatically to identify secondary structure, the impreciseness of definitions, along with errors and inconsistencies in experimental structure data, drastically limit their applicability to generate reliable simplified representations, especially for structural comparison. This article introduces a mathematically rigorous algorithm to delineate protein structure using the elegant statistical and inductive inference framework of minimum message length (MML). Our method generates consistent and statistically robust piecewise linear explanations of protein coordinate data, resulting in a powerful and concise representation of the structure. The delineation is completely independent of the approaches of using hydrogen-bonding patterns or inspecting local substructural geometry that the current methods use. Indeed, as is common with applications of the MML criterion, this method is free of parameters and thresholds, in striking contrast to the existing programs which are often beset by them. The analysis of results over a large number of proteins suggests that the method produces consistent delineation of structures that encompasses, among others, the segments corresponding to standard secondary structure. AVAILABILITY: http://www.csse.monash.edu.au/~karun/pmml.

SUMMARY: Protein topology diagrams are 2D representations of protein structure that are particularly useful in understanding and analysing complex protein folds. Generating such diagrams presents a major problem in graph drawing, with automatic approaches often resulting in errors or uninterpretable results. Here we apply a breakthrough in diagram layout to protein topology cartoons, providing clear, accurate, interactive and editable diagrams, which are also an interface to a structural search method. AVAILABILITY: Pro-origami is available via a web server at http://munk.csse.unimelb.edu.au/pro-origami CONTACT: [email protected]; [email protected].

We give a dynamic programming solution to the problem of scheduling scenes to minimize the cost of the talent. Starting from a basic dynamic program, we show a number of ways to improve the dynamic programming solution by preprocessing and restricting the search. We show how by considering a bounded version of the problem, and determining lower and upper bounds, we can improve the search. We then show how ordering the scenes from both ends can drastically reduce the search space. The final dynamic programming solution is orders of magnitude faster than competing approaches and finds optimal solutions to larger problems than were considered previously.

MOTIVATION: Cancer evolves through microevolution where random lesions that provide the biggest advantage to cancer stand out in their frequent occurrence in multiple samples. At the same time, a gene function can be changed by aberration of the corresponding gene or modification of microRNA (miRNA) expression, which attenuates the gene. In a large number of cancer samples, these two mechanisms might be distributed in a coordinated and almost mutually exclusive manner. Understanding this coordination may assist in identifying changes which significantly produce the same functional impact on cancer phenotype, and further identify genes that are universally required for cancer. Present methodologies for finding aberrations usually analyze single datasets, which cannot identify such pairs of coordinating genes and miRNAs. RESULTS: We have developed MIRAGAA, a statistical approach, to assess the coordinated changes of genome copy numbers and miRNA expression. We have evaluated MIRAGAA on The Cancer Genome Atlas (TCGA) Glioblastoma Multiforme datasets. In these datasets, a number of genome regions coordinating with different miRNAs are identified. Although well known for their biological significance, these genes and miRNAs would be left undetected for being less significant if the two datasets were analyzed individually. AVAILABILITY AND IMPLEMENTATION: The source code, implemented in R and java, is available from our project web site at http://www.csse.unimelb.edu.au/~rgaire/MIRAGAA/index.html. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

BACKGROUND: Searching a database of protein structures for matches to a query structure, or occurrences of a structural motif, is an important task in structural biology and bioinformatics. While there are many existing methods for structural similarity searching, faster and more accurate approaches are still required, and few current methods are capable of substructure (motif) searching. RESULTS: We developed an improved heuristic for tableau-based protein structure and substructure searching using simulated annealing, that is as fast or faster and comparable in accuracy, with some widely used existing methods. Furthermore, we created a parallel implementation on a modern graphics processing unit (GPU). CONCLUSIONS: The GPU implementation achieves up to 34 times speedup over the CPU implementation of tableau-based structure search with simulated annealing, making it one of the fastest available methods. To the best of our knowledge, this is the first application of a GPU to the protein structural search problem.

Unit two-variable-per-inequality (UTVPI) constraints form one of the largest class of integer constraints that are polynomial time solvable (unless P = NP). There is considerable interest in their use for constraint solving, abstract interpretation, spatial database algorithms, and theorem proving. In this paper we develop new incremental algorithms for UTVPI constraint satisfaction and implication checking that require ℴ(m + n log n + p) time and ℴ(n + m + p) space to incrementally check satisfiability of m UTVPI constraints on n variables, and we check the implication of p UTVPI constraints. The algorithms can be straightforwardly extended to create nonincremental implication checking and generation of all (nonredundant) implied constraints, as well as generate minimal unsatisfiable subsets and minimal implicants.

Binary Decision Diagram (BDD) based set bounds propagation is a powerful approach to solving set-constraint satisfaction problems. However, prior BDD based techniques in- cur the significant overhead of constructing and manipulating graphs during search. We present a set-constraint solver which combines BDD-based set-bounds propagators with the learning abilities of a modern SAT solver. Together with a number of improvements beyond the basic algorithm, this solver is highly competitive with existing propagation based set constraint solvers.

This paper describes the encoding of a telecommunications feature subscription configuration problem to propositional logic and its solution using a state-of-the-art Boolean satisfaction solver. The transformation of a problem instance to a corresponding propositional formula in conjunctive normal form is obtained in a declarative style. An experimental evaluation indicates that our encoding is considerably faster than previous approaches based on the use of Boolean satisfaction solvers. The key to obtaining such a fast solver is the careful design of the Boolean representation and of the basic operations in the encoding. The choice of a declarative programming style makes the use of complex circuit designs relatively easy to incorporate into the encoder and to fine tune the application.

BACKGROUND: Searching for proteins that contain similar substructures is an important task in structural biology. The exact solution of most formulations of this problem, including a recently published method based on tableaux, is too slow for practical use in scanning a large database. RESULTS: We developed an improved method for detecting substructural similarities in proteins using tableaux. Tableaux are compared efficiently by solving the quadratic program (QP) corresponding to the quadratic integer program (QIP) formulation of the extraction of maximally-similar tableaux. We compare the accuracy of the method in classifying protein folds with some existing techniques. CONCLUSION: We find that including constraints based on the separation of secondary structure elements increases the accuracy of protein structure search using maximally-similar subtableau extraction, to a level where it has comparable or superior accuracy to existing techniques. We demonstrate that our implementation is able to search a structural database in a matter of hours on a standard PC.

Abstract A constraint programming system combines two essential components: a constraint solver and a search engine. The constraint solver reasons about satisfiability of conjunctions of constraints, and the search engine controls the search for solutions by iteratively exploring a disjunctive search tree defined by the constraint program. In this paper we give a monadic definition of constraint programming in which the solver is defined as a monad threaded through the monadic search tree. We are then able to define search and search strategies as first-class objects that can themselves be built or extended by composable search transformers. Search transformers give a powerful and unifying approach to viewing search in constraint programming, and the resulting constraint programming system is first class and extremely flexible.

No abstract available.

Set bounds propagation is the most popular approach to solving constraint satisfaction problems (CSPs) involving set variables. The use of reduced ordered Binary Decision Diagrams (BDDs) to represent and solve set CSPs is well understood and brings the advantage that propagators for arbitrary set constraints can be built. This can substantially improve solving. The disadvantages of BDDs is that creating and manipulating BDDs can be expensive. In this paper we show how we can perform set bounds propagation using BDDs in a much more efficient manner by generically creating set constraint predicates, and using a marking approach to propagation. The resulting system can be significantly faster than competing approaches to set bounds propagation.

Dynamic programming is a powerful technique for solving optimization problems efficiently. We consider a dynamic program as simply a recursive program that is evaluated with memoization and lookup of answers. In this paper we examine how, given a function calculating a bound on the value of the dynamic program, we can optimize the compilation of the dynamic program function. We show how to automatically transform a dynamic program to a number of more efficientversions making use of the bounds function. We compare the different transformed versions on a number of example dynamic programs, and show the benefits in search space and time that can result.

Difference constraints of the form x - y ≤ d are well studied, with efficient algorithms for satisfaction and implication, because of their connection to shortest paths. Finite domain propagation algorithms however do not make use of these algorithms, and typically treat each difference constraint as a separate propagator. Propagation does guarantee completeness of solving but can be needlessly slow. In this paper we describe how to build a (bounds consistent) global propagator for difference constraints that treats them all simultaneously. SAT modulo theory solvers have included theory solvers for difference constraints for some time. While a theory solver for difference constraints gives the basis of a global difference constraint propagator, we show how the requirements on the propagator are quite different. We give experiments showing that treating difference constraints globally can substantially improve on the standard propagation approach

Constraint propagation solvers interleave propagation (removing impossible values from variables domains) with search. Propagation is performed by executing propagators (removing values) implementing constraints (defining impossible values). In order to specify constraint problems with a propagation solver often many new intermediate variables need to be introduced. Each variable plays a role in calculating the value of some expression. But as search proceeds not all of these expressions will be of interest any longer, but the propagators implementing them will remain active. In this paper we show how we can analyse the propagation graph of the solver in linear time to determine intermediate variables that can be removed without effecting the result. Experiments show that applying this analysis can reduce the space and time requirements for constraint propagation on example problems

UNLABELLED: Comparison and classification of folding patterns from a database of protein structures is crucial to understand the principles of protein architecture, evolution and function. Current search methods for proteins with similar folding patterns are slow and computationally intensive. The sharp growth in the number of known protein structures poses severe challenges for methods of structural comparison. There is a need for methods that can search the database of structures accurately and rapidly. We provide several methods to search for similar folding patterns using a concise tableau representation of proteins that encodes the relative geometry of secondary structural elements. Our first approach allows the extraction of identical and very closely-related protein folding patterns in constant-time (per hit). Next, we address the hard computational problem of extraction of maximally-similar subtableaux, when comparing two tableaux. We solve the problem using Quadratic and Linear integer programming formulations and demonstrate their power to identify subtle structural similarities, especially when protein structures significantly diverge. Finally, we describe a rapid and accurate method for comparing a query structure against a database of protein domains, TableauSearch. TableauSearch is rapid enough to search the entire structural database in seconds on a standard desktop computer. Our analysis of TableauSearch on many queries shows that the method is very accurate in identifying similarities of folding patterns, even between distantly related proteins. AVAILABILITY: A web server implementing the TableauSearch is available from http://hollywood.bx.psu.edu/TabSearch.

Abstract The HM(X) system is a generalization of the Hindley/Milner system parameterized in the constraint domain X. Type inference is performed by generating constraints out of the program text, which are then solved by the domain-specific constraint solver X. The solver has to be invoked at the latest when type inference reaches a let node so that we can build a polymorphic type. A typical example of such an inference approach is Milner's algorithm W. We formalize an inference approach where the HM(X) type inference problem is first mapped to a CLP(X) program. The actual type inference is achieved by executing the CLP(X) program. Such an inference approach supports the uniform construction of type inference algorithms and has important practical consequences when it comes to reporting type errors. The CLP(X) style inference system, where X is defined by Constraint Handling Rules, is implemented as part of the Chameleon system.

We investigate the usability of constraint-based alignment and distribution placement tools in diagram editors. Currently one-way constraints are used to provide alignment and distribution tools in many commercial editors. We believe the limitations of these constraints lead to serious usability issues, and thus suggest that such tools be implemented using multi-way constraints. We have conducted two usability studies, the first studies we are aware of that examine the relative usefulness of interactive graphical tools based on one-way and multi-way constraints. They provide strong evidence that multi-way constraint-based alignment and distribution tools are more usable than one-way constraint-based alignment and distribution tools.

This article presents a model and implementation techniques for speeding up constraint propagation. Three fundamental approaches to improving constraint propagation based on propagators as implementations of constraints are explored: keeping track of which propagators are at fixpoint, choosing which propagator to apply next, and how to combine several propagators for the same constraint. We show how idempotence reasoning and events help track fixpoints more accurately. We improve these methods by using them dynamically (taking into account current variable domains to improve accuracy). We define priority-based approaches to choosing a next propagator and show that dynamic priorities can improve propagation. We illustrate that the use of multiple propagators for the same constraint can be advantageous with priorities, and introduce staged propagators that combine the effects of multiple propagators with priorities for greater efficiency.

Abstract This paper presents a Prolog interface to the MiniSat satisfiability solver. Logic programming with satisfiability combines the strengths of the two paradigms: logic programming for encoding search problems into satisfiability on the one hand and efficient SAT solving on the other. This synergy between these two exposes a programming paradigm that we propose here as a logic programming pearl. To illustrate logic programming with SAT solving, we give an example Prolog program that solves instances of Partial MAXSAT.

A standard approach to large network visualization is to provide an overview of the network and a detailed view of a small component of the graph centred around a focal node. The user explores the network by changing the focal node in the detailed view or by changing the level of detail of a node or cluster. For scalability, fast force-based layout algorithms are used for the overview and the detailed view. However, using the same layout algorithm in both views is problematic since layout for the detailed view has different requirements to that in the overview. Here we present a model in which constrained graph layout algorithms are used for layout in the detailed view. This means the detailed view has high-quality layout including sophisticated edge routing and is customisable by the user who can add placement constraints on the layout. Scalability is still ensured since the slower layout techniques are only applied to the small subgraph shown in the detailed view. The main technical innovations are techniques to ensure that the overview and detailed view remain synchronized, and modifying constrained graph layout algorithms to support smooth, stable layout. The key innovation supporting stability are new dynamic graph layout algorithms that preserve the topology or structure of the network when the user changes the focus node or the level of detail by in situ semantic zooming. We have built a prototype tool and demonstrate its use in two application domains, UML class diagrams and biological networks.

We give a dynamic-programming solution to the problem of minimizing the maximum number of open stacks. Starting from a call-based dynamic program, we show a number of ways to improve the dynamic-programming search, preprocess the problem to simplify it, and determine lower and upper bounds. We then explore a number of search strategies for reducing the search space. The final dynamic-programming solution is, we believe, highly effective.

Abstract Functional dependencies are a popular and useful extension to Haskell style type classes. We give a reformulation of functional dependencies in terms of Constraint Handling Rules (CHRs). In previous work, CHRs have been employed for describing user-programmable type extensions in the context of Haskell style type classes. Here, we make use of CHRs to provide for the first time a concise result that under some sufficient conditions, functional dependencies allow for sound, complete and decidable type inference. The sufficient conditions imposed on functional dependencies can be very limiting. We show how to safely relax these conditions and suggest several sound extensions of functional dependencies. Our results allow for a better understanding of functional dependencies and open up the opportunity for new applications.

A widely adopted approach to solving constraint satisfaction problems combines systematic tree search with various degrees of constraint propagation for pruning the search space. One common technique to improve the execution efficiency is to add redundant constraints, which are constraints logically implied by others in the problem model. However, some redundant constraints are propagation redundant and hence do not contribute additional propagation information to the constraint solver. Redundant constraints arise naturally in the process of redundant modeling where two models of the same problem are connected and combined through channeling constraints. In this paper, we give general theorems for proving propagation redundancy of one constraint with respect to channeling constraints and constraints in the other model. We illustrate, on problems from CSPlib (http://www.csplib.org), how detecting and removing propagation redundant constraints in redundant modeling can speed up search by several order of magnitudes.

Taylor introduced a variable binding scheme for logic variables in his PARMA system, that uses cycles of bindings rather than the linear chains of bindings used in the standard WAM representation. Both the HAL and dProlog languages make use of the PARMA representation in their Herbrand constraint solvers. Unfortunately, PARMA's trailing scheme is considerably more expensive in both time and space consumption. The aim of this paper is to present several techniques that lower the cost. First, we introduce a trailing analysis for HAL using the classic PARMA trailing scheme that detects and eliminates unnecessary trailings. The analysis, whose accuracy comes from HAL's determinism and mode declarations, has been integrated in the HAL compiler and is shown to produce space improvements as well as speed improvements. Second, we explain how to modify the classic PARMA trailing scheme to halve its trailing cost. This technique is illustrated and evaluated both in the context of dProlog and HAL. Finally, we explain the modifications needed by the trailing analysis in order to be combined with our modified PARMA trailing scheme. Empirical evidence shows that the combination is more effective than any of the techniques when used in isolation.

Program analysis is essential for the optimized compilation of Constraint Handling Rules (CHRs) as well as the inference of behavioral properties such as confluence and termination. Up to now all program analyses for CHRs have been developed in an ad hoc fashion.In this work we bring the general program analysis methodology of abstract interpretation to CHRs: we formulate an abstract interpretation framework over the call-based operational semantics of CHRs. The abstract interpretation framework is non-obvious since it needs to handle the highly non-deterministic execution of CHRs. The use of the framework is illustrated with two instantiations: the CHR-specific late storage analysis and the more generally known groundness analysis. In addition, we discuss optimizations based on these analyses and present experimental results.

In this paper we present a new approach to modeling finite set domain constraint problems using Reduced Ordered Binary Decision Diagrams (ROBDDs). We show that it is possible to construct an efficient set domain propagator which compactly represents many set domains and set constraints using ROBDDs. We demonstrate that the ROBDD-based approach provides unprecedented flexibility in modeling constraint satisfaction problems, leading to performance improvements. We also show that the ROBDD-based modeling approach can be extended to the modeling of integer and multiset constraint problems in a straightforward manner. Since domain propagation is not always practical, we also show how to incorporate less strict consistency notions into the ROBDD framework, such as set bounds, cardinality bounds and lexicographic bounds consistency. Finally, we present experimental results that demonstrate the ROBDD-based solver performs better than various more conventional constraint solvers on several standard set constraint problems.

This article explores the question of when two propagation-based constraint systems have the same behavior, in terms of search space. We categorize the behavior of domain and bounds propagators for primitive constraints, and provide theorems that allow us to determine propagation behaviors for conjunctions of constraints. We then show how we can use this to analyze CLP(FD) programs to determine when we can safely replace domain propagators by more efficient bounds propagators without increasing search space. Empirical evaluation shows that programs optimized by the analysis' results are considerably more efficient.

We present a novel approach to allow for overloading of identifiers in the spirit of type classes. Our approach relies on a combination of the HM(X) type system framework with Constraint Handling Rules (CHRs). CHRs are a declarative language for writing incremental constraint solvers, that provide our scheme with a form of programmable type language. CHRs allow us to precisely describe the relationships among overloaded identifiers. Under some sufficient conditions on the CHRs we achieve decidable type inference and the semantic meaning of programs is unambiguous. Our approach provides a common formal basis for many type class extensions such as multiparameter type classes and functional dependencies.

Recent constraint logic programming (CLP) languages, such as HAL and Mercury, require type, mode and determinism declarations for predicates. This information allows the generation of efficient target code and the detection of many errors at compile-time. Unfortunately, mode checking in such languages is difficult. One of the main reasons is that, for each predicate mode declaration, the compiler is required to appropriately re-order literals in the predicate's definition. The task is further complicated by the need to handle complex instantiations (which interact with type declarations and higher-order predicates) and automatic initialization of solver variables. Here we define mode checking for strongly typed CLP languages which require reordering of clause body literals. In addition, we show how to handle a simple case of polymorphic modes by using the corresponding polymorphic types.

In this paper we discuss the optimizing compilation of Constraint Handling Rules (CHRs). CHRs are a multi-headed committed choice constraint language, commonly applied for writing incremental constraint solvers. CHRs are usually implemented as a language extension that compiles to the underlying language. In this paper we show how we can use different kinds of information in the compilation of CHRs to obtain access efficiency, and a better translation of the CHR rules into the underlying language, which in this case is HAL. The kinds of information used include the types, modes, determinism, functional dependencies and symmetries of the CHR constraints. We also show how to analyze CHR programs to determine this information about functional dependencies, symmetries and other kinds of information supporting optimizations.

All in-text\treferences\tunderlined\tin\tblue\tare\tlinked\tto\tpublications\ton\tResearchGate, letting you\taccess\tand\tread\tthem\timmediately.

We introduce just enough tabling (JET), a mechanism to suspend and resume the tabled execution of logic programs at an arbitrary point. In particular, JET allows pruning of tabled logic programs to be performed without resorting to any recomputation. We discuss issues that are involved in supporting pruning in tabled resolution, how re-execution of tabled computations which were previously pruned

Proceedings of the 2003 ACM SIGPLAN Haskell Workshop

Nogood recording is a dynamic learning technique widely applied to solve CSP (constraint satisfaction problems). It is highly effective in reducing the search space for SAT (satisfiability) problems. While SAT is NP-complete, the problem restricted to binary clauses (2SAT) is solvable in linear time. We can improve SAT solving by incorporating 2SAT solving techniques. In this paper we investigate extending nogood recording to make use of binary clause resolution. Our experiments show that nogoods generated from binary resolution can significantly reduce the search space, and size of nogoods generated, as well as the search time.

An unsatisfiable set of constraints is minimal if all its (strict) subsets aresatisfiable.A number of forms of error diagnosis, including circuit error diagnosis and type error diagnosis, require finding all minimal unsatisfiable subsets of a given set of constraints (representing an error), in order to generate the best explanation of the error. In this paper we give algorithms for efficiently determining all minimal unsatisfiable subsets for any kind of constraints. We show how taking into account notions of independence of constraints and using incremental constraint solvers can significantly improve the calculation of these subsets.

Constraint Handling Rules (CHRs) are a high-level committed choice programming language commonly used to write constraint solvers. While the semantic basis of CHRs allows them to extend arbitrary underlying constraint solvers, in practice, all current implementations only extend Herbrand equation solvers. In this paper we show how to define CHR programs that extend arbitrary solvers and fully interact with them. In the process, we examine how to compile such programs to perform as little recomputation as possible, and describe how to build index structures for CHR constraints that are modified automatically when variables in the underlying solver change. We report on the implementation of these techniques in the HAL compiler, and give empirical results illustrating their benefits.

We show how a range of role-based access control (RBAC) models may be usefully represented as constraint logic programs, executable logical specifications. The RBAC models that we define extend the "standard" RBAC models that are described by Sandhu et al., and enable security administrators to define a range of access policies that may include features, like denials of access and temporal authorizations, that are often useful in practice, but which are not widely supported in existing access control models. Representing access policies as constraint logic programs makes it possible to support certain policy options, constraint checks, and administrator queries that cannot be represented by using related methods (like logic programs). Representing an access control policy as a constraint logic program also enables access requests and constraint checks to be efficiently evaluated.

In this paper we present the first exception analysis for a non-strict language. We augment a simply-typed functional language with exceptions, and show that we can define a type-based inference system to detect uncaught exceptions. We have implemented this exception analysis in the GHC compiler for Haskell, which has been recently extended with exceptions. We give empirical evidence that the analysis is practical.

We present a minimal extension of the Hindley/Milner system to allow for overloading of identifiers. Our approach relies on a combination of the HM(X) type system framework with Constraint Handling Rules (CHRs). CHRs are a declarative language for writing incremental constraint solvers. CHRs allow us to precisely describe the relationships among overloaded identifiers. Under some sufficient conditions on the CHRs we achieve decidable type inference and the semantic meaning of programs is unambiguous. Our approach allows us to combine open and closed world overloading. We also show how to deal with overlapping definitions.

The paper presents a novel approach to pair-sharing analysis of logic programs. The pair-sharing domain ASub of Søndergaard is known to be more efficient than the set-sharing domain Sharing of Jacobs and Langen and gains accuracy because of linearity tracking. However, it is less accurate because of weaker groundness information, and the fact that it loses track of where new groundness eliminates sharing. In this paper we present a new domain which inherits the advantages of both ASub and Sharing and is uniformly more accurate in terms of pair-sharing than each of the two domains.The proposed domain expresses pair-sharing in terms of existence of traversable paths in relation graphs derived from program constraints. Each edge of a relation graph has an attached groundness formula which defines under what groundness conditions it still causes sharing. This allows the domain to maintain information about when groundness can eliminate sharing. Relation graphs are augmented by separate groundness information (usually Def or Pos). The groundness analysis and groundness formulae can be represented using efficient ROBDD methods.

Recent logic programming languages, such as Mercury and HAL, require type, mode and determinism declarations for predicates. This information allows the generation of efficient target code and the detection of many errors at compile-time. Unfortunately, mode checking in such languages is difficult. One of the main reasons is that, for each predicate mode declaration, the compiler is required to decide which parts of the procedure bind which variables, and how conjuncts in the predicate definition should be re-ordered to enforce this behaviour. Current mode checking systems limit the possible modes that may be used because they do not keep track of aliasing information, and have only a limited ability to infer modes, since inference does not perform reordering. In this paper we develop a mode inference system for Mercury based on mapping each predicate to a system of Boolean constraints that describe where its variables can be produced. This allows us handle programs that are not supported by the existing system.

The value of a variable is often given by a field of a heap cell, and frequently the program will pick up the values of several variables from different fields of the same heap cell. By keeping some of these variables out of the stack frame, and accessing them in their original locations on the heap instead, we can reduce the number of loads from and stores to the stack at the cost of introducing a smaller number of loads from the heap. We present an algorithm that finds the optimal set of variables to access via a heap cell instead of a stack slot, and transforms the code of the program accordingly. We have implemented this optimization in the Mercury compiler, and our measurements show that it can reduce program runtimes by up to 12% while at the same time reducing program size. The optimization is straightforward to apply to Mercury and to other languages with immutable data structures; its adaptation to languages with destructive assignment would require the compiler to perform mutability analysis.

Intelligent backtracking is a technique used in constraint programming for reducing search in solving combinatorial feasibility problems. The technique uses information derived from small sets of infeasible constraints discovered in one part of the search space to avoid searching other, similar, regions. It is often able to reduce the size of the search space significantly. For many problems, however, the computational effort required to achieve this reduction in search space is prohibitive. We introduce an algorithm that uses intelligent backtracking inside a linear-programming based branch-and-bound framework. We show that minimal infeasible sets can immediately be deduced from the dual extreme ray associated with the infeasible linear program. This allows us to obtain the reduction in search space associated with intelligent backtracking, without paying the large computational cost. We show the implementation of our intelligent backtracking approach as a branch-and-cut algorithm, and present computational results.

This paper explores the question of when two propagation-based constraint systems have the same behaviour, in terms of search space. We categorise the behaviour of domain and bounds propagators for primitive constraints, and provide theorems that allow us to determine propagation behaviours for conjunctions of constraints. We then show how we can use this to analyse CLP(FD) programs to determine when we can safely replace domain propagators by more efficient bounds propagators without increasing search space.

Cost-based unbalanced R-trees (CUR-trees) are a cost-function-based data structure for spatial data. CUR-trees are constructed specifically to improve the evaluation of intersection queries, the most basic selection query in an R-tree. A CUR-tree is built taking into account a given query distribution for the queries and a cost model for their execution. Depending on the expected frequency of access, objects or subtrees are stored higher up in the tree. After each insertion in the tree, local reorganizations of a node and its children have their expected query cost evaluated, and a reorganization is performed if this is beneficial. No strict balancing of the trees applies, allowing the tree to unfold solely based on the result of the cost evaluation. We present our cost-based approach and describe the evaluation and reorganization operations based on the cost function. We present a cost model for in-memory access costs and we present three different query models. In our experiments, we compare the performance of the CUR-tree to the R-tree and the R*-tree. The CUR-tree is able to significantly improve intersection query performance, without unacceptably increasing the cost of building the tree. The use of R-trees for in-memory data reflects the high (and growing) cost of bringing data from RAM into the CPU cache relative to the cost of other computations.

Linear equality and inequality constraints arise naturally in specifying many aspects of user interfaces, such as requiring that one window be to the left of another, requiring that a pane occupy the leftmost third of a window, or preferring that an object be contained within a rectangle if possible. Previous constraint solvers designed for user interface applications cannot handle simultaneous linear equations and inequalities efficiently. This is a major limitation, as such systems of constraints arise often in natural declarative specifications. We describe Cassowary---an incremental algorithm based on the dual simplex method, which can solve such systems of constraints efficiently. We have implemented the algorithm as part of a constraint-solving toolkit. We discuss the implementation of the toolkit, its application programming interface, and its performance.

Global analyzers traditionally read and analyze the entire program at once, in a nonincremental way. However, there are many situations which are not well suited to this simple model and which instead require reanalysis of certain parts of a program which has already been analyzed. In these cases, it appears inefficient to perform the analysis of the program again from scratch, as needs to be done with current systems. We describe how the fixed-point algorithms used in current generic analysis engines for (constraint) logic programming languages can be extended to support incremental analysis. The possible changes to a program are classified into three types: addition, deletion, and arbitrary change. For each one of these, we provide one or more algorithms for identifying the parts of the analysis that must be recomputed and for performing the actual recomputation. The potential benefits and drawbacks of these algorithms are discussed. Finally, we present some experimental results obtained with an implementation of the algorithms in the PLAI generic abstract interpretation framework. The results show significant benefits when using the proposed incremental analysis algorithms.

Cascading Style Sheets have been introduced by the W3C as a mechanism for controlling the appearance of HTML documents. In this paper, we demonstrate how constraints provide a powerful unifying formalism for declaratively understanding and specifying style sheets for web documents. With constraints we can naturally and declaratively specify complex behavior such as inheritance of properties and cascading of conflicting style rules. We give a detailed description of a constraint-based style sheet model, CCSS, which is compatible with virtually all of the CSS 2.0 specification. It allows more flexible specification of layout, and also allows the designer to provide multiple layouts that better meet the desires of the user and environmental restrictions. We also describe a prototype extension of the Amaya browser that demonstrates the feasibility of CCSS.

We investigate Jacobs and Langen's Sharing domain, introduced for the analysis of variable sharing in logic programs, and show that it is isomorphic to Marriott and Søndergaard's Pos domain, introduced for the analysis of groundness dependencies. Our key idea is to view the sets of variables in a Sharing domain element as the models of a corresponding Boolean function. This leads to a recasting of sharing analysis in terms of the property of “not being affected by the binding of a single variable.” Such an “unaffectedness dependency” analysis has close connections with groundness dependency analysis using positive Boolean functions. This new view improves our understanding of sharing analysis, and leads to an elegant expression of its combination with groundness dependency analysis based on the reduced product of Sharing and Pos. It also opens up new avenues for the efficient implementation of sharing analysis, for example using reduced order binary decision diagrams, as well as efficient implementation of the reduced product, using domain factorizations.

Heuristic repair algorithms, a class of local search methods, demonstrate impressive efficiency in solving some large-scale and hard instances of constraint satisfaction problems (CSPs). We draw a surprising connection between heuristic repair techniques and the discrete Lagrange multiplier methods by transforming CSPs into zero-one constrained optimization problems. A Lagrangian-based search scheme LSDL is proposed. We show how GENET, a representative heuristic repair algorithm, can be reconstructed from LSDL. The dual viewpoint of GENET as a heuristic repair method and Lagrange multiplier method allows us to investigate variants of GENET from both perspectives. Benchmarking results confirm that first, our reconstructed GENET has the same fast convergence behavior as other GENET implementations reported in the literature, competing favourably with other state-of-the-art methods on a set of hard graph colouring problems. Second, our best variant, which combines techniques from heuristic repair and Lagrangian methods, is always more efficient than the reconstructed GENET, and can better it by an order of magnitude.

The incorporation of global program analysis into recent compilers for Constraint Logic Programming (CLP) languages has greatly improved the efficiency of compiled programs. We present a global analyser based on abstract interpretation. Unlike traditional optimizers, whose designs tend to be ad hoc, the analyser has been designed with flexibility in mind. The analyser is incremental, allowing substantial program transformations by a compiler without requiring redundant re-computation of analysis data. The analyser is also generic in that it can perform a large number of different program analyses. Furthermore, the analyser has an object-oriented design, enabling it to be adapted to different applications easily and allowing it to be used with various CLP languages with simple modifications. As an example of this generality, we sketch the use of the analyser in two different applications involving two distinct CLP languages: an optimizing compiler for CLP(R) programs and an application for detecting occur-check problems in Prolog programs. © 1998 John Wiley & Sons Ltd.

We introduce a new constraint domain, aggregation constraints, that is useful in database query languages, and in constraint logic programming languages that incorporate aggregate functions. We formally study the fundamental problem of determining if a conjunction of aggregation constraints is satisfiable, and show that, for many classes of aggregation constraints, the problem is undecidable. We describe a complete and minimal axiomatization of aggregation constraints, for the SQL aggregate functions min, max, sum, count and average, over a non-empty, finite multiset on several domains. This axiomatization helps identify classes of aggregation constraints for which the satisfiability check is efficient. We present a polynomial-time algorithm that directly checks for satisfiability of a conjunction of aggregation range constraints over a single multiset; this is a practically useful class of aggregation constraints. We discuss the relationships between aggregation constraints over a non-empty, finite multiset of reals, and constraints on the elements of the multiset. We show how these relationships can be used to push constraints through aggregate functions to enable compile-time optimization of database queries involving aggregate functions and constraints.

Constraint Logic Programming (CLP) languages extend logic programming by allowing the use of constraints from different domains such as real numbers or Boolean functions. They have proved to be ideal for expressing problems that require interactive mathematical modeling and complex combinatorial optimization problems. However, CLP languages have mainly been considered as research systems, useful for rapid prototyping, by not really competitive with more conventional programming languages where efficiency is a more important consideration. One promising approach to improving the performance of CLP systems is the use of powerful program optimizations to reduce the cost of constraint solving. We extend work in this area by describing a new optimizing compiler for the CLP language CLP(ℛ). The compiler implements six powerful optimizations: reordering of constraints, removal of redundant variables, and specialization of constraints which cannot fail. Each program optimization is designed to remove the overhead of constraint solving when possible and keep the number of constraints in the store as small as possible. We systematically evaluate the effectiveness of each optimization in isolation and in combination. Our empirical evaluation of the compiler verifies that optimizing compilation can be made efficient enough to allow compilation of real-world programs and that it is worth performing such compilation because it gives significant time and space performance improvements.

Many important applications, such as graph coloring, scheduling and production planning, can be solved by GENET, a local search method which is used to solve binary constraint satisfaction problems (CSPs). Where complete search methods are typically augmented with consistency methods to reduce the search, local search methods are not. We propose a consistency technique, lazy arc consistency, which is suitable for use within GENET. We show it can improve the efficiency of the GENET search on some instances of binary CSPs, and does not suffer the overhead of full arc consistency.

Constraint satisfaction problems (CSPs) occur widely in real-life applications such as bin-packing, planning and scheduling. EGENET: a neural network simulator based on the min-conflict heuristic, has had remarkable success in solving hard CSPs such as hard graph-colouring problems. Consistency techniques such as arc consistency have been extensively used to improve the search behaviour of complete search methods, by removing values and combinations of values that cannot take part in any solution. They are not typically used for stochastic search methods such as EGENET. The authors show how to efficiently incorporate consistency methods in EGENET. This improves the convergence behaviour of EGENET and also makes it able to detect insoluble CSPs. They compare the improved EGENET against the original version and versions incorporating state-of-art consistency techniques such as AC-4 or PC-4.

Linear equality and inequality constraints arise naturally in specifying many aspects of user interfaces, such as requiring that one window be to the left of another, requiring that a pane occupy the leftmost l/3 of a window, or preferring that an object be contained within a rectangle if possible.Current constraint solvers designed for UI applications cannot efficiently handle simultaneous linear equations and inequalities.This is a major limitation.We describe incremental algorithms based on the dual simplex and active set methods that can solve such systems of constraints efficiently.

Magic sets rewriting is a well-known optimization heuristic for complex decision-support queries. There can be many variants of this rewriting even for a single query, which differ greatly in execution performance. We propose cost-based techniques for selecting an efficient variant from the many choices.Our first contribution is a practical scheme that models magic sets rewriting as a special join method that can be added to any cost-based query optimizer. We derive cost formulas that allow an optimizer to choose the best variant of the rewriting and to decide whether it is beneficial. The order of complexity of the optimization process is preserved by limiting the search space in a reasonable manner. We have implemented this technique in IBM's DB2 C/S V2 database system. Our performance measurements demonstrate that the cost-based magic optimization technique performs well, and that without it, several poor decisions could be made.Our second contribution is a formal algebraic model of magic sets rewriting, based on an extension of the multiset relational algebra, which cleanly defines the search space and can be used in a rule-based optimizer. We introduce the multiset θ-semijoin operator, and derive equivalence rules involving this operator. We demonstrate that magic sets rewriting for non-recursive SQL queries can be modeled as a sequential composition of these equivalence rules.

We present a general technique to push query constraints (such as length≤1000) into database views and (constraint) logic programs. We introduce the notion of parametrized constraints, which help us push constraints with argument values that are known only at run time, and develop techniques for pushing parametrized constraints into predicate/view definitions. Our technique provides a way of compiling programs with constraint queries into programs with parametrized constraints compiled in, and which can be executed on systems, such as database query evaluation systems, that do not handle full constraint solving. Thereby our technique can push constraint selections that earlier constraint query rewriting techniques could not. Our technique is independent of the actual constraint domain, and we illustrate its use with equality constraints on structures (which are useful in object-oriented query languages) and linear arithmetic constraints.

Central to constraint logic programming (CLP) languages is the notion of a global constraint solver which is queried to direct execution and to which constraints are monotonically added. We present a methodology for use in the compilation of CLP languages which is designed to reduce the overhead of the global constraint solver. This methododology is based on three optimizations. The first, refinement, involves adding new constraints, which in effect make information available earlier in the computation, guiding subsequent execution away from unprofitable choices. The second, removal, involves eliminating constraints from the solver when they are redundant. The last, reordering, involves moving constraint addition later and constraint removal earlier in the computation. Determining the applicability of each optimization requires sophisticated global analysis. These analyses are based on abstract interpretation and provide information about potential and definite interaction between constraints.

An abstract machine is described for the CLP(ℜ) programming language. It is intended as a first step toward enabling CLP(ℜ) programs to be executed with efficiency approaching that of conventional languages. The core Constraint Logic Arithmetic Machine (CLAM) extends the Warren Abstract Machine (WAM) for compiling Prolog with facilities for handling real arithmetic constraints. The full CLAM includes facilities for taking advantage of information obtained from global program analysis.

An overview of the structure of Aditi, a disk-based deductive database system under continuous development at the University of Melbourne, is presented. The aim of the project is to find out what implementation methods and optimization techniques would make deductive databases competitive with current commercial relational databases. The structure of the Aditi prototype is based on a variant of the client-server model. The front end of Aditi interacts with the user exclusively in a logical language that has more expressive power than relational query languages. The back end uses relational technology for efficiency in the management of disk-based data and uses some optimization algorithms especially developed for the bottom-up evaluation of logical queries involving recursion. The system has been functional for almost two years now, and has already proven its worth as a research tool.>

Constructive negation is an extension of the negation as failure rule to handle nonground negative subgoals in a constructive manner. It entails the following procedure: nodes of the subderivation for the nonground negative subgoal are collected as a disjunction and negated giving a formula equivalent to the negative subgoal. Constructive negation was formulated for logic programming in the Herbrand universe by introducing disequality constraints. A framework for constructive negation for constraint logic programming over arbitrary structures that is sound and complete with respect to the three-valued consequences of the completion of a program is described, and a simpler, more efficient form of constructive negation for the Herbrand universe is obtained. What makes a structure particularly suited to the use of constructive negation is characterized, and this suitability condition is shown for a number of structures and classes of structures.>

The incremental linear constraint satisfaction problem consists of repeatedly solving the satisfiability problem for a growing set of linear constraints. This problem is important to constraint logic programming systems where constraints are discovered one at a time and added to a current constraint set, and the satisfiability of this constraint set must be known at all times. Implicit equalities of a system of constraints are inequality constraints that are satisfied as an equality in all solutions of the system of constraints. Detecting implicit equalities is important in determining the minimal (canonical) representation of a system of linear constraints. In incremental constraint solving systems detecting implicit equalities provides information that can simplify further constraint solving. We present an algorithm which efficiently solves the incremental linear constraint satisfaction problem and detects all the implicit equalities present in the constraints. The algorithm forms a basis for the inequality constraint solver in the CLP(ℜ) system. INFORMS Journal on Computing, ISSN 1091-9856, was published as ORSA Journal on Computing from 1989 to 1995 under ISSN 0899-1499.