Ashish Sabharwal
Senior Research Scientist
Publications
Conference Papers  Journal Articles  Book Chapters, Surveys  Workshops, Invited Talks, Etc.  Tutorials, Teaching

Question Answering as Global Reasoning over Semantic Abstractions
We propose a novel method for exploiting the semantic structure of text to answer multiplechoice 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 offtheshelf, generalpurpose, pretrained 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 stateofthe 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
We present a new dataset and model for textual entailment, derived from treating multiplechoice questionanswering 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 nonentailed pairs, makes this new entailment task particularly difficult. The resulting challenge is evidenced by stateoftheart 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
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 highprobability 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
Given a knowledge base or KB containing (noisy) facts about common nouns or generics, such as "all trees produce oxygen" or "some animals live in forests", we consider the problem of inferring additional such facts at a precision similar to that of the starting KB. Such KBs capture general knowledge about the world, and are crucial for various applications such as question answering. Different from commonly studied named entity KBs such as Freebase, generics KBs involve quantification, have more complex underlying regularities, tend to be more incomplete, and violate the commonly used locally closed world assumption (LCWA). We show that existing KB completion methods struggle with this new task, and present the first approach that is successful. Our results demonstrate that external information, such as relation schemas and entity taxonomies, if used appropriately, can be a surprisingly powerful tool in this setting. First, our simple yet effective knowledge guided tensor factorization approach achieves stateoftheart results on two generics KBs (80% precise) for science, doubling their size at 74%86% precision. Second, our novel taxonomy guided, submodular, active learning method for collecting annotations about rare entities (e.g., oriole, a bird) is 6x more effective at inferring further new facts about them than multiple active learning baselines.

How Good Are My Predictions? Efficiently Approximating PrecisionRecall Curves for Massive Datasets
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 costeffectively approximating precisionrecall (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. Less

Learning What is Essential in Questions
Question answering (QA) systems are easily distracted by irrelevant or redundant words in questions, especially when faced with long or multisentence 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 stateoftheart QA solvers for elementarylevel 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 crowdsourced essential terms annotated science questions. Less

Answering Complex Questions Using Open Information Extraction
While there has been substantial progress in factoid questionanswering (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 semistructured knowledge for QA, but to date such knowledge has only been used to answer simple questions with retrievalbased 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 stateoftheart structured solver on complex questions of varying difficulty, while also removing the reliance on manually curated knowledge. Less

Question Answering via Integer Programming over SemiStructured Knowledge
Answering science questions posed in natural language is an important AI challenge. Answering such questions often requires nontrivial 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 semistructured knowledge base derived from text, including questions requiring multistep 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. Less

Combining Retrieval, Statistics, and Inference to Answer Elementary Science Questions
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 semiautomatically 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 nondiagram, multiple choice questions), and show that our overall system’s score is 71.3%, an improvement of 23.8% (absolute) over the MLNbased 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. Less

Selecting NearOptimal Learners via Incremental Data Allocation
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 nearoptimal 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 realworld 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 sublinear 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 realworld datasets only entail mild violations of the theoretical scenario, suggesting that the practical behavior of DAUB is likely to approach the idealized behavior. Less

Closing the Gap Between Short and Long XORs for Model Counting
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 nontrivial 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. Less

Exact Sampling with Integer Linear Programs and Random Perturbations
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 treewidth 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 lowdimensional perturbation method. Less

Adaptive Concentration Inequalities for Sequential Decision Problems
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 Hoeffdinglike 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. Less

Beyond Parity Constraints: Fourier Analysis of Hash Functions for Inference
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 highdimensional 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 wellstudied 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 realworld benchmarks. Less

Parsing Algebraic Word Problems into Equations
This paper formalizes the problem of solving multisentence 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 singleequation problems, yielding a 15% to 50% reduction in error. Less

Exploring Markov Logic Networks for Question Answering
Elementarylevel 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 wordbased baseline approaches. Less

BDDGuided Clause Generation
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. Less

Insights Into Parallelism with Intensive Knowledge Sharing
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 discrepancybased 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 wellknown 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. Less

NonRestarting SAT Solvers With Simple Preprocessing Can Efficiently Simulate Resolution
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 nonstandard and nonasserting 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 nonrestarting 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 nonrestarting. Less

Designing Fast Absorbing Markov Chains
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 gradientbased 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. Less

Lowdensity Parity Constraints for HashingBased Discrete Integration
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 highdimensional 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 lowdensity 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. Less

Parallel Combinatorial Optimization with Decision Diagrams
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 branchandbound 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 stateoftheart parallel integer programming when both use a single 32core machine. Less

Embed and Project: Discrete Sampling with Universal Hashing
We consider the problem of sampling from a probability distribution defined over a highdimensional discrete set, specified for instance by a graphical model. We propose a sampling algorithm, called PAWS, based on embedding the set into a higherdimensional space which is then randomly projected using universal hash functions to a lowerdimensional 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 stateoftheart 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. Less

Optimization With Parity Constraints: From Binary Codes to Discrete Integration
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 maxlikelihood 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. Less

Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization
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 constantfactor 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. Less

Algorithm Portfolios Based on CostSensitive Hierarchical Clustering
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 costsensitive hierarchical clustering model. Experimental results on SAT and MaxSAT show that the new method outperforms the most effective portfolio builders to date. Less

Resolution and Parallelizability: Barriers to the Efficient Parallelization of SAT Solvers
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 bestcase 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. Less

Large Landscape Conservation  Synthetic and RealWorld Datasets
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, costefficient 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 graphtheoretic optimization problems. We present a synthetic generator capable of creating families of randomized structured problems, capturing the essential features of realworld instances but allowing for a thorough typicalcase performance evaluation of different solution methods. We also present two largescale realworld datasets, including economic data on land cost, and species data for grizzly bears, wolverines and lynx. Less

Snappy: A Simple Algorithm Portfolio
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. Less

Stronger Inference Through Implied Literals from Conflicts and Knapsack Covers
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. Less

Boosting Sequential Solver Portfolios: Knowledge Sharing and Accuracy Prediction
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 metalevel 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. Less

Density Propagation and Improved Bounds on the Partition Function
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 messagepassing algorithm called Density Propagation (DP) for estimating this function. We show that DP is exact for treestructured graphical models and is, in general, a strict generalization of both sumproduct 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 finergrained density of state information is provably at least as tight as previously known bounds based on convexity of the logpartition function, and striclty stronger if a general condition holds. We conclude with empirical evidence of improvement over convex relaxations and meanfield based bounds. Less

Parallel SAT Solver Selection and Scheduling
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. Less

SatX10: A Scalable Plug & Play Parallel SAT Framework
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. Less

Learning BackClauses in SAT
SAT conflict analysis graphs have been used to learn additional clauses, which we refer to as backclauses. These clauses may be viewed as enabling the powerful notion of "probing": Backclauses 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 shortcutting 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 backclauses, proposed over a decade ago, are not yet part of standard clauselearning SAT solvers. Less
 Augmenting Clause Learning With Implied Literals

Guiding Combinatorial Search With UCT
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 stateoftheart MIP solver such as CPLEX can be boosted using UCT's guidance on a range of problem instances. Less

Accelerated Adaptive Markov Chain for Partition Function Computation
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 stateoftheart methods such as IJGP, TRW, and Gibbs sampling both in runtime and accuracy. We also show how obtaining a socalled density of states distribution allows for efficient weight learning in Markov Logic theories. Less

Algorithm Selection and Scheduling
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. Less

Constraint Reasoning and Kernel Clustering for Pattern Decomposition With Scaling
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 datadriven 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. Less

A General NogoodLearning Framework for PseudoBoolean MultiValued SAT
We formulate a general framework for pseudoBoolean multivalued nogoodlearning, generalizing conflict analysis performed by modern SAT solvers and its recent extension for disjunctions of multivalued 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. Less
 NonModelBased Algorithm Portfolios for SAT

An Empirical Study of Optimization for Maximizing Diffusion in Networks
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 simulationbased 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 "replan" 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 tradeoff between spending all budget upfront vs. saving part of it for later. Less

An Empirical Study of Optimal Noise and Runtime Distributions in Local Search
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 3CNF formulas and provide surprisingly simple analytical fits for the optimal (static) noise level and the runtime at optimal noise, as a function of the clausetovariable ratio. We also demonstrate, for the first time for local search, a powerlaw decay in the tail of the runtime distribution in the low noise regime. Finally, we discuss a Markov Chain model capturing this intriguing feature. Less

Understanding Sampling Style Adversarial Search Methods
UCT has recently emerged as an exciting new adversarial reasoning technique based on cleverly balancing exploration and exploitation in a MonteCarlo 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 indepth analysis of the potential of UCT in domainindependent 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. Less

Maximizing Spread of Cascades Using Network Design
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. Less

On Adversarial Search Spaces and SamplingBased Planning
Upper Confidence bounds applied to Trees (UCT), a banditbased MonteCarlo 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. Less

Integrating Systematic and Local Search Paradigms: A New Strategy for MaxSAT
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 multicore 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. Less

Relaxed DPLL Search for MaxSAT
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 lownoise 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. Less

Backdoors in the Context of Learning
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 ordersensitivity of branching can be exponentially smaller than “traditional” backdoors. We also study the effect of learning empirically. Less

Backdoors in the Context of Learning
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 seta 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. Less

MessagePassing and Local Heuristics as Decimation Strategies for Satisfiability
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 wellknown Belief Propagation (BP). Our results reveal that once we resolve convergence issues, BP itself can solve fairly hard random kSAT 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. Less

Counting Solution Clusters in Graph Coloring Problems Using Belief Propagation
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. Less

Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting
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 tradeoffs 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. Less

Connections in Networks: A Hybrid Approach
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 MIPbased optimization. Overall, this provides a much more scalable solution than simply optimizing a MIP model of the problem with Cplex. We report results for semistructured lattice instances as well as on real data used for the construction of a wildlife corridor for grizzly bears in the Northern Rockies region. Less

Filtering Atmost1 on Pairs of Set Variables

Tradeoffs in the Complexity of Backdoor Detection
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 stateoftheart constraint solvers. In particular, it was recently shown that the problem of identifying a strong Horn or 2CNFbackdoor 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 worstcase complexity results for strong backdoor detection, we show that SatzRand 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. Less

Survey Propagation Revisited
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 nontrivial 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 reopens 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. Less

The Impact of Network Topology on Pure Nash Equilibria in Graphical Games
Graphical games capture some of the key aspects relevant to the study and design of multiagent 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. Less

Counting CSP Solutions Using Generalized XOR Constraints
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 socalled 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. Less

Short XORs for Model Counting: From Theory to Practice
A promising approach for model counting was recently introduced, which in theory requires the use of large random xor or parity constraints to obtain nearexact 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. Less

Connections in Networks: Hardness of Feasibility versus Optimality
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 worstcase hardness and approximability. We then provide a typicalcase analysis by means of a detailed computational study. First, we identify an easyhardeasy 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 easyhardeasy pro file for the optimization component itself. Less

From Sampling to Model Counting
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 nearuniform 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. Less

NearUniform Sampling of Combinatorial Spaces Using XOR Constraints
We propose a new technique for sampling the solutions of combinatorial problems in a nearuniform 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 nearuniformly. The final sample is identified amongst the remaining ones using a stateoftheart 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. Less

Revisiting the Sequence Constraint
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. Less

QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
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 reinventing 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 suboptimal. We take a step back and propose a new approach to QBF modeling based on a gametheoretic view of problems and on a dual CNFDNF (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 socalled 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. Less

Model Counting: A New Strategy for Obtaining Good Bounds
Model counting is the classical problem of computing the number of solutions of a given propositional formula. It vastly generalizes the NPcomplete 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 socalled 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 nontrivial 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. Less

Friends or Foes? An AI Planning Perspective on Abstraction and Search
There is increasing awareness that planning and model checking are closely related fields. Abstraction means to perform search in an overapproximation 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 (overapproximation) methods known in planning, we prove that they cannot improve the bestcase 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 resolutionstyle proofs of unsolvability underlying SATbased optimal planners. This result is potentially relevant also for model checking, where SATbased techniques have recently been combined with abstraction. Exploring the issue in planning practice, we find that even handmade 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. Less

SymChaff: A StructureAware Satisfiability Solver
We present a novel lowoverhead framework for encoding and utilizing structural symmetry in propositional satisfiability algorithms (SAT solvers). We use the notion of complete multiclass 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. Less

Using Problem Structure for Efficient Clause Learning
DPLL based clause learning algorithms for satisfiability testing are known to work very well in practice. However, like most branchandbound 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. Less

Understanding the Power of Clause Learning
Efficient implementations of DPLL with the addition of clause learning are the fastest complete satisfiability solvers and can handle many significant realworld 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. Less

Boundeddepth Frege Lower Bounds for Weaker Pigeonhole Principles
We prove a quasipolynomial lower bound on the size of boundeddepth Frege proofs of the pigeonhole principle PHPm n where m = (1 + 1=polylog n)n. This lower bound qualitatively matches the known quasipolynomialsize boundeddepth 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. Less
 Resolution Complexity of Independent Sets in Random Graphs
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005 and earlier
Journal Articles

Tradeoffs in the Complexity of Backdoors to Satisfiability: Dynamic SubSolvers and Learning During Search

Wildlife Corridors as a Connected Subgraph Problem

Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting
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 tradeoffs 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. Less

Predicting direct protein interactions from affinity purification mass spectrometry data
Background: Affinity purification followed by mass spectrometry identification (APMS) is an increasingly popular approach to observe proteinprotein interactions (PPI) in vivo. One drawback of APMS, 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 APMS experiments, under which the problem of separating direct interactions from indirect ones is formulated. Then, given idealized quantitative APMS 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 APMS PPI data from yeast, and its performance is measured against a highquality interaction dataset. Conclusions: As the sensitivity of APMS 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. Less

Friends or Foes? On Planning as Satisfiability and Abstract CNF Encodings
Planning as satisfiability, as implemented in, for instance, the SATPLAN tool, is a highly competitive method for finding parallel stepoptimal 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. Less

Towards Understanding and Harnessing the Potential of Clause Learning
Efficient implementations of DPLL with the addition of clause learning are the fastest complete Boolean satisfiability solvers and can handle many significant realworld 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 wellstudied 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 DavisPutnam 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 speedups on grid and randomized pebbling problems, as well as substantial improvements on certain ordering formulas. Less

New Filtering Algorithms for Combinations of Among Constraints
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. Less

SymChaff: Exploiting Symmetry in a StructureAware Satisfiability Solver
This article presents a new lowoverhead 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 socalled symmetry sets and variable classes, captures variable semantics relevant to "complete multiclass 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 pseudoBoolean representations, general grouptheoretic methods, and ZBDDs. We demonstrate the efficacy of our technique through a solver called SymChaff, which achieves exponential speedup over DPLLbased SAT solvers on problems from both theory and practice, often by simply using natural tags or annotation in the problem specification. Less
 The Resolution Complexity of Independent Sets and Vertex Covers in Random Graphs
 BoundedDepth Frege Lower Bounds for Weaker Pigeonhole Principles
 Floodlight Illumination of Infinite Wedges
Book Chapter and Surveys
 Book Review: S. Russell, P. Norvig, Artificial Intelligence: A Modern Approach, Third Edition
 Incomplete Algorithms (for Satisfiability)
 Model Counting
 Exploiting Runtime Variation in Complete Solvers (for Satisfiability)
 Satisfiability Solvers
Workshops, Invited Talks, Other Work

Automatic Construction of InferenceSupporting Knowledge Bases
 General NogoodLearning Framework for PseudoBoolean MultiValued SAT
 Guiding Combinatorial Optimization with UCT

On the Behavior of UCT in Synthetic Search Spaces

A flat histogram method for inference with probabilistic and deterministic constraints

Bridging Constraint Reasoning and Machine Learning for Unsupervised Labeling and Decomposition

Backdoors in the Context of Combinatorial Optimization and Learning

Game Playing Techniques for Optimization Under Uncertainty

Computational Thinking for Material Discovery: Bridging Constraint Reasoning and Learning

Optimal Network Design for the Spread of Cascades
 Approximate Inference for Clusters in Solution Spaces

Connections in Networks: A Hybrid Approach

Optimizing Fish Passage Barrier Removal Using Mixed Integer Linear Programming

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

Backdoors in the Context of Learning

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

Domain Filtering for the Intersection of Set Variables

Solution Counting Methods for Combinatorial Problems

Hidden Structure in Constraint Reasoning Problems

Counting CSP Solutions Using Generalized XOR Constraints

Optimal Corridor Design for Grizzly Bear in the U.S. Northern Rockies
 Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting
 Tradeoffs in Backdoors: Inconsistency Detection, Dynamic Simplification, and Preprocessing

Hidden Structure in Combinatorial Problems

Filtering Algorithms for the Sequence Constraint
 Two Set Constraints for Modeling and Efficiency

Sampling and Soundness: Can We Have Both?

Empirical Validation of the Relationship Between Survey Propagation and Covers in Random 3SAT
 Sparse Message Passing Algorithms for Weighted Maximum Satisfiability

Streamlining Reasoning for Solution Finding and Counting

Algorithmic Applications of Propositional Proof Complexity
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 realworld 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 resolutionbased 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 structureaware SAT solvers based on highlevel problem descriptions. We present empirical studies which demonstrate that one can achieve enormous speedup in practice by incorporating variable orders as well as symmetry information obtained directly from the underlying problem domain. Less
 Model Checking: Two Decades of Novel Techniques and Trends
Tutorials and Teaching

Branching Strategies and Restarts in SAT Solvers
 Satisfied by Message Passing: Probabilistic Techniques for Combinatorial Problems

Combinatorial Problems (series of three lectures)

Beyond Traditional SAT Reasoning: QBF, Model Counting, and Solution SamplingAshish Sabharwal, Bart Selman AAAI 2007 Bibliography

Quantified Boolean Formula (QBF) Reasoning
 CSE 326, Data Structures
 Notes on Proof Complexity