Ashish Sabharwal

Papers

2018

• Question Answering as Global Reasoning over Semantic Abstractions

  Daniel Khashabi, Tushar Khot, Ashish Sabharwal, and Dan RothAAAI 2018

  We propose a novel method for exploiting the semantic structure of text to answer multiple-choice questions. The approach is especially suitable for domains that require reasoning over a diverse set of linguistic constructs but have limited training data. To address these challenges, we present the first system, to the best of our knowledge, that reasons over a wide range of semantic abstractions of the text, which are derived using off-the-shelf, general-purpose, pre-trained natural language modules such as semantic role labelers, coreference resolvers, and dependency parsers. Representing multiple abstractions as a family of graphs, we translate question answering (QA) into a search for an optimal subgraph that satisfies certain global and local properties. This formulation generalizes several prior structured QA systems. Our system, SEMANTICILP, demonstrates strong performance on two domains simultaneously. In particular, on a collection of challenging science QA datasets, it outperforms various state-of-the-art approaches, including neural models, broad coverage information retrieval, and specialized techniques using structured knowledge bases, by 2%-6%.

• SciTail: A Textual Entailment Dataset from Science Question Answering

  Tushar Khot, Ashish Sabharwal, and Peter ClarkAAAI 2018

  We present a new dataset and model for textual entailment, derived from treating multiple-choice question-answering as an entailment problem. SCITAIL is the first entailment set that is created solely from natural sentences that already exist independently \"in the wild\" rather than sentences authored specifically for the entailment task. Different from existing entailment datasets, we create hypotheses from science questions and the corresponding answer candidates, and premises from relevant web sentences retrieved from a large corpus. These sentences are often linguistically challenging. This, combined with the high lexical similarity of premise and hypothesis for both entailed and non-entailed pairs, makes this new entailment task particularly difficult. The resulting challenge is evidenced by state-of-the-art textual entailment systems achieving mediocre performance on SCITAIL, especially in comparison to a simple majority class baseline. As a step forward, we demonstrate that one can improve accuracy on SCITAIL by 5% using a new neural model that exploits linguistic structure.

• Approximate Inference via Weighted Rademacher Complexity

  Jonathan Kuck, Ashish Sabharwal, and Stefano ErmonAAAI 2018

  Rademacher complexity is often used to characterize the learnability of a hypothesis class and is known to be related to the class size. We leverage this observation and introduce a new technique for estimating the size of an arbitrary weighted set, defined as the sum of weights of all elements in the set. Our technique provides upper and lower bounds on a novel generalization of Rademacher complexity to the weighted setting in terms of the weighted set size. This generalizes Massart's Lemma, a known upper bound on the Rademacher complexity in terms of the unweighted set size.We show that the weighted Rademacher complexity can be estimated by solving a randomly perturbed optimization problem, allowing us to derive high-probability bounds on the size of any weighted set. We apply our method to the problems of calculating the partition function of an Ising model and computing propositional model counts (#SAT). Our experiments demonstrate that we can produce tighter bounds than competing methods in both the weighted and unweighted settings.

• Knowledge Completion for Generics using Guided Tensor Factorization

  Hanie Sedghi and Ashish SabharwalTACL 2018

2017

• How Good Are My Predictions? Efficiently Approximating Precision-Recall Curves for Massive Datasets

  Ashish Sabharwal and Hanie SedghiUAI 2017

  Large scale machine learning produces massive datasets whose items are often associated with a confidence level and can thus be ranked. However, computing the precision of these resources requires human annotation, which is often prohibitively expensive and is therefore skipped. We consider the problem of cost-effectively approximating precision-recall (PR) or ROC curves for such systems. Our novel approach, called PAULA, provides theoretically guaranteed lower and upper bounds on the underlying precision function while relying on only O(logN) annotations for a resource with N items.

• Learning What is Essential in Questions

  Daniel Khashabi, Tushar Khot, Ashish Sabharwal, and Dan RothCoNLL 2017

  Question answering (QA) systems are easily distracted by irrelevant or redundant words in questions, especially when faced with long or multi-sentence questions in difficult domains. This paper introduces and studies the notion of essential question terms with the goal of improving such QA solvers. We illustrate the importance of essential question terms by showing that humans' ability to answer questions drops significantly when essential terms are eliminated from questions. We then develop a classifier that reliably (90% mean average precision) identifies and ranks essential terms in questions. Finally, we use the classifier to demonstrate that the notion of question term essentiality allows state-of-the-art QA solvers for elementary-level science questions to make better and more informed decisions, improving performance by up to 5%. We also introduce a new dataset of over 2,200 crowd-sourced essential terms annotated science questions.

• Answering Complex Questions Using Open Information Extraction

  Tushar Khot, Ashish Sabharwal, and Peter ClarkACL 2017

  While there has been substantial progress in factoid question-answering (QA), answering complex questions remains challenging, typically requiring both a large body of knowledge and inference techniques. Open Information Extraction (Open IE) provides a way to generate semi-structured knowledge for QA, but to date such knowledge has only been used to answer simple questions with retrieval-based methods. We overcome this limitation by presenting a method for reasoning with Open IE knowledge, allowing more complex questions to be handled. Using a recently proposed support graph optimization framework for QA, we develop a new inference model for Open IE, in particular one that can work effectively with multiple short facts, noise, and the relational structure of tuples. Our model significantly outperforms a state-of-the-art structured solver on complex questions of varying difficulty, while also removing the reliance on manually curated knowledge.

2016

• Question Answering via Integer Programming over Semi-Structured Knowledge

  Daniel Khashabi, Tushar Khot, Ashish Sabharwal, Peter Clark, Oren Etzioni, and Dan RothIJCAI 2016

  Answering science questions posed in natural language is an important AI challenge. Answering such questions often requires non-trivial inference and knowledge that goes beyond factoid retrieval. Yet, most systems for this task are based on relatively shallow Information Retrieval (IR) and statistical correlation techniques operating on large unstructured corpora. We propose a structured inference system for this task, formulated as an Integer Linear Program (ILP), that answers natural language questions using a semi-structured knowledge base derived from text, including questions requiring multi-step inference and a combination of multiple facts. On a dataset of real, unseen science questions, our system significantly outperforms (+14%) the best previous attempt at structured reasoning for this task, which used Markov Logic Networks (MLNs). It also improves upon a previous ILP formulation by 17.7%. When combined with unstructured inference methods, the ILP system significantly boosts overall performance (+10%). Finally, we show our approach is substantially more robust to a simple answer perturbation compared to statistical correlation methods.

• Combining Retrieval, Statistics, and Inference to Answer Elementary Science Questions

  Peter Clark, Oren Etzioni, Daniel Khashabi, Tushar Khot, Ashish Sabharwal, Oyvind Tafjord, Peter TurneyAAAI 2016

  What capabilities are required for an AI system to pass standard 4th Grade Science Tests? Previous work has examined the use of Markov Logic Networks (MLNs) to represent the requisite background knowledge and interpret test questions, but did not improve upon an information retrieval (IR) baseline. In this paper, we describe an alternative approach that operates at three levels of representation and reasoning: information retrieval, corpus statistics, and simple inference over a semi-automatically constructed knowledge base, to achieve substantially improved results. We evaluate the methods on six years of unseen, unedited exam questions from the NY Regents Science Exam (using only non-diagram, multiple choice questions), and show that our overall system’s score is 71.3%, an improvement of 23.8% (absolute) over the MLN-based method describedin previous work. We conclude with a detailed analysis, illustrating the complementary strengths of each method in the ensemble. Our datasets are being released to enable further research.

• Selecting Near-Optimal Learners via Incremental Data Allocation

  Ashish Sabharwal, Horst Samulowitz, Gerald TesauroAAAI 2016

  We study a novel machine learning (ML) problem setting of sequentially allocating small subsets of training data amongst a large set of classifiers. The goal is to select a classifier that will give near-optimal accuracy when trained on all data, while also minimizing the cost of misallocated samples. This is motivated by large modern datasets and ML toolkits with many combinations of learning algorithms and hyperparameters. Inspired by the principle of "optimism under uncertainty," we propose an innovative strategy, Data Allocation using Upper Bounds (DAUB), which robustly achieves these objectives across a variety of real-world datasets. We further develop substantial theoretical support for DAUB in an idealized setting where the expected accuracy of a classifier trained on n samples can be known exactly. Under these conditions we establish a rigorous sub-linear bound on the regret of the approach (in terms of misallocated data), as well as a rigorous bound on suboptimality of the selected classi- fier. Our accuracy estimates using real-world datasets only entail mild violations of the theoretical scenario, suggesting that the practical behavior of DAUB is likely to approach the idealized behavior.

• Closing the Gap Between Short and Long XORs for Model Counting

  Shengjia Zhao, Tum Chaturapruek, Ashish Sabharwal, Stefano ErmonShengjia Zhao, Tum Chaturapruek, Ashish Sabharwal, Stefano ErmonAAAI 2016

  Many recent algorithms for approximate model counting are based on a reduction to combinatorial searches over random subsets of the space defined by parity or XOR constraints. Long parity constraints (involving many variables) provide strong theoretical guarantees but are computationally diffi- cult. Short parity constraints are easier to solve but have weaker statistical properties. It is currently not known how long these parity constraints need to be. We close the gap by providing matching necessary and sufficient conditions on the required asymptotic length of the parity constraints. Further, we provide a new family of lower bounds and the first non-trivial upper bounds on the model count that are valid for arbitrarily short XORs. We empirically demonstrate the effectiveness of these bounds on model counting benchmarks and in a Satisfiability Modulo Theory (SMT) application motivated by the analysis of contingency tables in statistics.

• Exact Sampling with Integer Linear Programs and Random Perturbations

  Carolyn Kim, Ashish Sabharwal, Stefano ErmonAAAI 2016

  We consider the problem of sampling from a discrete probability distribution specified by a graphical model. Exact samples can, in principle, be obtained by computing the mode of the original model perturbed with an exponentially many i.i.d. random variables. We propose a novel algorithm that views this as a combinatorial optimization problem and searches for the extreme state using a standard integer linear programming (ILP) solver, appropriately extended to account for the random perturbation. Our technique, GumbelMIP, leverages linear programming (LP) relaxations to evaluate the quality of samples and prune large portions of the search space, and can thus scale to large tree-width models beyond the reach of current exact inference methods. Further, when the optimization problem is not solved to optimality, our method yields a novel approximate sampling technique. We empirically demonstrate that our approach parallelizes well, our exact sampler scales better than alternative approaches, and our approximate sampler yields better quality samples than a Gibbs sampler and a low-dimensional perturbation method.

• Adaptive Concentration Inequalities for Sequential Decision Problems

  Shengjia Zhao, Enze Zhou, Ashish Sabharwal, and Stefano ErmonNIPS 2016

  A key challenge in sequential decision problems is to determine how many samples are needed for an agent to make reliable decisions with good probabilistic guarantees. We introduce Hoeffding-like concentration inequalities that hold for a random, adaptively chosen number of samples. Our inequalities are tight under natural assumptions and can greatly simplify the analysis of common sequential decision problems. In particular, we apply them to sequential hypothesis testing, best arm identification, and sorting. The resulting algorithms rival or exceed the state of the art both theoretically and empirically.

• Beyond Parity Constraints: Fourier Analysis of Hash Functions for Inference

  Tudor Achim, Ashish Sabharwal, and Stefano ErmonICML 2016

  Random projections have played an important role in scaling up machine learning and data mining algorithms. Recently they have also been applied to probabilistic inference to estimate properties of high-dimensional distributions; however , they all rely on the same class of projections based on universal hashing. We provide a general framework to analyze random projections which relates their statistical properties to their Fourier spectrum, which is a well-studied area of theoretical computer science. Using this framework we introduce two new classes of hash functions for probabilistic inference and model counting that show promising performance on synthetic and real-world benchmarks.

2015

• Parsing Algebraic Word Problems into Equations

  Rik Koncel-Kedziorski, Hannaneh Hajishirzi, Ashish Sabharwal, Oren Etzioni, Siena Dumas AngTACL 2015

  This paper formalizes the problem of solving multi-sentence algebraic word problems as that of generating and scoring equation trees. We use integer linear programming to generate equation trees and score their likelihood by learning local and global discriminative models. These models are trained on a small set of word problems and their answers, without any manual annotation, in order to choose the equation that best matches the problem text. We refer to the overall system as ALGES. We compare ALGES with previous work and show that it covers the full gamut of arithmetic operations whereas Hosseini et al. (2014) only handle addition and subtraction. In addition, ALGES overcomes the brittleness of the Kushman et al. (2014) approach on single-equation problems, yielding a 15% to 50% reduction in error.

• Exploring Markov Logic Networks for Question Answering

  Tushar Khot, Niranjan Balasubramanian, Eric Gribkoff, Ashish Sabharwal, Peter Clark, Oren EtzioniEMNLP 2015

  Elementary-level science exams pose significant knowledge acquisition and reasoning challenges for automatic question answering. We develop a system that reasons with knowledge derived from textbooks, represented in a subset of firstorder logic. Automatic extraction, while scalable, often results in knowledge that is incomplete and noisy, motivating use of reasoning mechanisms that handle uncertainty. Markov Logic Networks (MLNs) seem a natural model for expressing such knowledge, but the exact way of leveraging MLNs is by no means obvious. We investigate three ways of applying MLNs to our task. First, we simply use the extracted science rules directly as MLN clauses and exploit the structure present in hard constraints to improve tractability. Second, we interpret science rules as describing prototypical entities, resulting in a drastically simplified but brittle network. Our third approach, called Praline, uses MLNs to align lexical elements as well as define and control how inference should be performed in this task. Praline demonstrates a 15% accuracy boost and a 10x reduction in runtime as compared to other MLNbased methods, and comparable accuracy to word-based baseline approaches.

• BDD-Guided Clause Generation

  Brian Kell, Ashish Sabharwal, Willem-Jan van HoeveCPAIOR 2015

  Nogood learning is a critical component of Boolean satisfiability (SAT) solvers, and increasingly popular in the context of integer programming and constraint programming. We present a generic method to learn valid clauses from exact or approximate binary decision diagrams (BDDs) and resolution in the context of SAT solving. We show that any clause learned from SAT conflict analysis can also be generated using our method, while, in addition, we can generate stronger clauses that cannot be derived from one application of conflict analysis. Importantly, since SAT instances are often too large for an exact BDD representation, we focus on BDD relaxations of polynomial size and show how they can still be used to generated useful clauses. Our experimental results show that when this method is used as a preprocessing step and the generated clauses are appended to the original instance, the size of the search tree for a SAT solver can be significantly reduced.

2014

• Insights Into Parallelism with Intensive Knowledge Sharing

  Ashish Sabharwal, Horst Samulowitz International Conference on Principles and Practice of Constraint Programming 2014

  Novel search space splitting techniques have recently been successfully exploited to paralleliz Constraint Programming and Mixed Integer Programming solvers. We first show how universal hashing can be used to extend one such interesting approach to a generalized setting that goes beyond discrepancy-based search, while still retaining strong theoretical guarantees. We then explain that such static or explicit splitting approaches are not as effective in the context of parallel combinatorial search with intensive knowledge acquisition and sharing such as parallel SAT, where implicit splitting through clause sharing appears to dominate. Furthermore, we show that in a parallel setting there exists a surprising tradeoff between the well-known communication cost for knowledge sharing across multiple compute nodes and the so far neglected cost incurred by the computational load per node. We provide experimental evidence that one can successfully exploit this tradeoff and achieve reasonable speedups in parallel SAT solving beyond 16 cores.

• Non-Restarting SAT Solvers With Simple Preprocessing Can Efficiently Simulate Resolution

  Paul Beame, Ashish SabharwalAAAI 2014Poster | PowerPoint

  Propositional satisfiability (SAT) solvers based on conflict directed clause learning (CDCL) implicitly produce resolution refutations of unsatisfiable formulas. The precise class of formulas for which they can produce polynomial size refutations has been the subject of several studies, with special focus on the clause learning aspect of these solvers. The results, however, assume the use of non-standard and non-asserting learning schemes, or rely on polynomially many restarts for simulating individual steps of a resolution refutation, or work with a theoretical model that significantly deviates from certain key aspects of all modern CDCL solvers such as learning only one asserting clause from each conflict and other techniques such as conflict guided backjumping and phase saving. We study non-restarting CDCL solvers that learn only one asserting clause per conflict and show that, with simple preprocessing that depends only on the number of variables of the input formula, such solvers can polynomially simulate resolution. We show, moreover, that this preprocessing allows one to convert any CDCL solver to one that is non-restarting.

• Designing Fast Absorbing Markov Chains

  Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, Bart SelmanAAAI 2014

  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.

• Low-density Parity Constraints for Hashing-Based Discrete Integration

  Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, Bart SelmanICML 2014

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

• Parallel Combinatorial Optimization with Decision Diagrams

  David Bergman, Andre Cire, Ashish Sabharwal, Horst Samulowitz, Vijay Saraswat, Willem-Jan van HoeveCPAIOR 2014

  We propose a new approach for parallelizing search for combinatorial optimization that is based on a recursive application of approximate Decision Diagrams. This generic scheme can, in principle, be applied to any combinatorial optimization problem for which a decision diagram representation is available. We consider the maximum independent set problem as a specific case study, and show how a recently proposed sequential branch-and-bound scheme based on approximate decision diagrams can be parallelized efficiently using the X10 parallel programming and execution framework. Experimental results using our parallel solver, DDX10, running on up to 256 compute cores spread across a cluster of machines indicate that parallel decision diagrams scale effectively and consistently. Moreover, on graphs of relatively high density, parallel decision diagrams often outperform state-of-the-art parallel integer programming when both use a single 32-core machine.

2013

• Embed and Project: Discrete Sampling with Universal Hashing

  Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, Bart SelmanNIPS 2013

  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.

• Optimization With Parity Constraints: From Binary Codes to Discrete Integration

  Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, Bart SelmanUAI 2013Runner-up for Best Paper Award | Facebook Best Student Paper Award

  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.

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

  Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, Bart SelmanICML 2013

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

• Algorithm Portfolios Based on Cost-Sensitive Hierarchical Clustering

  Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, Meinolf SellmannIJCAI 2013Basis of SAT Competition 2013 Winner in Open and Random tracks

  Different solution approaches for combinatorial problems often exhibit incomparable performance that depends on the concrete problem instance to be solved. Algorithm portfolios aim to combine the strengths of multiple algorithmic approaches by training a classifier that selects or schedules solvers dependent on the given instance. We devise a new classifier that selects solvers based on a cost-sensitive hierarchical clustering model. Experimental results on SAT and MaxSAT show that the new method outperforms the most effective portfolio builders to date.

• Resolution and Parallelizability: Barriers to the Efficient Parallelization of SAT Solvers

  George Katsirelos, Ashish Sabharwal, Horst Samulowitz, Laurent SimonAAAI 2013PowerPoint

  Recent attempts to create versions of Satisfiability (SAT) solvers that exploit parallel hardware and information sharing have met with limited success. In fact, the most successful parallel solvers in recent competitions were based on portfolio approaches with little to no exchange of information between processors. This experience contradicts the apparent parallelizability of exploring a combinatorial search space. We present evidence that this discrepancy can be explained by studying SAT solvers through a proof complexity lens, as resolution refutation engines. Starting with the observation that a recently studied measure of resolution proofs, namely depth, provides a (weak) upper bound to the best possible speedup achievable by such solvers, we empirically show the existence of bottlenecks to parallelizability that resolution proofs typically generated by SAT solvers exhibit. Further, we propose a new measure of parallelizability based on the best-case makespan of an offline resource constrained scheduling problem. This measure explicitly accounts for a bounded number of parallel processors and appears to empirically correlate with parallel speedups observed in practice. Our findings suggest that efficient parallelization of SAT solvers is not simply a matter of designing the right clause sharing heuristics; even in the best case, it can be -- and indeed is -- hindered by the structure of the resolution proofs current SAT solvers typically produce.

• Large Landscape Conservation - Synthetic and Real-World Datasets

  Bistra N. Dilkina, Katherine J. Lai, Ronan LeBras, Yexiang Xue, Carla P. Gomes, Ashish Sabharwal, Jordan Suter, Kevin S. McKelvey, Michael K. Schwartz, Claire A. MontgomeryAAAI 2013

  Biodiversity underpins ecosystem goods and services and hence protecting it is key to achieving sustainability. However, the persistence of many species is threatened by habitat loss and fragmentation due to human land use and climate change. Conservation efforts are implemented under very limited economic resources, and therefore designing scalable, cost-efficient and systematic approaches for conservation planning is an important and challenging computational task. In particular, preserving landscape connectivity between good habitat has become a key conservation priority in recent years. We give an overview of landscape connectivity conservation and some of the underlying graph-theoretic optimization problems. We present a synthetic generator capable of creating families of randomized structured problems, capturing the essential features of real-world instances but allowing for a thorough typical-case performance evaluation of different solution methods. We also present two large-scale real-world datasets, including economic data on land cost, and species data for grizzly bears, wolverines and lynx.

• Snappy: A Simple Algorithm Portfolio

  Horst Samulowitz, Chandra Reddy, Ashish Sabharwal, Meinolf SellmannSAT 2013

  Algorithm portfolios try to combine the strength of individual algorithms to tackle a problem instance at hand with the most suitable technique. In the context of SAT the effectiveness of such approaches is often demonstrated at the SAT Competitions. In this paper we show that a competitive algorithm portfolio can be designed in an extremely simple fashion. In fact, the algorithm portfolio we present does not require any offline learning nor knowledge of any complex Machine Learning tools. We hope that the utter simplicity of our approach combined with its effectiveness will make algorithm portfolios accessible by a broader range of researchers including SAT and CSP solver developers.

• Stronger Inference Through Implied Literals from Conflicts and Knapsack Covers

  Tobias Achterberg, Ashish Sabharwal, Horst SamulowitzCPAIOR 2013

  Implied literals detection has been shown to improve performance of Boolean satisfiability (SAT) solvers for certain problem classes, in particular when applied in an efficient dynamic manner on learned clauses derived from conflicts during backtracking search. We explore this technique further and extend it to mixed integer linear programs (MIPs) in the context of conflict constraints. This results in stronger inference from clique tables and implication tables already commonly maintained by MIP solvers. Further, we extend the technique to knapsack covers and propose an efficient implementation. Our experiments show that implied literals, in particular through stronger inference from knapsack covers, improve the performance of the MIP engine of IBM ILOG CPLEX Optimization Studio 12.5, especially on harder instances.

• Boosting Sequential Solver Portfolios: Knowledge Sharing and Accuracy Prediction

  Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, Meinolf SellmannLION 7 (2013)Basis of SAT Challenge 2012 Best Interacting Multi-Engine Approach in Application track

  Sequential algorithm portfolios for satisfiability testing (SAT), such as SATzilla and 3S, have enjoyed much success in the last decade. By leveraging the differing strengths of individual SAT solvers, portfolios employing older solvers have often fared as well or better than newly designed ones, in several categories of the annual SAT Competitions and Races. We propose two simple yet powerful techniques to further boost the performance of sequential portfolios, namely, a generic way of knowledge sharing suitable for sequential SAT solver schedules which is commonly employed in parallel SAT solvers, and a meta-level guardian classifier for judging whether to switch the main solver suggested by the portfolio with a recourse action solver. With these additions, we show that the performance of the sequential portfolio solver 3S, which dominated other sequential categories but was ranked 10th in the application category of the 2011 SAT Competition, can be boosted significantly, bringing it just one instance short of matching the performance of the winning application track solver, while still outperforming all other solvers submitted to the crafted and random categories.

2012

• Density Propagation and Improved Bounds on the Partition Function

  Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, Bart SelmanNIPS 2012

  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 maxproduct 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 striclty stronger if a general condition holds. We conclude with empirical evidence of improvement over convex relaxations and mean-field based bounds.

• Parallel SAT Solver Selection and Scheduling

  Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, Meinolf SellmannCP 2012

  Combining differing solution approaches by means of solver portfolios has proven as a highly effective technique for boosting solver performance. We consider the problem of generating parallel SAT solver portfolios. Our approach is based on a recently introduced sequential SAT solver portfolio that excelled at the last SAT competition. We show how the approach can be generalized for the parallel case, and how obstacles like parallel SAT solvers and symmetries induced by identical processors can be overcome. We compare different ways of computing parallel solver portfolios with the best performing parallel SAT approaches to date. Extensive experimental results show that the developed methodology very significantly improves our current parallel SAT solving capabilities.

• SatX10: A Scalable Plug & Play Parallel SAT Framework

  Bard Bloom, David Grove, Benjamin Herta, Ashish Sabharwal, Horst Samulowitz, Vijay SaraswatSAT 2012Code

  We propose a framework for SAT researchers to conveniently try out new ideas in the context of parallel SAT solving without the burden of dealing with all the underlying system issues that arise when implementing a massively parallel algorithm. The framework is based on the parallel execution language X10, and allows the parallel solver to easily run on both a single machine with multiple cores and across multiple machines, sharing information such as learned clauses.

• Learning Back-Clauses in SAT

  Ashish Sabharwal, Horst Samulowitz, Meinolf SellmannSAT 2012

  SAT conflict analysis graphs have been used to learn additional clauses, which we refer to as back-clauses. These clauses may be viewed as enabling the powerful notion of "probing": Back-clauses make inferences that would normally have to be deduced by setting a variable deliberately the other way and observing that unit propagation leads to a conflict. We show that short-cutting this process can in fact improve the performance of modern SAT solvers in theory and in practice. Based on out numerical results, it is suprising that back-clauses, proposed over a decade ago, are not yet part of standard clause-learning SAT solvers.

• Augmenting Clause Learning With Implied Literals

  Arie Matsliah, Ashish Sabharwal, Horst SamulowitzSAT 2012

• Guiding Combinatorial Search With UCT

  Ashish Sabharwal, Horst Samulowitz, Chandra ReddyCPAIOR 2012

  We propose a new approach for search tree exploration in the context of combinatorial optimization, specifically Mixed Integer Programming (MIP), that is based on UCT, an algorithm for the multiarmed bandit problem designed for balancing exploration and exploitation in an online fashion. UCT has recently been highly successful in game tree search. We discuss the differences that arise when UCT is applied to search trees as opposed to bandits or game trees, and provide initial results demonstrating that the performance of even a highly optimized state-of-the-art MIP solver such as CPLEX can be boosted using UCT's guidance on a range of problem instances.

2011

• Accelerated Adaptive Markov Chain for Partition Function Computation

  Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, Bart SelmanNIPS 2011

  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.

• Algorithm Selection and Scheduling

  Serdar Kadioglu, Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, Meinolf SellmannCP 2011Basis of SAT Competition 2011 Winner in Crafted and Random categories (total 7 medals) | PowerPoint

  Algorithm portfolios aim to increase the robustness of our ability to solve problems efficiently. While recently proposed algorithm selection methods come ever closer to identifying the most appropriate solver given an input instance, they are bound to make wrong and, at times, costly decisions. Solver scheduling has been proposed to boost the performance of algorithm selection. Scheduling tries to allocate time slots to the given solvers in a portfolio so as to maximize, say, the number of solved instances within a given time limit. We show how to solve the corresponding optimization problem at a low computational cost using column generation, resulting in fast and high quality solutions. We integrate this approach with a recently introduced algorithm selector, which we also extend using other techniques. We propose various static as well as dynamic scheduling strategies, and demonstrate that in comparison to pure algorithm selection, our novel combination of scheduling and solver selection can significantly boost performance.

• Constraint Reasoning and Kernel Clustering for Pattern Decomposition With Scaling

  Ronan LeBras, Theodoros Damoulas, John M. Gregoire, Ashish Sabharwal, Carla P. Gomes, R. Bruce van DoverCP 2011

  Motivated by an important and challenging task encountered in material discovery, we consider the problem of finding K basis patterns of numbers that jointly compose N observed patterns while enforcing additional spatial and scaling constraints. We propose a Constraint Programming (CP) model which captures the exact problem structure yet fails to scale in the presence of noisy data about the patterns. We alleviate this issue by employing Machine Learning (ML) techniques, namely kernel methods and clustering, to decompose the problem into smaller ones based on a global data-driven view, and then stitch the partial solutions together using a global CP model. Combining the complementary strengths of CP and ML techniques yields a more accurate and scalable method than the few found in the literature for this complex problem.

• A General Nogood-Learning Framework for Pseudo-Boolean Multi-Valued SAT

  Siddhartha Jain, Ashish Sabharwal, Meinolf SellmannAAAI 2011

  We formulate a general framework for pseudo-Boolean multivalued nogood-learning, generalizing conflict analysis performed by modern SAT solvers and its recent extension for disjunctions of multi-valued variables. This framework can handle more general constraints as well as different domain representations, such as interval domains which are commonly used for bounds consistency in constraint programming (CP), and even set variables. Our empirical evaluation shows that our solver, built upon this framework, works robustly across a number of challenging domains.

• Non-Model-Based Algorithm Portfolios for SAT

  Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, Meinolf SellmannSAT 2011

2010

• An Empirical Study of Optimization for Maximizing Diffusion in Networks

  Kiyan Ahmadizadeh, Bistra Dilkina, Carla P. Gomes, Ashish SabharwalCP 2010

  We study the problem of maximizing the amount of stochastic diffusion in a network by acquiring nodes within a certain limited budget. We use a Sample Average Approximation (SAA) scheme to translate this stochastic problem into a simulation-based deterministic optimization problem, and present a detailed empirical study of three variants of the problem: where all purchases are made upfront, where the budget is split but one still commits to purchases from the outset, and where one has the ability to observe the stochastic outcome of the first stage in order to "re-plan" for the second stage. We apply this to a Red Cockaded Woodpecker conservation problem. Our results show interesting runtime distributions and objective value patterns, as well as a delicate trade-off between spending all budget upfront vs. saving part of it for later.

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

  Lukas Kroc, Ashish Sabharwal, Bart SelmanSAT 2010

  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.

• Understanding Sampling Style Adversarial Search Methods

  Raghuram Ramanujan, Ashish Sabharwal, Bart SelmanUAI 2010

  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.

• Maximizing Spread of Cascades Using Network Design

  Daniel Sheldon, Bistra Dilkina, Adam Elmachtoub, Ryan Finseth, Ashish Sabharwal, Jon Conrad,Carla Gomes, David Shmoys, Will Allen, Ole Amundsen, William VaughanUAI 2010

  We introduce a new optimization framework to maximize the expected spread of cascades in networks. Our model allows a rich set of actions that directly manipulate cascade dynamics by adding nodes or edges to the network. Our motivating application is one in spatial conservation planning, where a cascade models the dispersal of wild animals through a fragmented landscape. We propose a mixed integer programming (MIP) formulation that combines elements from network design and stochastic optimization. Our approach results in solutions with stochastic optimality guarantees and points to conservation strategies that are fundamentally different from naive approaches.

• On Adversarial Search Spaces and Sampling-Based Planning

  Raghuram Ramanujan, Ashish Sabharwal, Bart SelmanICAPS 2010

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

2009

• Integrating Systematic and Local Search Paradigms: A New Strategy for MaxSAT

  Lukas Kroc, Ashish Sabharwal, Carla P. Gomes, Bart SelmanIJCAI 2009

  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 unsatisfi- ability is already hard; otherwise the method falls back to pure local search.

• Relaxed DPLL Search for MaxSAT

  Lukas Kroc, Ashish Sabharwal, Bart SelmanSAT 2009Slides

  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.

• Backdoors in the Context of Learning

  Bistra Dilkina, Carla P. Gomes, Ashish SabharwalSAT 2009Slides | Extended Version

  The concept of backdoor variables has been introduced as a structural property of combinatorial problems that provides insight into the surprising ability of modern satisfiability (SAT) solvers to tackle extremely large instances. This concept is, however, oblivious to "learning" during search—a key feature of successful combinatorial reasoning engines for SAT, mixed integer programming (MIP), etc. We extend the notion of backdoors to the context of learning during search. We prove that the smallest backdoors for SAT that take into account clause learning and order-sensitivity of branching can be exponentially smaller than “traditional” backdoors. We also study the effect of learning empirically.

• Backdoors in the Context of Learning

  Bistra Dilkina, Carla P. Gomes, Yuri Malitski, Ashish Sabharwal, Meinolf SellmannCPAIOR 2009(Draft PDF)

  There has been considerable interest in the identification of structural properties of combinatorial problems that lead, directly or indirectly, to the development of efficient algorithms for solving them. One such concept is that of a backdoor set--a set of variables such that once they are instantiated, the remaining problem simplifies to a tractable form. While backdoor sets were originally defined to capture structure in decision problems with discrete variables, here we introduce a notion of backdoors that captures structure in optimization problems, which often have both discrete and continuous variables. We show that finding a feasible solution and proving optimality are characterized by backdoors of different kinds and size. Surprisingly, in certain mixed integer programming problems, proving optimality involves a smaller backdoor set than finding the optimal solution. We also show extensive results on the number of backdoors of various sizes in optimization problems. Overall, this work demonstrates that backdoors, appropriately generalized, are also effective in capturing problem structure in optimization problems.

• Message-Passing and Local Heuristics as Decimation Strategies for Satisfiability

  Lukas Kroc, Ashish Sabharwal, Bart SelmanSAC 2009Slides | Bibliography

  Decimation is a simple process for solving constraint satisfaction problems, by repeatedly fixing variable values and simplifying without reconsidering earlier decisions. We investigate different decimation strategies, contrasting those based on local, syntactic information from those based on message passing, such as statistical physics based Survey Propagation (SP) and the related and more well-known Belief Propagation (BP). Our results reveal that once we resolve convergence issues, BP itself can solve fairly hard random k-SAT formulas through decimation; the gap between BP and SP narrows down quickly as k increases. We also investigate observable differences between BP/SP and other common CSP heuristics as decimation proceeds, exploring the hardness of the decimated formulas and identifying a somewhat unexpected feature of message passing heuristics, namely, unlike other heuristics for satisfiability, they avoid unit propagation as variables are fixed.

2008

• Counting Solution Clusters in Graph Coloring Problems Using Belief Propagation

  Lukas Kroc, Ashish Sabharwal, Bart SelmanNIPS 2008Slides | Bibliography

  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 clusters exactly using advanced techniques from the knowledge compilation literature. This methodology scales up to several hundred variables.

• Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting

  Lukas Kroc, Ashish Sabharwal, Bart SelmanCPAIOR 2008Slides | Bibliography

  We consider the problem of estimating the model count (number of solutions) of Boolean formulas, and present two techniques that compute estimates of these counts, as well as either lower or upper bounds with different trade-offs between efficiency, bound quality, and correctness guarantee. For lower bounds, we use a recent framework for probabilistic correctness guarantees, and exploit message passing techniques for marginal probability estimation, namely, variations of Belief Propagation (BP). Our results suggest that BP provides useful information even on structured loopy formulas. For upper bounds, we perform multiple runs of the MiniSat SAT solver with a minor modification, and obtain statistical bounds on the model count based on the observation that the distribution of a certain quantity of interest is often very close to the normal distribution. Our experiments demonstrate that our model counters based on these two ideas, BPCount and MiniCount, can provide very good bounds in time significantly less than alternative approaches.

• Connections in Networks: A Hybrid Approach

  Carla P. Gomes, Willem-Jan van Hoeve, Ashish SabharwalCPAIOR 2008Slides | Bibliography

  This paper extends our previous work by exploring the use of a hybrid solution method for solving the connection subgraph problem. We employ a two phase solution method, which drastically reduces the cost of testing for infeasibility and also helps prune the search space for MIP-based optimization. Overall, this provides a much more scalable solution than simply optimizing a MIP model of the problem with Cplex. We report results for semi-structured lattice instances as well as on real data used for the construction of a wildlife corridor for grizzly bears in the Northern Rockies region.

• Filtering Atmost1 on Pairs of Set Variables

  Willem-Jan van Hoeve, Ashish SabharwalCPAIOR 2008Bibliography

2007

• Tradeoffs in the Complexity of Backdoor Detection

  Bistra Dilkina, Carla P. Gomes, Ashish SabharwalCP 2007Bibliography | Extended Results

  There has been considerable interest in the identification of structural properties of combinatorial problems that lead to efficient algorithms for solving them. Some of these properties are "easily" identifiable, while others are of interest because they capture key aspects of state-of-the-art constraint solvers. In particular, it was recently shown that the problem of identifying a strong Horn- or 2CNF-backdoor can be solved by exploiting equivalence with deletion backdoors, and is NPcomplete. We prove that strong backdoor identification becomes harder than NP (unless NP=coNP) as soon as the inconsequential sounding feature of empty clause detection (present in all modern SAT solvers) is added. More interestingly, in practice such a feature as well as polynomial time constraint propagation mechanisms often lead to much smaller backdoor sets. In fact, despite the worst-case complexity results for strong backdoor detection, we show that Satz-Rand is remarkably good at finding small strong backdoors on a range of experimental domains. Our results suggest that structural notions explored for designing efficient algorithms for combinatorial problems should capture both statically and dynamically identifiable properties.

• Survey Propagation Revisited

  Lukas Kroc, Ashish Sabharwal, Bart SelmanUAI 2007Nominated for the UAI-07 Best Student Paper Award | Bibliography

  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.

• The Impact of Network Topology on Pure Nash Equilibria in Graphical Games

  Bistra Dilkina, Carla P. Gomes, Ashish SabharwalAAAI 2007Nominated for the AAAI-07 Best Paper Award | Bibliography

  Graphical games capture some of the key aspects relevant to the study and design of multi-agent systems. It is often of interest to find the conditions under which a game is stable, i.e., the players have reached a consensus on their actions. In this paper, we characterize how different topologies of the interaction network affect the probability of existence of a pure Nash equilibrium in a graphical game with random payoffs. We show that for tree topologies with unbounded diameter the probability of a pure Nash equilibrium vanishes as the number of players grows large. On the positive side, we define several families of graphs for which the probability of a pure Nash equilibrium is at least 1 − 1/e even as the number of players goes to infinity. We also empirically show that adding a small number of connection "shortcuts" can increase the probability of pure Nash.

• Counting CSP Solutions Using Generalized XOR Constraints

  Carla P. Gomes, Willem-Jan van Hoeve, Ashish Sabharwal, Bart SelmanAAAI 2007Slides | Bibliography

  We present a general framework for determining the number of solutions of constraint satisfaction problems (CSPs) with a high precision. Our first strategy uses additional binary variables for the CSP, and applies an XOR or parity constraint based method introduced previously for Boolean satisfiability (SAT) problems. In the CSP framework, in addition to the naive individual filtering of XOR constraints used in SAT, we are able to apply a global domain filtering algorithm by viewing these constraints as a collection of linear equalities over the field of two elements. Our most promising strategy extends this approach further to larger domains, and applies the so-called generalized XOR constraints directly to CSP variables. This allows us to reap the benefits of the compact and structured representation that CSPs offer. We demonstrate the effectiveness of our counting framework through experimental comparisons with the solution enumeration approach (which, we believe, is the current best generic solution counting method for CSPs), and with solution counting in the context of SAT and integer programming.

• Short XORs for Model Counting: From Theory to Practice

  Carla P. Gomes, Joerg Hoffmann, Ashish Sabharwal, Bart SelmanSAT 2007Slides | Bibliography

  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.

• Connections in Networks: Hardness of Feasibility versus Optimality

  Jon Conrad, Carla P. Gomes, Willem-Jan van Hoeve, Ashish Sabharwal, Jordan SuterCPAIOR 2007Slides | Bibliography

  We study the complexity of combinatorial problems that consist of competing infeasibility and optimization components. In particular, we investigate the complexity of the connection subgraph problem, which occurs, e.g., in resource environment economics and social networks. We present results on its worst-case hardness and approximability. We then provide a typical-case analysis by means of a detailed computational study. First, we identify an easy-hard-easy pattern, coinciding with the feasibility phase transition of the problem. Second, our experimental results reveal an interesting interplay between feasibility and optimization. They surprisingly show that proving optimality of the solution of the feasible instances can be substantially easier than proving infeasibility of the infeasible instances in a computationally hard region of the problem space. We also observe an intriguing easy-hard-easy pro- file for the optimization component itself.

• From Sampling to Model Counting

  Carla P. Gomes, Joerg Hoffmann, Ashish Sabharwal, Bart SelmanIJCAI 2007Nominated for the IJCAI-07 Best Paper Award | Bibliography

  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.

2006

• Near-Uniform Sampling of Combinatorial Spaces Using XOR Constraints

  Carla P. Gomes, Ashish Sabharwal, Bart SelmanNIPS 2006Bibliography

  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 (XOR) 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.

• Revisiting the Sequence Constraint

  Willem-Jan van Hoeve, Gilles Pesant, Louis-Martin Rousseau, Ashish SabharwalCP 2006Best Paper Award | Bibliography

  Many combinatorial problems, such as car sequencing and rostering, feature sequence constraints, restricting the number of occurrences of certain values in every subsequence of a given width. To date, none of the filtering algorithms proposed guaranteed domain consistency. In this paper, we present three filtering algorithms for the sequence constraint, with complementary strengths. One borrows ideas from dynamic programming; another reformulates it as a regular constraint; the last is customized. The last two algorithms establish domain consistency. Our customized algorithm does so in polynomial time, and can even be applied to a generalized sequence constraint for subsequences of variable widths. Experimental results show the practical usefulness of each.

• QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency

  Ashish Sabharwal, Carlos Ansotegui, Carla P. Gomes, Justin W. Hart, Bart SelmanSAT 2006Slides | Video from slides | Bibliography

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

• Model Counting: A New Strategy for Obtaining Good Bounds

  Carla P. Gomes, Ashish Sabharwal, Bart SelmanAAAI 2006Slides | Bibliography

  Model counting is the classical problem of computing the number of solutions of a given propositional formula. It vastly generalizes the NP-complete problem of propositional satisfiability, and hence is both highly useful and extremely expensive to solve in practice. We present a new approach to model counting that is based on adding a carefully chosen number of so-called streamlining constraints to the input formula in order to cut down the size of its solution space in a controlled manner. Each of the additional constraints is a randomly chosen XOR or parity constraint on the problem variables, represented either directly or in the standard CNF form. Inspired by a related yet quite different theoretical study of the properties of XOR constraints, we provide a formal proof that with high probability, the number of XOR constraints added in order to bring the formula to the boundary of being unsatisfiable determines with high precision its model count. Experimentally, we demonstrate that this approach can be used to obtain good bounds on the model counts for formulas that are far beyond the reach of exact counting methods. In fact, we obtain the first non-trivial solution counts for very hard, highly structured combinatorial problem instances. Note that unlike other counting techniques, such as Markov Chain Monte Carlo methods, we are able to provide highconfidence guarantees on the quality of the counts obtained.

• Friends or Foes? An AI Planning Perspective on Abstraction and Search

  Joerg Hoffmann, Ashish Sabharwal, Carmel DomshlakICAPS 2006Nominated for the ICAPS-06 Best Paper Award | Bibliography

  There is increasing awareness that planning and model checking are closely related fields. Abstraction means to perform search in an over-approximation of the original problem instance, with a potentially much smaller state space. This is the most essential method in model checking. One would expect that it can also be made successful in planning. We show, however, that this is likely to not be the case. The main reason is that, while in model checking one traditionally uses blind search to exhaust the state space and prove the absence of solutions, in planning informed search is used to find solutions. We give an exhaustive theoretical and practical account of the use of abstraction in planning. For all abstraction (over-approximation) methods known in planning, we prove that they cannot improve the best-case behavior of informed search. While this is easy to see for heuristic search, we were quite surprised to find that it also holds, in most cases, for the resolution-style proofs of unsolvability underlying SATbased optimal planners. This result is potentially relevant also for model checking, where SAT-based techniques have recently been combined with abstraction. Exploring the issue in planning practice, we find that even hand-made abstractions do not tend to improve the performance of planners, unless the attacked task contains huge amounts of irrelevance. We relate these findings to the kinds of application domains that are typically addressed in model checking.

2005 and earlier

• SymChaff: A Structure-Aware Satisfiability Solver

  Ashish SabharwalAAAI 2005Slides | Bibliography

  We present a novel low-overhead framework for encoding and utilizing structural symmetry in propositional satisfiability algorithms (SAT solvers). We use the notion of complete multi-class symmetry and demonstrate the efficacy of our technique through a solver SymChaff that achieves exponential speedup by using simple tags in the specification of problems from both theory and practice.

• Using Problem Structure for Efficient Clause Learning

  Ashish Sabharwal, Paul Beame, Henry KautzSAT 2003Slides | Bibliography

  DPLL based clause learning algorithms for satisfiability testing are known to work very well in practice. However, like most branch-and-bound techniques, their performance depends heavily on the variable order used in making branching decisions. We propose a novel way of exploiting the underlying problem structure to guide clause learning algorithms toward faster solutions. The key idea is to use a higher level problem description, such as a graph or a PDDL specification, to generate a good branching sequence as an aid to SAT solvers. The sequence captures hierarchical structure that is lost in the CNF translation. We show that this leads to exponential speedups on grid and randomized pebbling problems. The ideas we use originate from the analysis of problem structure recently used in [1] to study clause learning from a theoretical perspective.

• Understanding the Power of Clause Learning

  Paul Beame, Henry Kautz, Ashish SabharwalIJCAI 2003Slides | Bibliography

  Efficient implementations of DPLL with the addition of clause learning are the fastest complete satisfiability solvers and can handle many significant real-world problems, such as verification, planning, and design. Despite its importance, little is known of the ultimate strengths and limitations of the technique. This paper presents the first precise characterization of clause learning as a proof system, and begins the task of understanding its power. In particular, we show that clause learning using any nonredundant scheme and unlimited restarts is equivalent to general resolution. We also show that without restarts but with a new learning scheme, clause learning can provide exponentially smaller proofs than regular resolution, which itself is known to be much stronger than ordinary DPLL.

• Bounded-depth Frege Lower Bounds for Weaker Pigeonhole Principles

  Josh Buresh-Oppenheim, Paul Beame, Toniann Pitassi, Ran Raz, Ashish SabharwalFOCS 2002Bibliography

  We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle PHPm n where m = (1 + 1=polylog n)n. This lower bound qualitatively matches the known quasipolynomial-size bounded-depth Frege proofs for these principles. Our technique, which uses a switching lemma argument like other lower bounds for boundeddepth Frege proofs, is novel in that the tautology to which this switching lemma is applied remains random throughout the argument.

• Resolution Complexity of Independent Sets in Random Graphs

  Paul Beame, Russell Impagliazzo, Ashish SabharwalCCC 2001Bibliography

Journal Articles

• Tradeoffs in the Complexity of Backdoors to Satisfiability: Dynamic Sub-Solvers and Learning During Search

  Bistra Dilkina, Carla Gomes, Ashish SabharwalAMAI 2014

• Wildlife Corridors as a Connected Subgraph Problem

  Jon Conrad, Carla P. Gomes, Willem-Jan van Hoeve, Ashish Sabharwal, Jordan F. SuterJEEM 2012Also as TechReport 2010, Incorporating Economic and Ecological Information into the Optimal Design of Wildlife Corridors

• Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting

  Lukas Kroc, Ashish Sabharwal, Bart SelmanANOR 2011

  We consider the problem of estimating the model count (number of solutions) of Boolean formulas, and present two techniques that compute estimates of these counts, as well as either lower or upper bounds with different trade-offs between efficiency, bound quality, and correctness guarantee. For lower bounds, we use a recent framework for probabilistic correctness guarantees, and exploit message passing techniques for marginal probability estimation, namely, variations of the Belief Propagation (BP) algorithm. Our results suggest that BP provides useful information even on structured, loopy formulas. For upper bounds, we perform multiple runs of the MiniSat SAT solver with a minor modification, and obtain statistical bounds on the model count based on the observation that the distribution of a certain quantity of interest is often very close to the normal distribution. Our experiments demonstrate that our model counters based on these two ideas, BPCount and MiniCount, can provide very good bounds in time significantly less than alternative approaches.

• Predicting direct protein interactions from affinity purification mass spectrometry data

  Ethan Kim, Ashish Sabharwal, Adrian R. Vetta, Mathieu BlanchetteALMOB 2010

  Background: Affinity purification followed by mass spectrometry identification (AP-MS) is an increasingly popular approach to observe protein-protein interactions (PPI) in vivo. One drawback of AP-MS, however, is that it is prone to detecting indirect interactions mixed with direct physical interactions. Therefore, the ability to distinguish direct interactions from indirect ones is of much interest. Results: We first propose a simple probabilistic model for the interactions captured by AP-MS experiments, under which the problem of separating direct interactions from indirect ones is formulated. Then, given idealized quantitative AP-MS data, we study the problem of identifying the most likely set of direct interactions that produced the observed data. We address this challenging graph theoretical problem by first characterizing signatures that can identify weakly connected nodes as well as dense regions of the network. The rest of the direct PPI network is then inferred using a genetic algorithm. Our algorithm shows good performance on both simulated and biological networks with very high sensitivity and specificity. Then the algorithm is used to predict direct interactions from a set of AP-MS PPI data from yeast, and its performance is measured against a high-quality interaction dataset. Conclusions: As the sensitivity of AP-MS pipeline improves, the fraction of indirect interactions detected will also increase, thereby making the ability to distinguish them even more desirable. Despite the simplicity of our model for indirect interactions, our method provides a good performance on the test networks.

• Friends or Foes? On Planning as Satisfiability and Abstract CNF Encodings

  Carmel Domshlak, Joerg Hoffmann, Ashish SabharwalJAIR 2009Bibliography

  Planning as satisfiability, as implemented in, for instance, the SATPLAN tool, is a highly competitive method for finding parallel step-optimal plans. A bottleneck in this approach is to prove the absence of plans of a certain length. Specifically, if the optimal plan has n steps, then it is typically very costly to prove that there is no plan of length n−1. We pursue the idea of leading this proof within solution length preserving abstractions (overapproximations) of the original planning task. This is promising because the abstraction may have a much smaller state space; related methods are highly successful in model checking. In particular, we design a novel abstraction technique based on which one can, in several widely used planning benchmarks, construct abstractions that have exponentially smaller state spaces while preserving the length of an optimal plan.

• Towards Understanding and Harnessing the Potential of Clause Learning

  Paul Beame, Henry Kautz, Ashish SabharwalJAIR 2004Runner-up for the IJCAI-JAIR 2003-2008 Best Paper Prize | See also chapter 4 of my Ph.D. thesis, in particular Corollary 4.2 | Bibliography

  Efficient implementations of DPLL with the addition of clause learning are the fastest complete Boolean satisfiability solvers and can handle many significant real-world problems, such as verification, planning and design. Despite its importance, little is known of the ultimate strengths and limitations of the technique. This paper presents the first precise characterization of clause learning as a proof system (CL), and begins the task of understanding its power by relating it to the well-studied resolution proof system. In particular, we show that with a new learning scheme, CL can provide exponentially shorter proofs than many proper refinements of general resolution (RES) satisfying a natural property. These include regular and Davis-Putnam resolution, which are already known to be much stronger than ordinary DPLL. We also show that a slight variant of CL with unlimited restarts is as powerful as RES itself. Translating these analytical results to practice, however, presents a challenge because of the nondeterministic nature of clause learning algorithms. We propose a novel way of exploiting the underlying problem structure, in the form of a high level problem description such as a graph or PDDL specification, to guide clause learning algorithms toward faster solutions. We show that this leads to exponential speed-ups on grid and randomized pebbling problems, as well as substantial improvements on certain ordering formulas.

• New Filtering Algorithms for Combinations of Among Constraints

  Willem-Jan van Hoeve, Gilles Pesant, Louis-Martin Rousseau, Ashish SabharwalConstraints 2009Bibliography

  Several combinatorial problems, such as car sequencing and rostering, feature sequence constraints, restricting the number of occurrences of certain values in every subsequence of a given length. We present three new filtering algorithms for the sequence constraint, including the first to establish domain consistency in polynomial time. The filtering algorithms have complementary strengths: One borrows ideas from dynamic programming; another reformulates it as a regular constraint; the last is customized. The last two algorithms establish domain consistency, and the customized one does so in polynomial time. We provide experimental results that show the practical usefulness of each. We also show that the customized algorithm equally applies to a generalized version of the sequence constraint for subsequences of varied lengths. The significant computational advantage of using one generalized sequence constraint over a semantically equivalent combination of among or sequence constraints is demonstrated experimentally.

• SymChaff: Exploiting Symmetry in a Structure-Aware Satisfiability Solver

  Ashish SabharwalConstraints 2009Bibliography

  This article presents a new low-overhead framework for representing and utilizing problem symmetry in propositional satisfiability algorithms. While many previous approaches have focused on symmetry extraction as a key component, the novelty in the proposed strategy lies in using high level problem description to pass on symmetry information to the SAT solver in a simple and concise form, in addition to the usual CNF formula. This information, comprising of the so-called symmetry sets and variable classes, captures variable semantics relevant to "complete multi-class symmetry" and is utilized dynamically to prune the search space. This allows us to address many limitations of alternative approaches like symmetry breaking predicates, implicit pseudo-Boolean representations, general group-theoretic methods, and ZBDDs. We demonstrate the efficacy of our technique through a solver called SymChaff, which achieves exponential speedup over DPLL-based SAT solvers on problems from both theory and practice, often by simply using natural tags or annotation in the problem specification.

• The Resolution Complexity of Independent Sets and Vertex Covers in Random Graphs

  Paul Beame, Russell Impagliazzo, Ashish SabharwalComputational Complexity 2007Bibliography

• Bounded-Depth Frege Lower Bounds for Weaker Pigeonhole Principles

  Josh Buresh-Oppenheim, Paul Beame, Toniann Pitassi, Ran Raz, Ashish SabharwalSICOMP 2004Bibliography

• Floodlight Illumination of Infinite Wedges

  Matthew Cary, Atri Rudra, Ashish Sabharwal, Erik VeeCOMGEO 2010

Book Chapter and Surveys

• Book Review: S. Russell, P. Norvig, Artificial Intelligence: A Modern Approach, Third Edition

  Ashish Sabharwal, Bart SelmanAIJ 2011

• Incomplete Algorithms (for Satisfiability)

  Henry Kautz, Ashish Sabharwal, Bart SelmanHandbook of Satisfiability, IOS Press. Editors: Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. Chapter 6, pp 185-203, 2009.Draft

• Model Counting

  Carla P. Gomes, Ashish Sabharwal, Bart SelmanHandbook of Satisfiability, IOS Press. Editors: Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. Chapter 20, pp 633-654, 2009.Draft

• Exploiting Runtime Variation in Complete Solvers (for Satisfiability)

  Carla P. Gomes, Ashish SabharwalHandbook of Satisfiability, IOS Press. Editors: Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. Chapter 9, pp 271-288, 2009.

• Satisfiability Solvers

  Carla P. Gomes, Henry Kautz, Ashish Sabharwal, Bart SelmanHandbook of Knowledge Representation, in the series Foundations of Artificial Intelligence, vol. 3. Editors: Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter. Elsevier, pp 89-134, 2008.

Workshops, Invited Talks, Other Work

• Automatic Construction of Inference-Supporting Knowledge Bases

  Peter Clark, Niranjan Balasubramanian, Sumithra Bhakthavatsalam, Kevin Humphreys, Jesse Kinkead, Ashish Sabharwal, and Oyvind TafjordAKBC-2014 at NIPS. 4th Workshop on Automated Knowledge Base Construction, in conjunction with NIPS-2014, Montreal, QC, Dec 2014Outstanding Paper Award

• General Nogood-Learning Framework for Pseudo-Boolean Multi-Valued SAT

  Siddhartha Jain, Ashish Sabharwal, Meinolf SellmannCSPSAT-2011 at SAT-2011. 1st International Workshop on the Cross-Fertilization Between CSP and SAT, Ann Arbor, MI, June 2011Slides

• Guiding Combinatorial Optimization with UCT

  Ashish Sabharwal, Horst SamulowitzMCTS-2011. ICAPS 2011 Workshop on Monte-Carlo Tree Search: Theory and Applications, Freiburg, Germany, June 2011

• On the Behavior of UCT in Synthetic Search Spaces

  Raghuram Ramanujan, Ashish Sabharwal, Bart SelmanMCTS-2011. ICAPS 2011 Workshop on Monte-Carlo Tree Search: Theory and Applications, Freiburg, Germany, June 2011

• A flat histogram method for inference with probabilistic and deterministic constraints

  Stefano Ermon, Carla Gomes, Ashish Sabharwal, Bart SelmanDISCML-2010. NIPS 2010 Workshop on Discrete Optimization in Machine Learning: Structures, Algorithms and Applications, Whistler, BC, Canada, Dec 2010

• Bridging Constraint Reasoning and Machine Learning for Unsupervised Labeling and Decomposition

  Ronan LeBras, Theodoros Damoulas, John M. Gregoire, Ashish Sabharwal (presenting author), Carla P. Gomes, R. Bruce van DoverINFORMS-2010. INFORMS Annual Meeting, Austin, TX, Nov 2010

• Backdoors in the Context of Combinatorial Optimization and Learning

  Bistra Dilkina, Carla P. Gomes, Yuri Malitsky, Ashish Sabharwal (presenting author), Meinolf SellmannINFORMS-2010. INFORMS Annual Meeting, Austin, TX, Nov 2010

• Game Playing Techniques for Optimization Under Uncertainty

  Kiyan Ahmadizadeh, Carla P. Gomes, Ashish SabharwalCROCS at CP-10. Third International Workshop on Constraint Reasoning and Optimization for Computational Sustainability, St Andrews, Scotland, Sep 2010

• Computational Thinking for Material Discovery: Bridging Constraint Reasoning and Learning

  Ronan LeBras, Theodoros Damoulas, John M. Gregoire, Ashish Sabharwal, Carla P. Gomes, R. Bruce van DoverCROCS at CPAIOR-10. Second International Workshop on Constraint Reasoning and Optimization for Computational Sustainability (in conjunction with CPAIOR-10 conference), Bologna, Italy, June 2010

• Optimal Network Design for the Spread of Cascades

  Daniel Sheldon, Bistra Dilkina, Adam Elmachtoub, Ryan Finseth, Ashish Sabharwal, Jon Conrad,Carla Gomes, David Shmoys, Will Allen, Ole Amundsen, William VaughanCROCS at CPAIOR-10. Second International Workshop on Constraint Reasoning and Optimization for Computational Sustainability (in conjunction with CPAIOR-10 conference), Bologna, Italy, June 2010

• Approximate Inference for Clusters in Solution Spaces

  Lukas Kroc, Ashish Sabharwal, Bart SelmanWARA-2010. AAAI-10 Workshop on Abstraction, Reformulation, and Approximation, Atlanta, GA, Jul 2010

• Connections in Networks: A Hybrid Approach

  Carla P. Gomes, Willem-Jan van Hoeve (presenter), Ashish SabharwalINFORMS-09. INFORMS Annual Meeting, San Diego, CA, Oct 2009

• Optimizing Fish Passage Barrier Removal Using Mixed Integer Linear Programming

  Carla P. Gomes, Ashish SabharwalCROCS-09. First International Workshop on Constraint Reasoning and Optimization for Computational Sustainability (in conjunction with CP-09 Conference), Lisbon, Portugal, Sep 2009Slides

• Integrating Systematic and Local Search Paradigms: A New Strategy for MaxSAT

  Lukas Kroc, Ashish Sabharwal, Carla P. Gomes, Bart SelmanSoCS-09. The 2009 International Symposium on Combinatorial Search, Lake Arrowhead, CA, July 2009

• Backdoors in the Context of Learning

  Bistra Dilkina, Carla P. Gomes, Ashish Sabharwal (presenter)CORS-INFORMS-09. CORS-INFORMS International Meeting, Toronto, ON, Canada, June 2009

• Integrating Systematic and Local Search Paradigms: A New Strategy for MaxSAT

  Lukas Kroc, Ashish Sabharwal (presenter), Carla P. Gomes, Bart SelmanCORS-INFORMS-09. CORS-INFORMS International Meeting, Toronto, ON, Canada, June 2009

• Domain Filtering for the Intersection of Set Variables

  Willem-Jan van Hoeve (presenter), Ashish SabharwalEURO-09. 23rd European Conference on Operational Research, Bonn, Germany, Jul 2009

• Solution Counting Methods for Combinatorial Problems

  Carla P. Gomes, Willem-Jan van Hoeve, Lukas Kroc, Ashish Sabharwal (presenter), Bart SelmanINFORMS-08. INFORMS Annual Meeting, Washington, DC, Oct 2008Slides

• Hidden Structure in Constraint Reasoning Problems

  Bistra Dilkina, Carla P. Gomes, Ashish Sabharwal (presenter)INFORMS-08. INFORMS Annual Meeting, Washington, DC, Oct 2008Slides

• Counting CSP Solutions Using Generalized XOR Constraints

  Carla P. Gomes, Willem-Jan van Hoeve (presenter), Ashish Sabharwal, Bart SelmanINFORMS-08. INFORMS Annual Meeting, Washington, DC, Oct 2008

• Optimal Corridor Design for Grizzly Bear in the U.S. Northern Rockies

  Jordan F. Suter (presenter), Jon Conrad, Carla P. Gomes, Willem-Jan van Hoeve, Ashish SabharwalAAEA-08. American Agricultural Economics Association Annual Meeting, Orlando, FL, Jul 2008

• Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting

  Lukas Kroc (presenter), Ashish Sabharwal, and Bart SelmanISAIM-08. 10th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, FL, Jan 2008Bibliography

• Tradeoffs in Backdoors: Inconsistency Detection, Dynamic Simplification, and Preprocessing

  Bistra Dilkina, Carla Gomes, Ashish Sabharwal (presenter)ISAIM-08. 10th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, FL, Jan 2008Slides | Bibliography

• Hidden Structure in Combinatorial Problems

  Carla P. Gomes, Ashish Sabharwal (presenter)INFORMS-07. INFORMS Annual Meeting, Seattle, WA, Nov 2007

• Filtering Algorithms for the Sequence Constraint

  Willem-Jan van Hoeve (presenter), Gilles Pesant, Louis-Martin Rousseau, Ashish SabharwalINFORMS-07. INFORMS Annual Meeting, Seattle, WA, Nov 2007

• Two Set Constraints for Modeling and Efficiency

  Willem-Jan van Hoeve, Ashish Sabharwal (presenter)ModRef-07 at CP-07. 6th International Workshop on Constraint Modelling and Reformulation, Providence, RI, Sep 2007. In conjunction with the CP-07 conferenceSlides | Bibliography

• Sampling and Soundness: Can We Have Both?

  Carla P. Gomes, Joerg Hoffmann, Ashish Sabharwal, Bart SelmanISWC-07. 6th International Semantic Web Conference, Busan, Korea, Nov 2007

• Empirical Validation of the Relationship Between Survey Propagation and Covers in Random 3-SAT

  Lukas Kroc (presenter), Ashish Sabharwal, Bart SelmanAISP-07. Workshop on Algorithms, Inference, & Statistical Physics, Santa Fe, NM, May 2007Slides

• Sparse Message Passing Algorithms for Weighted Maximum Satisfiability

  Aron Culotta, Andrew McCallum, Bart Selman, Ashish SabharwalNESCAI-07. 2nd North East Student Colloquium on Artificial Intelligence, Ithaca, NY, Apr 2007.

• Streamlining Reasoning for Solution Finding and Counting

  Carla P. Gomes (presenter), Ashish Sabharwal, Meinolf Sellmann, Bart SelmanINFORMS-06. INFORMS Annual Meeting, Pittsburgh, PA, Nov 2006

• Algorithmic Applications of Propositional Proof Complexity

  PH.D. ThesisUniversity of Washington, Seattle, 2005Advisors: Profs. Paul Beame and Henry Kautz | BibliographyChapters (single-spaced):Title page | Abstract | Contents | Ch. 1 | Ch. 2 | Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7

  This thesis explores algorithmic applications of proof complexity theory to the areas of exact and approximation algorithms for graph problems as well as propositional reasoning systems studied commonly by the artificial intelligence and formal verification communities. On the theoretical side, our focus is on the propositional proof system called resolution. On the practical side, we concentrate on propositional satisfiability algorithms (SAT solvers) which form the core of numerous real-world automated reasoning systems. There are three major contributions in this work. (A) We study the behavior of resolution on appropriate encodings of three graphs problems, namely, independent set, vertex cover, and clique. We prove lower bounds on the sizes of resolution proofs for these problems and derive from this unconditional hardness of approximation results for resolution-based algorithms. (B) We explore two key techniques used in SAT solvers called clause learning and restarts, providing the first formal framework for their analysis. Formulating them as proof systems, we put them in perspective with respect to resolution and its refinements. (C) We present new techniques for designing structure-aware SAT solvers based on high-level problem descriptions. We present empirical studies which demonstrate that one can achieve enormous speed-up in practice by incorporating variable orders as well as symmetry information obtained directly from the underlying problem domain.

• Model Checking: Two Decades of Novel Techniques and Trends

  General Examination Report, University of Washington, Seattle, May 2002

Tutorials and Teaching

Tutorials

• Branching Strategies and Restarts in SAT Solvers

  Ashish SabharwalGeneral Principles Workshop at CPAIOR-2013Workshop on General Principles in Seeking Feasible Solutions for Combinatorial Problems, at CPAIOR-2013 Conference, Yorktown Heights, NY, May 2013 | Slides

• Satisfied by Message Passing: Probabilistic Techniques for Combinatorial Problems

  Lukas Kroc, Ashish Sabharwal, Bart SelmanAAAI 2008Shorter version also at: LION 2009 | Bibliography

• Combinatorial Problems (series of three lectures)

  Ashish Sabharwal, Bart SelmanKITPC 2008
  SlidesFinding Solutions | Counting and Sampling Solutions | The Next Level of Complexity

• Beyond Traditional SAT Reasoning: QBF, Model Counting, and Solution Sampling

  Ashish Sabharwal, Bart SelmanAAAI 2007Bibliography | AAAI-07 Tutorial

• Quantified Boolean Formula (QBF) Reasoning

  Bart Selman, Carla Gomes, Ashish SabharwalTutorial prepared for DARPA, Feb 2007Slides | Video

Course Material

• CSE 326, Data Structures

  Fall 2003, University of Washington

• Notes on Proof Complexity

  Lectures by Paul Beame, scribed by Ashish SabharwalIAS/PCMI Summer School, Princeton, NJ, Aug 2000