Arrow Research search

Author name cluster

Bart Selman

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

85 papers
2 author rows

Possible papers

85

ICML Conference 2023 Conference Paper

Weighted Sampling without Replacement for Deep Top-k Classification

  • Dieqiao Feng
  • Yuanqi Du
  • Carla P. Gomes
  • Bart Selman

The top-$k$ classification accuracy is a crucial metric in machine learning and is often used to evaluate the performance of deep neural networks. These networks are typically trained using the cross-entropy loss, which optimizes for top-$1$ classification and is considered optimal in the case of infinite data. However, in real-world scenarios, data is often noisy and limited, leading to the need for more robust losses. In this paper, we propose using the Weighted Sampling Without Replacement (WSWR) method as a learning objective for top-$k$ loss. While traditional methods for evaluating WSWR-based top-$k$ loss are computationally impractical, we show a novel connection between WSWR and Reinforcement Learning (RL) and apply well-established RL algorithms to estimate gradients. We compared our method with recently proposed top-$k$ losses in various regimes of noise and data size for the prevalent use case of $k = 5$. Our experimental results reveal that our method consistently outperforms all other methods on the top-$k$ metric for noisy datasets, has more robustness on extreme testing scenarios, and achieves competitive results on training with limited data.

AAAI Conference 2022 Conference Paper

Cooperative Multi-Agent Fairness and Equivariant Policies

  • Niko A. Grupen
  • Bart Selman
  • Daniel D. Lee

We study fairness through the lens of cooperative multi-agent learning. Our work is motivated by empirical evidence that naive maximization of team reward yields unfair outcomes for individual team members. To address fairness in multiagent contexts, we introduce team fairness, a group-based fairness measure for multi-agent learning. We then prove that it is possible to enforce team fairness during policy optimization by transforming the team’s joint policy into an equivariant map. We refer to our multi-agent learning strategy as Fairness through Equivariance (Fair-E) and demonstrate its effectiveness empirically. We then introduce Fairness through Equivariance Regularization (Fair-ER) as a soft-constraint version of Fair-E and show that it reaches higher levels of utility than Fair-E and fairer outcomes than non-equivariant policies. Finally, we present novel findings regarding the fairnessutility trade-off in multi-agent settings; showing that the magnitude of the trade-off is dependent on agent skill.

NeurIPS Conference 2022 Conference Paper

Left Heavy Tails and the Effectiveness of the Policy and Value Networks in DNN-based best-first search for Sokoban Planning

  • Dieqiao Feng
  • Carla P. Gomes
  • Bart Selman

Despite the success of practical solvers in various NP-complete domains such as SAT and CSP as well as using deep reinforcement learning to tackle two-player games such as Go, certain classes of PSPACE-hard planning problems have remained out of reach. Even carefully designed domain-specialized solvers can fail quickly due to the exponential search space on hard instances. Recent works that combine traditional search methods, such as best-first search and Monte Carlo tree search, with Deep Neural Networks' (DNN) heuristics have shown promising progress and can solve a significant number of hard planning instances beyond specialized solvers. To better understand why these approaches work, we studied the interplay of the policy and value networks of DNN-based best-first search on Sokoban and show the surprising effectiveness of the policy network, further enhanced by the value network, as a guiding heuristic for the search. To further understand the phenomena, we studied the cost distribution of the search algorithms and found that Sokoban instances can have heavy-tailed runtime distributions, with tails both on the left and right-hand sides. In particular, for the first time, we show the existence of \textit{left heavy tails} and propose an abstract tree model that can empirically explain the appearance of these tails. The experiments show the critical role of the policy network as a powerful heuristic guiding the search, which can lead to left heavy tails with polynomial scaling by avoiding exploring exponentially sized subtrees. Our results also demonstrate the importance of random restarts, as are widely used in traditional combinatorial solvers, for DNN-based search methods to avoid left and right heavy tails.

AAMAS Conference 2022 Conference Paper

Multi-Agent Curricula and Emergent Implicit Signaling

  • Niko A. Grupen
  • Daniel D. Lee
  • Bart Selman

Emergent communication has made strides towards learning communication from scratch, but has focused primarily on protocols that resemble human language. In nature, multi-agent cooperation gives rise to a wide range of communication that varies in structure and complexity. In this work, we recognize the full spectrum of communication that exists in nature and propose studying lower-level communication. Speci�cally, we study emergent implicit signaling in the context of decentralized multi-agent learning in di�cult, sparse reward environments. However, learning to coordinate in such environments is challenging. We propose a curriculum-driven strategy that combines: (i) velocity-based environment shaping, tailored to the skill level of the multi-agent team; and (ii) a behavioral curriculum that helps agents learn successful single-agent behaviors as a precursor to learning multi-agent behaviors. Pursuitevasion experiments show that our approach learns e�ective coordination, signi�cantly outperforming sophisticated analytical and learned policies. Our method completes the pursuit-evasion task even when pursuers move at half of the evader’s speed, whereas the highest-performing baseline fails at 80% of the evader’s speed. Moreover, we examine the use of implicit signals in coordination through position-based social in�uence. We show that pursuers trained with our strategy exchange more than twice as much information (in bits) than baseline methods, indicating that our method has learned, and relies heavily on, the exchange of implicit signals.

NeurIPS Conference 2020 Conference Paper

A Novel Automated Curriculum Strategy to Solve Hard Sokoban Planning Instances

  • Dieqiao Feng
  • Carla P. Gomes
  • Bart Selman

In recent years, we have witnessed tremendous progress in deep reinforcement learning (RL) for tasks such as Go, Chess, video games, and robot control. Nevertheless, other combinatorial domains, such as AI planning, still pose considerable challenges for RL approaches. The key difficulty in those domains is that a positive reward signal becomes {\em exponentially rare} as the minimal solution length increases. So, an RL approach loses its training signal. There has been promising recent progress by using a curriculum-driven learning approach that is designed to solve a single hard instance. We present a novel {\em automated} curriculum approach that dynamically selects from a pool of unlabeled training instances of varying task complexity guided by our {\em difficulty quantum momentum} strategy. We show how the smoothness of the task hardness impacts the final learning results. In particular, as the size of the instance pool increases, the ``hardness gap'' decreases, which facilitates a smoother automated curriculum based learning process. Our automated curriculum approach dramatically improves upon the previous approaches. We show our results on Sokoban, which is a traditional PSPACE-complete planning problem and presents a great challenge even for specialized solvers. Our RL agent can solve hard instances that are far out of reach for any previous state-of-the-art Sokoban solver. In particular, our approach can uncover plans that require hundreds of steps, while the best previous search methods would take many years of computing time to solve such instances. In addition, we show that we can further boost the RL performance with an intricate coupling of our automated curriculum approach with a curiosity-driven search strategy and a graph neural net representation.

IJCAI Conference 2020 Conference Paper

Solving Hard AI Planning Instances Using Curriculum-Driven Deep Reinforcement Learning

  • Dieqiao Feng
  • Carla Gomes
  • Bart Selman

Despite significant progress in general AI planning, certain domains remain out of reach of current AI planning systems. Sokoban is a PSPACE-complete planning task and represents one of the hardest domains for current AI planners. Even domain-specific specialized search methods fail quickly due to the exponential search complexity on hard instances. Our approach based on deep reinforcement learning augmented with a curriculum-driven method is the first one to solve hard instances within one day of training while other modern solvers cannot solve these instances within any reasonable time limit. In contrast to prior efforts, which use carefully handcrafted pruning techniques, our approach automatically uncovers domain structure. Our results reveal that deep RL provides a promising framework for solving previously unsolved AI planning problems, provided a proper training curriculum can be devised.

NeurIPS Conference 2018 Conference Paper

Understanding Batch Normalization

  • Nils Bjorck
  • Carla Gomes
  • Bart Selman
  • Kilian Weinberger

Batch normalization (BN) is a technique to normalize activations in intermediate layers of deep neural networks. Its tendency to improve accuracy and speed up training have established BN as a favorite technique in deep learning. Yet, despite its enormous success, there remains little consensus on the exact reason and mechanism behind these improvements. In this paper we take a step towards a better understanding of BN, following an empirical approach. We conduct several experiments, and show that BN primarily enables training with larger learning rates, which is the cause for faster convergence and better generalization. For networks without BN we demonstrate how large gradient updates can result in diverging loss and activations growing uncontrollably with network depth, which limits possible learning rates. BN avoids this problem by constantly correcting activations to be zero-mean and of unit standard deviation, which enables larger gradient steps, yields faster convergence and may help bypass sharp local minima. We further show various ways in which gradients and activations of deep unnormalized networks are ill-behaved. We contrast our results against recent findings in random matrix theory, shedding new light on classical initialization schemes and their consequences.

IJCAI Conference 2017 Conference Paper

XOR-Sampling for Network Design with Correlated Stochastic Events

  • Xiaojian Wu
  • Yexiang Xue
  • Bart Selman
  • Carla P. Gomes

Many network optimization problems can be formulated as stochastic network design problems in which edges are present or absent stochastically. Furthermore, protective actions can guarantee that edges will remain present. We consider the problem of finding the optimal protection strategy under a budget limit in order to maximize some connectivity measurements of the network. Previous approaches rely on the assumption that edges are independent. In this paper, we consider a more realistic setting where multiple edges are not independent due to natural disasters or regional events that make the states of multiple edges stochastically correlated. We use Markov Random Fields to model the correlation and define a new stochastic network design framework. We provide a novel algorithm based on Sample Average Approximation (SAA) coupled with a Gibbs or XOR sampler. The experimental results on real road network data show that the policies produced by SAA with the XOR sampler have higher quality and lower variance compared to SAA with Gibbs sampler.

NeurIPS Conference 2016 Conference Paper

Solving Marginal MAP Problems with NP Oracles and Parity Constraints

  • Yexiang Xue
  • Zhiyuan Li
  • Stefano Ermon
  • Carla Gomes
  • Bart Selman

Arising from many applications at the intersection of decision-making and machine learning, Marginal Maximum A Posteriori (Marginal MAP) problems unify the two main classes of inference, namely maximization (optimization) and marginal inference (counting), and are believed to have higher complexity than both of them. We propose XOR MMAP, a novel approach to solve the Marginal MAP problem, which represents the intractable counting subproblem with queries to NP oracles, subject to additional parity constraints. XOR MMAP provides a constant factor approximation to the Marginal MAP problem, by encoding it as a single optimization in a polynomial size of the original problem. We evaluate our approach in several machine learning and decision-making applications, and show that our approach outperforms several state-of-the-art Marginal MAP solvers.

ICML Conference 2016 Conference Paper

Variable Elimination in the Fourier Domain

  • Yexiang Xue
  • Stefano Ermon
  • Ronan LeBras
  • Carla P. Gomes
  • Bart Selman

The ability to represent complex high dimensional probability distributions in a compact form is one of the key insights in the field of graphical models. Factored representations are ubiquitous in machine learning and lead to major computational advantages. We explore a different type of compact representation based on discrete Fourier representations, complementing the classical approach based on conditional independencies. We show that a large class of probabilistic graphical models have a compact Fourier representation. This theoretical result opens up an entirely new way of approximating a probability distribution. We demonstrate the significance of this approach by applying it to the variable elimination algorithm. Compared with the traditional bucket representation and other approximate inference algorithms, we obtain significant improvements.

ICRA Conference 2016 Conference Paper

Watch-Bot: Unsupervised learning for reminding humans of forgotten actions

  • Chenxia Wu
  • Jiemi Zhang
  • Bart Selman
  • Silvio Savarese
  • Ashutosh Saxena

We present a robotic system that watches a human using a Kinect v2 RGB-D sensor, detects what he forgot to do while performing an activity, and if necessary reminds the person using a laser pointer to point out the related object. Our simple setup can be easily deployed on any assistive robot. Our approach is based on a learning algorithm trained in a purely unsupervised setting, which does not require any human annotations. This makes our approach scalable and applicable to variant scenarios. Our model learns the action/object co-occurrence and action temporal relations in the activity, and uses the learned rich relationships to infer the forgotten action and the related object. We show that our approach not only improves the unsupervised action segmentation and action cluster assignment performance, but also effectively detects the forgotten actions on a challenging human activity RGB-D video dataset. In robotic experiments, we show that our robot is able to remind people of forgotten actions successfully.

AAAI Conference 2015 Conference Paper

Pattern Decomposition with Complex Combinatorial Constraints: Application to Materials Discovery

  • Stefano Ermon
  • Ronan Le Bras
  • Santosh Suram
  • John Gregoire
  • Carla Gomes
  • Bart Selman
  • Robert van Dover

Identifying important components or factors in large amounts of noisy data is a key problem in machine learning and data mining. Motivated by a pattern decomposition problem in materials discovery, aimed at discovering new materials for renewable energy, e. g. for fuel and solar cells, we introduce CombiFD, a framework for factor based pattern decomposition that allows the incorporation of a-priori knowledge as constraints, including complex combinatorial constraints. In addition, we propose a new pattern decomposition algorithm, called AMIQO, based on solving a sequence of (mixed-integer) quadratic programs. Our approach considerably outperforms the state of the art on the materials discovery problem, scaling to larger datasets and recovering more precise and physically meaningful decompositions. We also show the effectiveness of our approach for enforcing background knowledge on other application domains.

IJCAI Conference 2015 Conference Paper

Uncovering Hidden Structure through Parallel Problem Decomposition for the Set Basis Problem: Application to Materials Discovery

  • Yexiang Xue
  • Stefano Ermon
  • Carla P. Gomes
  • Bart Selman

Exploiting parallelism is a key strategy for speeding up computation. However, on hard combinatorial problems, such a strategy has been surprisingly challenging due to the intricate variable interactions. We introduce a novel way in which parallelism can be used to exploit hidden structure of hard combinatorial problems. Our approach complements divide-and-conquer and portfolio approaches. We evaluate our approach on the minimum set basis problem: a core combinatorial problem with a range of applications in optimization, machine learning, and system security. We also highlight a novel sustainability related application, concerning the discovery of new materials for renewable energy sources such as improved fuel cell catalysts. In our approach, a large number of smaller sub-problems are identified and solved concurrently. We then aggregate the information from those solutions, and use this information to initialize the search of a global, complete solver. We show that this strategy leads to a substantial speed-up over a sequential approach, since the aggregated sub-problem solution information often provides key structural insights to the complete solver. Our approach also greatly outperforms state-of-the-art incomplete solvers in terms of solution quality. Our work opens up a novel angle for using parallelism to solve hard combinatorial problems.

AAAI Conference 2014 Conference Paper

Challenges in Materials Discovery – Synthetic Generator and Real Datasets

  • Ronan Le Bras
  • Richard Bernstein
  • John Gregoire
  • Santosh Suram
  • Carla Gomes
  • Bart Selman
  • R. Bruce van Dover

Newly-discovered materials have been central to recent technological advances. They have contributed significantly to breakthroughs in electronics, renewable energy and green buildings, and overall, have promoted the advancement of global human welfare. Yet, only a fraction of all possible materials have been explored. Accelerating the pace of discovery of materials would foster technological innovations, and would potentially address pressing issues in sustainability, such as energy production or consumption. The bottleneck of this discovery cycle lies, however, in the analysis of the materials data. As materials scientists have recently devised techniques to efficiently create thousands of materials and experimentalists have developed new methods and tools to characterize these materials, the limiting factor has become the data analysis itself. Hence, the goal of this paper is to stimulate the development of new computational techniques for the analysis of materials data, by bringing together the complimentary expertise of materials scientists and computer scientists. In collaboration with two major research laboratories in materials science, we provide the first publicly available dataset for the phase map identification problem. In addition, we provide a parameterized synthetic data generator to assess the quality of proposed approaches, as well as tools for data visualization and solution evaluation.

AAAI Conference 2014 Conference Paper

Designing Fast Absorbing Markov Chains

  • Stefano Ermon
  • Carla Gomes
  • Ashish Sabharwal
  • Bart Selman

Markov Chains are a fundamental tool for the analysis of real world phenomena and randomized algorithms. Given a graph with some specified sink nodes and an initial probability distribution, we consider the problem of designing an absorbing Markov Chain that minimizes the time required to reach a sink node, by selecting transition probabilities subject to some natural regularity constraints. By exploiting the Markovian structure, we obtain closed form expressions for the objective function as well as its gradient, which can be thus evaluated efficiently without any simulation of the underlying process and fed to a gradient-based optimization package. For the special case of designing reversible Markov Chains, we show that global optimum can be efficiently computed by exploiting convexity. We demonstrate how our method can be used for the evaluation and design of local search methods tailored for certain domains.

ICML Conference 2014 Conference Paper

Low-density Parity Constraints for Hashing-Based Discrete Integration

  • Stefano Ermon
  • Carla P. Gomes
  • Ashish Sabharwal
  • Bart Selman

In recent years, a number of probabilistic inference and counting techniques have been proposed that exploit pairwise independent hash functions to infer properties of succinctly defined high-dimensional sets. While providing desirable statistical guarantees, typical constructions of such hash functions are themselves not amenable to efficient inference. Inspired by the success of LDPC codes, we propose the use of low-density parity constraints to make inference more tractable in practice. While not strongly universal, we show that such sparse constraints belong to a new class of hash functions that we call Average Universal. These weaker hash functions retain the desirable statistical guarantees needed by most such probabilistic inference methods. Thus, they continue to provide provable accuracy guarantees while at the same time making a number of algorithms significantly more scalable in practice. Using this technique, we provide new, tighter bounds for challenging discrete integration and model counting problems.

IROS Conference 2014 Conference Paper

Synthesizing manipulation sequences for under-specified tasks using unrolled Markov Random Fields

  • Jaeyong Sung
  • Bart Selman
  • Ashutosh Saxena

Many tasks in human environments require performing a sequence of navigation and manipulation steps involving objects. In unstructured human environments, the location and configuration of the objects involved often change in unpredictable ways. This requires a high-level planning strategy that is robust and flexible in an uncertain environment. We propose a novel dynamic planning strategy, which can be trained from a set of example sequences. High level tasks are expressed as a sequence of primitive actions or controllers (with appropriate parameters). Our score function, based on Markov Random Field (MRF), captures the relations between environment, controllers, and their arguments. By expressing the environment using sets of attributes, the approach generalizes well to unseen scenarios. We train the parameters of our MRF using a maximum margin learning method. We provide a detailed empirical validation of our overall framework demonstrating successful plan strategies for a variety of tasks. 1

AAAI Conference 2014 Conference Paper

Uncovering Hidden Structure through Parallel Problem Decomposition

  • Yexiang Xue
  • Stefano Ermon
  • Carla Gomes
  • Bart Selman

A key strategy for speeding up computation is to run in parallel on multiple cores. However, on hard combinatorial problems, exploiting parallelism has been surprisingly challenging. It appears that traditional divide-and-conquer strategies do not work well, due to the intricate non-local nature of the interactions between the problem variables. In this paper, we introduce a novel way in which parallelism can be used to exploit hidden structure of hard combinatorial problems. We demonstrate the success of this approach on minimal set basis problem, which has a wide range of applications in machine learning and system security, etc. We also show the effectiveness on a related application problem from materials discovery. In our approach, a large number of smaller sub-problems are identified and solved concurrently. We then aggregate the information from those solutions, and use this to initialize the search of a global, complete solver. We show that this strategy leads to a significant speed-up over a sequential approach. The strategy also greatly outperforms state-of-the-art incomplete solvers in terms of solution quality. Our work opens up a novel angle for using parallelism to solve hard combinatorial problems.

IJCAI Conference 2013 Conference Paper

Crowdsourcing Backdoor Identification for Combinatorial Optimization

  • Ronan Le Bras
  • Richard Bernstein
  • Carla P. Gomes
  • Bart Selman
  • R. Bruce van Dover

We will show how human computation insights can be key to identifying so-called backdoor variables in combinatorial optimization problems. Backdoor variables can be used to obtain dramatic speedups in combinatorial search. Our approach leverages the complementary strength of human input, based on a visual identification of problem structure, crowdsourcing, and the power of combinatorial solvers to exploit complex constraints. We describe our work in the context of the domain of materials discovery. The motivation for considering the materials discovery domain comes from the fact that new materials can provide solutions for key challenges in sustainability, e. g. , in energy, new catalysts for more efficient fuel cell technology.

IJCAI Conference 2013 Conference Paper

Double-Wheel Graphs Are Graceful

  • Ronan Le Bras
  • Carla P. Gomes
  • Bart Selman

We present the first polynomial time construction procedure for generating graceful double-wheel graphs. A graph is graceful if its vertices can be labeled with distinct integer values from {0, .. ., e}, where e is the number of edges, such that each edge has a unique value corresponding to the absolute difference of its endpoints. Graceful graphs have a range of practical application domains, including in radio astronomy, X-ray crystallography, cryptography, and experimental design. Various families of graphs have been proven to be graceful, while others have only been conjectured to be. In particular, it has been conjectured that so-called double-wheel graphs are graceful. A double-wheel graph consists of two cycles of N nodes connected to a common hub. We prove this conjecture by providing the first construction for graceful double-wheel graphs, for any N > 3, using a framework that combines streamlined constraint reasoning with insights from human computation. We also use this framework to provide a polynomial time construction for diagonally ordered magic squares.

NeurIPS Conference 2013 Conference Paper

Embed and Project: Discrete Sampling with Universal Hashing

  • Stefano Ermon
  • Carla Gomes
  • Ashish Sabharwal
  • Bart Selman

We consider the problem of sampling from a probability distribution defined over a high-dimensional discrete set, specified for instance by a graphical model. We propose a sampling algorithm, called PAWS, based on embedding the set into a higher-dimensional space which is then randomly projected using universal hash functions to a lower-dimensional subspace and explored using combinatorial search methods. Our scheme can leverage fast combinatorial optimization tools as a blackbox and, unlike MCMC methods, samples produced are guaranteed to be within an (arbitrarily small) constant factor of the true probability distribution. We demonstrate that by using state-of-the-art combinatorial search tools, PAWS can efficiently sample from Ising grids with strong interactions and from software verification instances, while MCMC and variational methods fail in both cases.

UAI Conference 2013 Conference Paper

Optimization With Parity Constraints: From Binary Codes to Discrete Integration

  • Stefano Ermon
  • Carla P. Gomes
  • Ashish Sabharwal
  • Bart Selman

Many probabilistic inference tasks involve summations over exponentially large sets. Recently, it has been shown that these problems can be reduced to solving a polynomial number of MAP inference queries for a model augmented with randomly generated parity constraints. By exploiting a connection with max-likelihood decoding of binary codes, we show that these optimizations are computationally hard. Inspired by iterative message passing decoding algorithms, we propose an Integer Linear Programming (ILP) formulation for the problem, enhanced with new sparsification techniques to improve decoding performance. By solving the ILP through a sequence of LP relaxations, we get both lower and upper bounds on the partition function, which hold with high probability and are much tighter than those obtained with variational methods.

SAT Conference 2013 Conference Paper

Solutions for Hard and Soft Constraints Using Optimized Probabilistic Satisfiability

  • Marcelo Finger
  • Ronan LeBras
  • Carla P. Gomes
  • Bart Selman

Abstract Practical problems often combine real-world hard constraints with soft constraints involving preferences, uncertainties or flexible requirements. A probability distribution over the models that meet the hard constraints is an answer to such problems that is in the spirit of incorporating soft constraints. We propose a method using SAT-based reasoning, probabilistic reasoning and linear programming that computes such a distribution when soft constraints are interpreted as constraints whose violation is bound by a given probability. The method, called Optimized Probabilistic Satisfiability (oPSAT), consists of a two-phase computation of a probability distribution over the set of valuations of a SAT formula. Algorithms for both phases are presented and their complexity is discussed. We also describe an application of the oPSAT technique to the problem of combinatorial materials discovery.

ICML Conference 2013 Conference Paper

Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization

  • Stefano Ermon
  • Carla P. Gomes
  • Ashish Sabharwal
  • Bart Selman

Integration is affected by the curse of dimensionality and quickly becomes intractable as the dimensionality of the problem grows. We propose a randomized algorithm that, with high probability, gives a constant-factor approximation of a general discrete integral defined over an exponentially large set. This algorithm relies on solving only a small number of instances of a discrete combinatorial optimization problem subject to randomly generated parity constraints used as a hash function. As an application, we demonstrate that with a small number of MAP queries we can efficiently approximate the partition function of discrete graphical models, which can in turn be used, for instance, for marginal computation or model selection.

NeurIPS Conference 2012 Conference Paper

Density Propagation and Improved Bounds on the Partition Function

  • Stefano Ermon
  • Ashish Sabharwal
  • Bart Selman
  • Carla Gomes

Given a probabilistic graphical model, its density of states is a function that, for any likelihood value, gives the number of configurations with that probability. We introduce a novel message-passing algorithm called Density Propagation (DP) for estimating this function. We show that DP is exact for tree-structured graphical models and is, in general, a strict generalization of both sum-product and max-product algorithms. Further, we use density of states and tree decomposition to introduce a new family of upper and lower bounds on the partition function. For any tree decompostion, the new upper bound based on finer-grained density of state information is provably at least as tight as previously known bounds based on convexity of the log-partition function, and strictly stronger if a general condition holds. We conclude with empirical evidence of improvement over convex relaxations and mean-field based bounds.

AAAI Conference 2012 Conference Paper

From Streamlined Combinatorial Search to Efficient Constructive Procedures

  • Ronan Le Bras
  • Carla Gomes
  • Bart Selman

In recent years, significant progress in the area of search, constraint satisfaction, and automated reasoning has been driven in part by the study of challenge problems from combinatorics and finite algebra. This work has led to the discovery of interesting discrete structures with intricate mathematical properties. While some of those results have resolved open questions and conjectures, a shortcoming is that they generally do not provide further mathematical insights, from which one could derive more general observations. We propose an approach that integrates specialized combinatorial search, using so-called streamlining, with a human computation component. We use this approach to discover efficient constructive procedures for generating certain classes of combinatorial objects of any size. More specifically, using our framework, we discovered two complementary efficient constructions for generating so-called Spatially Balanced Latin squares (SBLS) of any order N, such that 2N+1 is prime. Previously constructions for SBLSs were not known. Our approach also enabled us to derive a new lower bound for socalled weak Schur numbers, improving on a series of earlier results for Schur numbers.

AAMAS Conference 2012 Conference Paper

Probabilistic Planning with Non-Linear Utility Functions and Worst-Case Guarantees

  • Stefano Ermon
  • Carla Gomes
  • Bart Selman
  • Alexander Vladimirsky

Markov Decision Processes are one of the most widely used frameworks to formulate probabilistic planning problems. Since planners are often risk-sensitive in high-stake situations, non-linear utility functions are often introduced to describe their preferences among all possible outcomes. Alternatively, risk-sensitive decision makers often require their plans to satisfy certain worst-case guarantees. We show how to combine these two approaches by considering problems where we maximize the expected utility of the total reward subject to worst-case constraints. We generalize several existing results on the structure of optimal policies to the constrained case, both for finite and infinite horizon problems. We provide a Dynamic Programming algorithm to compute the optimal policy, and we introduce an admissible heuristic to effectively prune the search space. Finally, we use a stochastic shortest path problem on large real-world road networks to demonstrate the practical applicability of our method.

SAT Conference 2012 Conference Paper

SMT-Aided Combinatorial Materials Discovery

  • Stefano Ermon
  • Ronan LeBras
  • Carla P. Gomes
  • Bart Selman
  • R. Bruce van Dover

Abstract In combinatorial materials discovery, one searches for new materials with desirable properties by obtaining measurements on hundreds of samples in a single high-throughput batch experiment. As manual data analysis is becoming more and more impractical, there is a growing need to develop new techniques to automatically analyze and interpret such data. We describe a novel approach to the phase map identification problem where we integrate domain-specific scientific background knowledge about the physical and chemical properties of the materials into an SMT reasoning framework. We evaluate the performance of our method on realistic synthetic measurements, and we show that it provides accurate and physically meaningful interpretations of the data, even in the presence of artificially added noise.

UAI Conference 2012 Conference Paper

Uniform Solution Sampling Using a Constraint Solver As an Oracle

  • Stefano Ermon
  • Carla P. Gomes
  • Bart Selman

We consider the problem of sampling from solutions defined by a set of hard constraints on a combinatorial space. We propose a new sampling technique that, while enforcing a uniform exploration of the search space, leverages the reasoning power of a systematic constraint solver in a black-box scheme. We present a series of challenging domains, such as energy barriers and highly asymmetric spaces, that reveal the difficulties introduced by hard constraints. We demonstrate that standard approaches such as Simulated Annealing and Gibbs Sampling are greatly affected, while our new technique can overcome many of these difficulties. Finally, we show that our sampling scheme naturally defines a new approximate model counting technique, which we empirically show to be very accurate on a range of benchmark problems.

ICRA Conference 2012 Conference Paper

Unstructured human activity detection from RGBD images

  • Jaeyong Sung
  • Colin Ponce
  • Bart Selman
  • Ashutosh Saxena

Being able to detect and recognize human activities is essential for several applications, including personal assistive robotics. In this paper, we perform detection and recognition of unstructured human activity in unstructured environments. We use a RGBD sensor (Microsoft Kinect) as the input sensor, and compute a set of features based on human pose and motion, as well as based on image and point-cloud information. Our algorithm is based on a hierarchical maximum entropy Markov model (MEMM), which considers a person's activity as composed of a set of sub-activities. We infer the two-layered graph structure using a dynamic programming approach. We test our algorithm on detecting and recognizing twelve different activities performed by four people in different environments, such as a kitchen, a living room, an office, etc. , and achieve good performance even when the person was not seen before in the training set. 1

IJCAI Conference 2011 Conference Paper

A Flat Histogram Method for Computing the Density of States of Combinatorial Problems

  • Stefano Ermon
  • Carla Gomes
  • Bart Selman

Consider a combinatorial state space S, such as the set of all truth assignments to N Boolean variables. Given a partition of S, we consider the problem of estimating the size of all the subsets in which S is divided. This problem, also known as computing the density of states, is quite general and has many applications. For instance, if we consider a Boolean formula in CNF and we partition according to the number of violated constraints, computing the density of states is a generalization of both SAT, MAXSAT and model counting. We propose a novel Markov Chain Monte Carlo algorithm to compute the density of states of Boolean formulas that is based on a flat histogram approach. Our method represents a new approach to a variety of inference, learning, and counting problems. We demonstrate its practical effectiveness by showing that the method converges quickly to an accurate solution on a range of synthetic and real-world instances.

AAMAS Conference 2011 Conference Paper

A Message Passing Approach To Multiagent Gaussian Inference for Dynamic Processes

  • Stefano Ermon
  • Carla Gomes
  • Bart Selman

In [1], we introduced a novel distributed inference algorithm for the multiagent Gaussian inference problem, based on the framework of graphical models and message passing algorithms. We compare it to current state of the art techniques and we demonstrate that it is the most efficient one in terms of communication resources used. Moreover, we show experimentally that it outperforms the other methods in terms of estimation error on a general class of problems, even in presence of data loss.

NeurIPS Conference 2011 Conference Paper

Accelerated Adaptive Markov Chain for Partition Function Computation

  • Stefano Ermon
  • Carla Gomes
  • Ashish Sabharwal
  • Bart Selman

We propose a novel Adaptive Markov Chain Monte Carlo algorithm to compute the partition function. In particular, we show how to accelerate a flat histogram sampling technique by significantly reducing the number of ``null moves'' in the chain, while maintaining asymptotic convergence properties. Our experiments show that our method converges quickly to highly accurate solutions on a range of benchmark instances, outperforming other state-of-the-art methods such as IJGP, TRW, and Gibbs sampling both in run-time and accuracy. We also show how obtaining a so-called density of states distribution allows for efficient weight learning in Markov Logic theories.

SAT Conference 2011 Conference Paper

Applying UCT to Boolean Satisfiability

  • Alessandro Previti
  • Raghuram Ramanujan
  • Marco Schaerf
  • Bart Selman

Abstract In this paper we perform a preliminary investigation into the application of sampling-based search algorithms to satisfiability testing of propositional formulas in Conjunctive Normal Form (CNF). In particular, we adapt the Upper Confidence bounds applied to Trees (UCT) algorithm [5] which has been successfully used in many game playing programs including MoGo, one of the strongest computer Go players [3].

IJCAI Conference 2011 Conference Paper

Risk-Sensitive Policies for Sustainable Renewable Resource Allocation

  • Stefano Ermon
  • Jon Conrad
  • Carla Gomes
  • Bart Selman

Markov Decision Processes arise as a natural model for many renewable resources allocation problems. In many such problems, high stakes decisions with potentially catastrophic outcomes (such as the collapse of an entire ecosystem) need to be taken by carefully balancing social, economic, and ecologic goals. We introduce a broad class of such MDP models with a risk averse attitude of the decision maker, in order to obtain policies that are more balanced with respect to the welfare of future generations. We prove that they admit a closed form solution that can be efficiently computed. We show an application of the proposed framework to the Pacific Halibut marine fishery, obtaining new and more cautious policies. Our results strengthen findings of related policies from the literature by providing new evidence that a policy based on periodic closures of the fishery should be employed, in place of the one traditionally used that harvests a constant proportion of the stock every year.

ICAPS Conference 2011 Conference Paper

Trade-Offs in Sampling-Based Adversarial Planning

  • Raghuram Ramanujan
  • Bart Selman

The Upper Confidence bounds for Trees (UCT) algorithm has in recent years captured the attention of the planning and game-playing community due to its notable success in the game of Go. However, attempts to reproduce similar levels of performance in domains that are the forte of Minimax-style algorithms have been largely unsuccessful, making any comparative studies of the two hard. In this paper, we study UCT in the game of Mancala, which to our knowledge is the first domain where both search algorithms perform quite well with minimal enhancement. We focus on the three key components of the UCT algorithm in its purest form - targeted node expansion, state value estimation via playouts and averaging backups - and look at their contributions to the overall performance of the algorithm. We study the trade-offs involved in using alternate ways to perform these steps. Finally, we demonstrate a novel hybrid approach to enhancing UCT, that exploits its superior decision accuracy in regions of the search space with few terminal nodes.

SAT Conference 2010 Conference Paper

An Empirical Study of Optimal Noise and Runtime Distributions in Local Search

  • Lukas Kroc
  • Ashish Sabharwal
  • Bart Selman

Abstract This paper presents a detailed empirical study of local search for Boolean satisfiability (SAT), highlighting several interesting properties, some of which were previously unknown or had only anecdotal evidence. Specifically, we study hard random 3-CNF formulas and provide surprisingly simple analytical fits for the optimal (static) noise level and the runtime at optimal noise, as a function of the clause-to-variable ratio. We also demonstrate, for the first time for local search, a power-law decay in the tail of the runtime distribution in the low noise regime. Finally, we discuss a Markov Chain model capturing this intriguing feature.

AAMAS Conference 2010 Conference Paper

Collaborative Multiagent Gaussian Inference in a Dynamic Environment Using Belief Propagation

  • Stefano Ermon
  • Carla Gomes
  • Bart Selman

The problem of multiagent Gaussian inference in a dynamicenvironment, also known as distributed Kalman filtering, is formulated into the framework of message passing algorithms. Upon generalizing the derivation of the standardKalman filter to the distributed case, we propose novel solutions that outperform current state of the art techniques.

ICAPS Conference 2010 Conference Paper

On Adversarial Search Spaces and Sampling-Based Planning

  • Raghuram Ramanujan
  • Ashish Sabharwal
  • Bart Selman

Upper Confidence bounds applied to Trees (UCT), a bandit-based Monte-Carlo sampling algorithm for planning, has recently been the subject of great interest in adversarial reasoning. UCT has been shown to outperform traditional minimax based approaches in several challenging domains such as Go and Kriegspiel, although minimax search still prevails in other domains such as Chess. This work provides insights into the properties of adversarial search spaces that play a key role in the success or failure of UCT and similar sampling-based approaches. We show that certain "early loss" or "shallow trap" configurations, while unlikely in Go, occur surprisingly often in games like Chess (even in grandmaster games). We provide evidence that UCT, unlike minimax search, is unable to identify such traps in Chess and spends a great deal of time exploring much deeper game play than needed.

UAI Conference 2010 Conference Paper

Playing games against nature: optimal policies for renewable resource allocation

  • Stefano Ermon
  • Jon Conrad
  • Carla P. Gomes
  • Bart Selman

In this paper we introduce a class of Markov decision processes that arise as a natural model for many renewable resource allocation problems. Upon extending results from the inventory control literature, we prove that they admit a closed form solution and we show how to exploit this structure to speed up its computation. We consider the application of the proposed framework to several problems arising in very different domains, and as part of the ongoing effort in the emerging field of Computational Sustainability we discuss in detail its application to the Northern Pacific Halibut marine fishery. Our approach is applied to a model based on real world data, obtaining a policy with a guaranteed lower bound on the utility function that is structurally very different from the one currently employed.

UAI Conference 2010 Conference Paper

Understanding Sampling Style Adversarial Search Methods

  • Raghuram Ramanujan
  • Ashish Sabharwal
  • Bart Selman

UCT has recently emerged as an exciting new adversarial reasoning technique based on cleverly balancing exploration and exploitation in a Monte-Carlo sampling setting. It has been particularly successful in the game of Go but the reasons for its success are not well understood and attempts to replicate its success in other domains such as Chess have failed. We provide an in-depth analysis of the potential of UCT in domain-independent settings, in cases where heuristic values are available, and the effect of enhancing random playouts to more informed playouts between two weak minimax players. To provide further insights, we develop synthetic game tree instances and discuss interesting properties of UCT, both empirically and analytically.

IJCAI Conference 2009 Conference Paper

  • Lukas Kroc
  • Ashish Sabharwal
  • Carla P. Gomes
  • Bart Selman

Systematic search and local search paradigms for combinatorial problems are generally believed to have complementary strengths. Nevertheless, attempts to combine the power of the two paradigms have had limited success, due in part to the expensive information communication overhead involved. We propose a hybrid strategy based on shared memory, ideally suited for multi-core processor architectures. This method enables continuous information exchange between two solvers without slowing down either of the two. Such a hybrid search strategy is surprisingly effective, leading to substantially better quality solutions to many challenging Maximum Satisfiability (MaxSAT) instances than what the current best exact or heuristic methods yield, and it often achieves this within seconds. This hybrid approach is naturally best suited to MaxSAT instances for which proving unsatisfiability is already hard; otherwise the method falls back to pure local search.

SAT Conference 2009 Conference Paper

Relaxed DPLL Search for MaxSAT

  • Lukas Kroc
  • Ashish Sabharwal
  • Bart Selman

Abstract We propose a new incomplete algorithm for the Maximum Satisfiability (MaxSAT) problem on unweighted Boolean formulas, focused specifically on instances for which proving unsatisfiability is already computationally difficult. For such instances, our approach is often able to identify a small number of what we call “bottleneck” constraints, in time comparable to the time it takes to prove unsatisfiability. These bottleneck constraints can have useful semantic content. Our algorithm uses a relaxation of the standard backtrack search for satisfiability testing (SAT) as a guiding heuristic, followed by a low-noise local search when needed. This allows us to heuristically exploit the power of unit propagation and clause learning. On a test suite consisting of all unsatisfiable industrial instances from SAT Race 2008, our solver, RelaxedMinisat, is the only (MaxSAT) solver capable of identifying a single bottleneck constraint in all but one instance.

NeurIPS Conference 2008 Conference Paper

Counting Solution Clusters in Graph Coloring Problems Using Belief Propagation

  • Lukas Kroc
  • Ashish Sabharwal
  • Bart Selman

We show that an important and computationally challenging solution space feature of the graph coloring problem (COL), namely the number of clusters of solutions, can be accurately estimated by a technique very similar to one for counting the number of solutions. This cluster counting approach can be naturally written in terms of a new factor graph derived from the factor graph representing the COL instance. Using a variant of the Belief Propagation inference framework, we can efficiently approximate cluster counts in random COL problems over a large range of graph densities. We illustrate the algorithm on instances with up to 100, 000 vertices. Moreover, we supply a methodology for computing the number of clus- ters exactly using advanced techniques from the knowledge compilation literature. This methodology scales up to several hundred variables.

IJCAI Conference 2007 Conference Paper

  • J
  • ouml; rg Hoffmann
  • Carla Gomes
  • Bart Selman
  • Henry Kautz

Translation to Boolean satisfiability is an important approach for solving state-space reachability problems that arise in planning and verification. Many important problems, however, involve numeric variables; for example, C programs or planning with resources. Focussing on planning, we propose a method for translating such problems into propositional SAT, based on an approximation of reachable variable domains. We compare to a more direct translation into "SAT modulo theory" (SMT), that is, SAT extended with numeric variables and arithmetic constraints. Though translation to SAT generates much larger formulas, we show that it typically outperforms translation to SMT almost up to the point where the formulas don't fit into memory any longer. We also show that, even though our planner is optimal, it tends to outperform state-of-the-art sub-optimal heuristic planners in domains with tightly constrained resources. Finally we present encouraging initial results on applying the approach to model checking.

IJCAI Conference 2007 Conference Paper

  • Ioannis A. Vetsikas
  • Nicholas R. Jennings
  • Bart Selman

This paper presents a methodology for designing trading agents for complex games. We compute, for the first time, Bayes-Nash equilibria for first-price single-unit auctions and mth-price multi-unit auctions, when the auction has a set of possible closing times, one of which is chosen randomly for the auction to end at. To evaluate this approach we used our analysis to generate strategies for the International Trading Agent Competition. One of these was evaluated as the best overall and was subsequently used very successfully by our agent WhiteBear in the 2005 competition.

IJCAI Conference 2007 Conference Paper

  • Carla P. Gomes
  • Joerg Hoffmann
  • Ashish Sabharwal
  • Bart Selman

We introduce a new technique for counting models of Boolean satisfiability problems. Our approach incorporates information obtained from sampling the solution space. Unlike previous approaches, our method does not require uniform or near-uniform samples. It instead converts local search sampling without any guarantees into very good bounds on the model count with guarantees. We give a formal analysis and provide experimental results showing the effectiveness of our approach.

SAT Conference 2007 Conference Paper

Short XORs for Model Counting: From Theory to Practice

  • Carla P. Gomes
  • Jörg Hoffmann 0001
  • Ashish Sabharwal
  • Bart Selman

Abstract A promising approach for model counting was recently introduced, which in theory requires the use of large random xor or parity constraints to obtain near-exact counts of solutions to Boolean formulas. In practice, however, short xor constraints are preferred as they allow better constraint propagation in SAT solvers. We narrow this gap between theory and practice by presenting experimental evidence that for structured problem domains, very short xor constraints can lead to probabilistic variance as low as large xor constraints, and thus provide the same correctness guarantees. We initiate an understanding of this phenomenon by relating it to structural properties of synthetic instances.

UAI Conference 2007 Conference Paper

Survey Propagation Revisited

  • Lukas Kroc
  • Ashish Sabharwal
  • Bart Selman

Survey propagation (SP) is an exciting new technique that has been remarkably successful at solving very large hard combinatorial problems, such as determining the satisfiability of Boolean formulas. In a promising attempt at understanding the success of SP, it was recently shown that SP can be viewed as a form of belief propagation, computing marginal probabilities over certain objects called covers of a formula. This explanation was, however, shortly dismissed by experiments suggesting that non-trivial covers simply do not exist for large formulas. In this paper, we show that these experiments were misleading: not only do covers exist for large hard random formulas, SP is surprisingly accurate at computing marginals over these covers despite the existence of many cycles in the formulas. This re-opens a potentially simpler line of reasoning for understanding SP, in contrast to some alternative lines of explanation that have been proposed assuming covers do not exist.

NeurIPS Conference 2006 Conference Paper

Near-Uniform Sampling of Combinatorial Spaces Using XOR Constraints

  • Carla Gomes
  • Ashish Sabharwal
  • Bart Selman

We propose a new technique for sampling the solutions of combinatorial problems in a near-uniform manner. We focus on problems specified as a Boolean formula, i. e. , on SAT instances. Sampling for SAT problems has been shown to have interesting connections with probabilistic reasoning, making practical sampling algorithms for SAT highly desirable. The best current approaches are based on Markov Chain Monte Carlo methods, which have some practical limitations. Our approach exploits combinatorial properties of random parity (X O R) constraints to prune away solutions near-uniformly. The final sample is identified amongst the remaining ones using a state-of-the-art SAT solver. The resulting sampling distribution is provably arbitrarily close to uniform. Our experiments show that our technique achieves a significantly better sampling quality than the best alternative.

SAT Conference 2006 Conference Paper

QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency

  • Ashish Sabharwal
  • Carlos Ansótegui
  • Carla P. Gomes
  • Justin W. Hart
  • Bart Selman

Abstract Quantified Boolean Formulas (QBFs) present the next big challenge for automated propositional reasoning. Not surprisingly, most of the present day QBF solvers are extensions of successful propositional satisfiability algorithms (SAT solvers). They directly integrate the lessons learned from SAT research, thus avoiding re-inventing the wheel. In particular, they use the standard conjunctive normal form (CNF) augmented with layers of variable quantification for modeling tasks as QBF. We argue that while CNF is well suited to “existential reasoning” as demonstrated by the success of modern SAT solvers, it is far from ideal for “universal reasoning” needed by QBF. The CNF restriction imposes an inherent asymmetry in QBF and artificially creates issues that have led to complex solutions, which, in retrospect, were unnecessary and sub-optimal. We take a step back and propose a new approach to QBF modeling based on a game-theoretic view of problems and on a dual CNF-DNF (disjunctive normal form) representation that treats the existential and universal parts of a problem symmetrically. It has several advantages: (1) it is generic, compact, and simpler, (2) unlike fully non-clausal encodings, it preserves the benefits of pure CNF and leverages the support for DNF already present in many QBF solvers, (3) it doesn’t use the so-called indicator variables for conversion into CNF, thus circumventing the associated illegal search space issue, and (4) our QBF solver based on the dual encoding ( Duaffle ) consistently outperforms the best solvers by two orders of magnitude on a hard class of benchmarks, even without using standard learning techniques.

ICAPS Conference 2006 Conference Paper

Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning

  • Jörg Hoffmann 0001
  • Carla P. Gomes
  • Bart Selman

In AI Planning, as well as Verification, a successful method is to compile the application into boolean satisfiability (SAT), and solve it with state-of-the-art DPLL-based procedures. There is a lack of formal understanding why this works so well. Focussing on the Planning context, we identify a form of problem structure concerned with the symmetrical or asymmetrical nature of the cost of achieving the individual planning goals. We quantify this sort of structure with a simple numeric parameter called AsymRatio, ranging between 0 and 1. We show empirically that AsymRatio correlates strongly with SAT solver performance in a broad range of Planning benchmarks, including the domains used in the 3rd International Planning Competition. We then examine carefully crafted synthetic planning domains that allow to control the amount of structure, and that are clean enough for a rigorous analysis of the combinatorial search space. The domains are parameterized by size n, and by a structure parameter k, so that AsymRatio is asymptotic to k/n. The CNFs we examine are unsatisfiable, encoding one planning step less than the length of the optimal plan. We prove upper and lower bounds on the size of the best possible DPLL refutations, under different settings of k, as a function of n. We also identify the best possible sets of branching variables (backdoors). With minimum AsymRatio, we prove exponential lower bounds, and identify minimal backdoors of size linear in the number of variables. With maximum AsymRatio, we identify logarithmic DPLL refutations (and backdoors), showing a doubly exponential gap between the two structural extreme cases. This provides a concrete insight into the practical efficiency of modern SAT solvers.

SAT Conference 2005 Conference Paper

A New Approach to Model Counting

  • Wei Wei 0040
  • Bart Selman

Abstract We introduce ApproxCount, an algorithm that approximates the number of satisfying assignments or models of a formula in propositional logic. Many AI tasks, such as calculating degree of belief and reasoning in Bayesian networks, are computationally equivalent to model counting. It has been shown that model counting in even the most restrictive logics, such as Horn logic, monotone CNF and 2CNF, is intractable in the worst-case. Moreover, even approximate model counting remains a worst-case intractable problem. So far, most practical model counting algorithms are based on backtrack style algorithms such as the DPLL procedure. These algorithms typically yield exact counts but are limited to relatively small formulas. Our ApproxCount algorithm is based on SampleSat, a new algorithm that samples from the solution space of a propositional logic formula near-uniformly. We provide experimental results for formulas from a variety of domains. The algorithm produces good estimates for formulas much larger than those that can be handled by existing algorithms.

SAT Conference 2004 Conference Paper

From Spin Glasses to Hard Satisfiable Formulas

  • Haixia Jia
  • Cristopher Moore
  • Bart Selman

We introduce a highly structured family of hard satisfiable 3-SAT formulas corresponding to an ordered spin-glass model from statistical physics. This model has provably “glassy” behavior; that is, it has many local optima with large energy barriers between them, so that local search algorithms get stuck and have difficulty finding the true ground state, i.e., the unique satisfying assignment. We test the hardness of our formulas with two complete Davis-Putnam solvers, Satz and zChaff, and two incomplete solvers, WalkSAT and the recently introduced Survey Propagation algorithm SP. We compare our formulas to random XOR-SAT formulas and to two other generators of hard satisfiable instances, the minimum disagreement parity formulas of Crawford et al., and Hirsch’s hgen2. For the complete solvers √ the running time of our formulas grows exponentially in n, and exceeds that of random XOR-SAT formulas for small problem sizes. More interestingly, our formulas appear to be harder for WalkSAT than any other known generator of satisfiable instances.

IJCAI Conference 2003 Conference Paper

Backdoors To Typical Case Complexity

  • Ryan Williams
  • Carla P. Gomes
  • Bart Selman

There has been significant recent progress in reasoning and constraint processing methods. In areas such as planning and finite model-checking, current solution techniques can handle combinatorial problems with up to a million variables and five million constraints. The good scaling behavior of these methods appears to defy what one would expect based on a worst-case complexity analysis. In order to bridge this gap between theory and practice, we propose a new framework for studying the complexity of these techniques on practical problem instances. In particular, our approach incorporates general structural properties observed in practical problem instances into the formal complexity analysis. We introduce a notion of "backdoors", which are small sets of variables that capture the overall combinatorics of the problem instance. We provide empirical results showing the existence of such backdoors in real-world problems. We then present a series of complexity results that explain the good scaling behavior of current reasoning and constraint methods observed on practical problem instances.

IJCAI Conference 2003 Conference Paper

Sampling Combinatorial Spaces Using Biased Random Walks

  • Jordan Erenrich
  • Bart Selman

For probabilistic reasoning, one often needs to sample from a combinatorial space. For example, one may need to sample uniformly from the space of all satisfying assignments. Can state-of-the-art search procedures for SAT be used to sample effectively from the space of all solutions? And, if so, how uniformly do they sample? Our initial results find that on the positive side, one can find all solutions to a given instance. Nevertheless, sampling can be highly biased. This research provides a starting point for the development of more balanced procedures.

UAI Conference 2001 Conference Paper

A Bayesian Approach to Tackling Hard Computational Problems

  • Eric Horvitz
  • Yongshao Ruan
  • Carla P. Gomes
  • Henry A. Kautz
  • Bart Selman
  • Max Chickering

We are developing a general framework for using learned Bayesian models for decision-theoretic control of search and reasoningalgorithms. We illustrate the approach on the specific task of controlling both general and domain-specific solvers on a hard class of structured constraint satisfaction problems. A successful strategyfor reducing the high (and even infinite) variance in running time typically exhibited by backtracking search algorithms is to cut off and restart the search if a solution is not found within a certainamount of time. Previous work on restart strategies have employed fixed cut off values. We show how to create a dynamic cut off strategy by learning a Bayesian model that predicts the ultimate length of a trial based on observing the early behavior of the search algorithm. Furthermore, we describe the general conditions under which a dynamic restart strategy can outperform the theoretically optimal fixed strategy.

AAAI Conference 1999 Conference Paper

Control Knowledge in Planning: Benefits and Tradeoffs

  • Yi-Cheng Huang
  • Bart Selman
  • Cornell University; Henry Kautz
  • AT
  • T Labs - Research

Recent newplanning paradigms, such as Graphplan and Satplan, have been shownto outperform moretraditional domain-independentplanners. Aninteresting aspect of these planners is that they do not incorporate domainspecific control knowledge, but instead rely on efficient graph-basedor propositional representations and advancedsearch techniques. Analternative approach has been proposed in the TLPlansystem. TLPlanis an exampleof a powerful planner incorporating declarative control specified in temporal logic formulas. Weshowhowthese control rules can be parsed into Satplan. Ourempirical results showup to an order of magnitudespeed up. Wealso provide a detailed comparison with TLPlan, and showhowthe search strategies in TLPlanlead to efficient plans in terms of the numberof actions but with little or no parallelism. The Satplan and Graphplan formalisms on the other hand do find highly parallel plans, but are less effective in sequential domains. Ourresults enhanceour understandingof the various tradeoffs in planning technology, and extend earlier workon control knowledgein the Satplan frameworkby Ernst et a/. (1997) and Kautz and Selman(1998).

IJCAI Conference 1999 Conference Paper

Unifying SAT-based and Graph-based Planning

  • Henry Kautz
  • Bart Selman

The B l a c k b o x planning system unifies the planning as satisfiability framework (Kautz and Selman 1992, 1996) with the plan graph approach to STRIPS planning (Blum and Furst 1995). We show that STRIPS problems can be directly translated into SAT and efficiently solved using new randomized systematic solvers. For certain computationally challenging benchmark problems this unified approach outperforms both SATPLAN and Graphplan alone. We also demonstrate that polynomialtime SAT simplification algorithms applied to the encoded problem instances are a powerful complement to the "mutex" propagation algorithm that works directly on the plan graph.

ICAPS Conference 1998 Conference Paper

Randomization in Backtrack Search: Exploiting Heavy-Tailed Profiles for Solving Hard Scheduling Problems

  • Carla P. Gomes
  • Bart Selman
  • Ken McAloon
  • Carol Tretkoff

We studytheruntime profiles ofcomplete backtrackstylesearch methods applied to hardscheduling problems. Suchsearch methods oftenexhibit a largevariability in performance dueto thenon-standard nature oftheirunderlying costdistributions. Thedistributions generally exhibit verylongtails or"heavy tails" andarebestcharacterized bya general class ofdistributions thathavenomoments (i. e., aninfinite mean, variance, etc.). Weshowhowonecanexploit thespecialnature ofsuchdistributions tosignificantly improveupon deterministic complete search procedures.

ICAPS Conference 1998 Conference Paper

The Role of Domain-Specific Knowledge in the Planning as Satisfiability Framework

  • Henry A. Kautz
  • Bart Selman

SATPLAN is currently one of the fastest planning systems for domain-independentplanning. In nearly all practical applications, however, there exists an abundance of domain-specific knowledgethat can be used to improve the performanceof a planning system. This knowledgeis traditionally encoded as procedures or rules that are tied to the details of the planning engine. Wepresent a way to encode domain knowledge in a purely declarative, algorithm independentmanner. Wedemonstrate that the same heuristic knowledgecan be used by completelydifferent search engines, one systematic, the other using greedy local search. This approach greatly enhances the power of SATPLAN: solution times for someproblems are reduced fxomdays to seconds. problem log. a log. b log. c log. d bw. a bw. b bw. c bw. d sob length 11 13 13 14 6 9 14 18 soln size 54 47 63 74 12 18 28 36 as configurations TM 10 sl0 l° 10 1016 110--0-~ 1091 1013[ I019 J Table 1: Planning benchmark testbed. For logistics problems, the solution length is optimal, and the number of actions per solution is the smallest that has been found using any search procedure so far. For the blocks world (one arm), the solution length and sizes are optimal (each time step includes a pickup/putdown pair).

UAI Conference 1997 Conference Paper

Algorithm Portfolio Design: Theory vs. Practice

  • Carla P. Gomes
  • Bart Selman

Stochastic algorithms are among the best for solving computationally hard search and reasoning problems. The runtime of such procedures is characterized by a random variable. Different algorithms give rise to different probability distributions. One can take advantage of such differences by combining several algorithms into a portfolio, and running them in parallel or interleaving them on a single processor. We provide a detailed evaluation of the portfolio approach on distributions of hard combinatorial search problems. We show under what conditions the protfolio approach can have a dramatic computational advantage over the best traditional methods.

AAAI Conference 1996 Conference Paper

Challenge Problems for Artificial Intelligence

  • Bart Selman
  • Thomas Dean
  • Tom M. Mitchell

AI textbooks and papers often discuss the big questions, such as "how to reason with uncertainty", "how to reason efficiently", or "how to improve performance through learning ." It is more difficult, however, to find descriptions of concrete problems or challenges that are still ambitious and interesting, yet not so open-ended. The goal of this panel is to formulate a set of such challenge problems for the field. Each panelist was asked to formulate one or more challenges. The emphasis is on problems for which there is a good chance that they will be resolved within the next five to ten years.

AAAI Conference 1994 Conference Paper

Noise Strategies for Improving Local Search

  • Bart Selman

It has recently been shown that local search is surprisingly good at f? inding satisfying assignments for certain computationally hard classes of CNF formulas. The performance of basic local search methods can be further enhanced by introducing mechanisme for escaping from local minima in the search space. We will compare three such mechanisms: simulated annealing, random noise, and a strategy called “mixed random walk”. We show that mixed random walk is the superior strategy. We also present results demonstrating the effectiveness of local search with walk for solving circuit ByntheBiB and circuit diagnosis problems. Finally, we demonstrate that mixed random walk improves upon the best known methods for solving MAX-SAT problems.

AAAI Conference 1993 Conference Paper

An Empirical Study of Greedy Local Search for Satisfiability Testing

  • Bart Selman

GSAT is a randomized local search procedure for solving propositional satisfiability problems. GSAT can solve hard, randomly generated problems that are an order of magnitude larger than those that can be handled by more traditional approaches, such as the Davis- Putnam procedure. This paper presents the results of numerous experiments we have performed with GSAT, in order to improve our understanding of its capabilities and limitations. We first characterize the space traversed by GSAT. We will see that for nearly all problem classes we have encountered, the space consists of a steep descent followed by broad flat plateaus. We then compare GSAT with simulated annealing, and show how GSAT can be viewed as an efficient method for executing the lowtemperature tail of an annealing schedule. Finally, we report on extensions to the basic GSAT procedure. We discuss two general, domain-independent extensions that dramatically improve GSAT’ s performance on structured problems: the use of clause weights, and a way to average in near-solutions when initializing the procedure before each try.

IJCAI Conference 1993 Conference Paper

Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems

  • Bart Selman
  • Henry Kautz

GSAT is a randomized local search procedure for solving propositional satisfiability problems (Selman et al. 1992). GSAT can solve hard, randomly generated problems that are an order of magnitude larger than those that can be handled by more traditional approaches such as the Davis-Putnam procedure. GSAT also efficiently solves encodings of graph coloring problems, N-queens, and Boolean induction. However, GSAT does not perform as well on handcrafted encodings of blocks-world planning problems and formulas with a high degree of asymmetry. We present three strategies that dramatically improve GSAT's performance on such formulas. These strategies, in effect, manage to uncover hidden structure in the formula under considerations, thereby significantly extending the applicability of the GSAT algorithm.

AAAI Conference 1992 Conference Paper

A New Method for Solving Hard Satisfiability Problems

  • Bart Selman

We introduce a greedy local search procedure called GSAT for solving propositional satisfiability problems. Our experiments show that this procedure can be used to solve hard, randomly generated problems that are an order of magnitude larger than those that can be handled by more traditional approaches such as the Davis-Putnam procedure or resolution. We also show that GSAT can solve structured satisfiability problems quickly. In particular, we solve encodings of graph coloring problems, N-queens, and Boolean induction. General application strategies and limitations of the approach are also discussed. GSAT is best viewed as a model-finding procedure. Its good performance suggests that it may be advantageous to reformulate reasoning tasks that have traditionally been viewed as theorem-proving problems as model-finding tasks.

AAAI Conference 1991 Conference Paper

Knowledge Compilation Using Horn Approximations

  • Bart Selman

We present a new approach to developing fast and efficient knowledge representation systems. Previous approaches to the problem of tractable inference have used restricted languages or incomplete inference mechanisms - problems include lack of expressive power, lack of inferential power, and/or lack of a formal characterization of what can and cannot be inferred. To overcome these disadvantages, we introduce a knowledge compilation method. We allow the user to enter statements in a general, unrestricted representation language, which the system compiles into a restricted language that allows for efficient inference. Since an exact translation into a tractable form is often impossible, the system searches for the best approximation of the original information. We will describe how the approximation can be used to speed up inference without giving up correctness or completeness. We illustrate our method by studying the approximation of logical theories by Horn theories. Following the formal definition of Horn approximation, we present “anytime” algorithms for generating such approximations. We subsequently discuss extensions to other useful classes of approximations.

AAAI Conference 1990 Conference Paper

Abductive and Default Reasoning: A Computational Core

  • Bart Selman

Of all the possible ways of computing abductive explanations, the ATMS procedure is one of the most popular. While this procedure is known to run in exponential time in the worst case, the proof actually depends on the existence of queries with an exponential number of answers. But how much of the difficulty stems from having to return these large sets of explanations? Here we explore abduction tasks similar to that of the ATMS, but which return relatively small answers. The main result is that although it is possible to generate some non-trivial explanations quickly, deciding if there is an explanation containing a given hypothesis is NPhard, as is the task of generating even one explanation expressed in terms of a given set of assumption letters. Thus, the method of simply listing all explanations, as employed by the ATMS, probably cannot be improved upon. An interesting result of our analysis is the discovery of a subtask that is at the core of generating explanations, and is also at the core of generating extensions in Reiter’ s default logic. Moreover, it is this subtask that accounts for the computational difficulty of both forms of reasoning. This establishes for the first time a strong connection between computing abductive explanations and computing extensions in default logic.

NMR Workshop 1989 Conference Paper

The Complexity of Model-Preference Default Theories

  • Bart Selman
  • Henry A. Kautz

Abstract Most formal theories of default inference have very poor computational properties, and are easily shown to be intractable, or worse, undecidable. We are therefore investigating limited but efficiently computable theories of default reasoning. This paper defines systems of Propositional Model Preference Defaults, which provide a true model-theoretic account of default inference with exceptions. Some of our results extend to other nonmonotonic formalisms, such as Default Logic. The most general system of Model Preference Defaults is decidable but still intractable. Inspired by the very good (linear) complexity of propositional Horn theories, we consider systems of Horn Defaults. Surprisingly, finding a most-preferred model in even this very limited system is shown to be NP-Hard. Tractability can be achieved in two ways: by eliminating the “specificity ordering” among default rules, thus limiting the system's expressive power; and by restricting our attention to systems of Acyclic Horn Defaults. These acyclic theories can encode inheritance hierarchies of the form examined by Touretzky, but are strictly more general. This analysis suggests several directions for future research: finding other syntactic restrictions which permit efficient computation; or more daringly, investigation of default systems whose implementations do not require checking global consistency — that is, fast “approximate” inference.