Jinbo Huang

AIJ Journal 2013 Journal Article

Decomposition and tractability in qualitative spatial and temporal reasoning

• Jinbo Huang
• Jason Jingshi Li
• Jochen Renz

Constraint networks in qualitative spatial and temporal reasoning (QSTR) typically feature variables defined on infinite domains. Mainstream algorithms for deciding network consistency are based on searching for network refinements whose consistency is known to be tractable, either directly or by using a SAT solver. Consequently, these algorithms treat all networks effectively as complete graphs, and are not directly amenable to complexity bounds based on network structure, such as measured by treewidth, that are well known in the finite-domain case. The present paper makes two major contributions, spanning both theory and practice. First, we identify a sufficient condition under which consistency can be decided in polynomial time for networks of bounded treewidth in QSTR, and show that this condition is satisfied by a range of calculi including the Interval Algebra, Rectangle Algebra, Block Algebra, RCC8, and RCC5. Second, we apply the techniques used in establishing these results to a SAT encoding of QSTR, and obtain a new, more compact encoding which is also guaranteed to be solvable in polynomial time for networks of bounded treewidth, and which leads to a significant advance of the state of the art in solving the hardest benchmark problems.

KR Conference 2012 Conference Paper

Compactness and Its Implications for Qualitative Spatial and Temporal Reasoning

• Jinbo Huang

problem of deciding whether a set of equalities and inequalities between rational variables is satisfiable, which corresponds to the well-known CSP for the Point Algebra (Vilain and Kautz 1986). Our first result shows that CSP(A) has compactness if the template A is ω-categorical, that is, if A is the unique countable model, up to isomorphism, of the set of all first-order sentences that are true in A. The structure P mentioned above, for example, is ω-categorical (Hirsch 1996), implying that the CSP for the Point Algebra has compactness. While compactness involves infinite constraint networks, our second result shows that it has useful consequences where we are dealing only with finite networks. Specifically, we show that where compactness holds, the recently introduced patchwork property (Lutz and Milic̆ić 2007) is equivalent to the existence of a canonical solution for every finite satisfiable network, which is a solution that can be extended into a solution for any finite satisfiable extension of the network. These two results for general CSPs have important corollaries that significantly strengthen and expand previous results in the field of qualitative reasoning: A constraint satisfaction problem has compactness if any infinite set of constraints is satisfiable whenever all its finite subsets are satisfiable. We prove a sufficient condition for compactness, which holds for a range of problems including those based on the well-known Interval Algebra (IA) and RCC8. Furthermore, we show that compactness leads to a useful necessary and sufficient condition for the recently introduced patchwork property, namely that patchwork holds exactly when every satisfiable finite network (i. e., set of constraints) has a canonical solution, that is, a solution that can be extended to a solution for any satisfiable finite extension of the network. Applying these general theorems to qualitative reasoning, we obtain important new results as well as significant strengthenings of previous results regarding IA, RCC8, and their fragments and extensions. In particular, we show that all the maximal tractable fragments of IA and RCC8 (containing the base relations) have patchwork and canonical solutions as long as networks are algebraically closed.

ECAI Conference 2012 Conference Paper

Implementation of Critical Path Heuristics for SAT

• Jinbo Huang

Recent work has shown that SAT can be theoretically more powerful than heuristic search provided the heuristic used by search is implemented as a set of clauses on which unit propagation simulates the evaluation of the heuristic. The hmaxheuristic has been shown to be implemented trivially by the empty set of clauses. This paper presents an implementation of hm, a generalization of hmax.

ECAI Conference 2012 Conference Paper

SAT vs. Search for Qualitative Temporal Reasoning

• Jinbo Huang

Empirical data from recent work has indicated that SAT-based solvers can outperform native search-based solvers on certain classes of problems in qualitative temporal reasoning, particularly over the Interval Algebra (IA). The present work shows that, for reasoning with IA, SAT strictly dominates search in theoretical power: (1) We present a SAT encoding of IA that simulates the use of tractable subsets in native solvers. (2) We show that the refutation of any inconsistent IA network can always be done by SAT (via our new encoding) as efficiently as by native search. (3) We exhibit a class of IA networks that provably require exponential time to refute by native search, but can be refuted by SAT in polynomial time.

KR Conference 2012 Short Paper

Search Strategy Simulation in Constraint Booleanization

• Jinbo Huang

better solution methods. In other words, the goal in this case is not necessarily to devise a Booleanization that will outperform native methods for constraints of type X, but rather one whose effectiveness is maximized, particularly by capitalizing on successful techniques used in native methods. It is in this spirit that we propose, in this work, a new, substantially improved Boolean encoding of C UMULATIVE, one of the the most widely used global constraints (Rossi, van Beek, and Walsh 2006). We first present an encoding that utilizes recent advances in solving pseudo-Boolean (PB) constraints (Eén and Sörensson 2006), and then show how we can augment the encoding to effectively simulate domain splitting, a search strategy known to be beneficial for C U MULATIVE constraints in native search algorithms (Simonis and O’Sullivan 2008; Huang and Korf 2009). Empirical results indicate that our new encoding leads to significant improvements over the original Booleanization, while we observe, on the other hand, the efficiency of native solvers over our Booleanization on some of the benchmarks. In concluding the paper, we discuss analytically some strength and weaknesses of our work. Within the recently proposed Universal Booleanization framework, we consider the C UMULATIVE constraint, for which the original Boolean encoding proves ineffective, and present a new Boolean encoding that causes the SAT solver to simulate, largely, the search strategy used by some of the best-performing native methods. Apart from providing motivation for future research in a similar direction, we obtain a significantly enhanced version of Universal Booleanization for problems containing C UMULATIVE constraints.

AAAI Conference 2010 Conference Paper

Computing Cost-Optimal Definitely Discriminating Tests

• Anika Schumann
• Jinbo Huang
• Martin Sachenbacher

The goal of testing is to discriminate between multiple hypotheses about a system—for example, different fault diagnoses—by applying input patterns and verifying or falsifying the hypotheses from the observed outputs. Definitely discriminating tests (DDTs) are those input patterns that are guaranteed to discriminate between different hypotheses of non-deterministic systems. Finding DDTs is important in practice, but can be very expensive ( p 2-complete). Even more challenging is the problem of finding a DDT that minimizes the cost of the testing process, i. e. , an input pattern that can be most cheaply enforced and that is a DDT. This paper addresses both problems. We show how we can transform a given problem into a Boolean structure in decomposable negation normal form (DNNF), and extract from it a Boolean formula whose models correspond to DDTs. This allows us to harness recent advances in both knowledge compilation and satisfiability for efficient and scalable DDT computation in practice. Furthermore, we show how we can generate a DNNF structure compactly encoding all DDTs of the problem and use it to obtain a cost-optimal DDT in time linear in the size of the structure. Experimental results from a realworld application show that our method can compute DDTs in less than 1 second for instances that were previously intractable, and cost-optimal DDTs in less than 20 seconds where previous approaches could not even compute an arbitrary DDT.

AIJ Journal 2010 Journal Article

Extended clause learning

• Jinbo Huang

The past decade has seen clause learning as the most successful algorithm for SAT instances arising from real-world applications. This practical success is accompanied by theoretical results showing clause learning as equivalent in power to resolution. There exist, however, problems that are intractable for resolution, for which clause-learning solvers are hence doomed. In this paper, we present extended clause learning, a practical SAT algorithm that surpasses resolution in power. Indeed, we prove that it is equivalent in power to extended resolution, a proof system strictly more powerful than resolution. Empirical results based on an initial implementation suggest that the additional theoretical power can indeed translate into substantial practical gains.

KR Conference 2010 Conference Paper

New Advances in Sequential Diagnosis

• Sajjad Siddiqi
• Jinbo Huang

Sequential diagnosis takes measurements of an abnormal system to identify faulty components, where the goal is to reduce the diagnostic cost, defined here as the number of measurements. To propose measurement points, previous work employs a heuristic based on reducing the entropy over a set of diagnoses, which can be impractical when the set of diagnoses is too large. Focusing on a smaller set of probable diagnoses scales the approach but generally leads to increased diagnostic cost. We propose a new diagnostic framework employing three new techniques—a more efficient heuristic for measurement point selection, abstraction-based sequential diagnosis, and component cloning—which scales to large systems with good performance in terms of diagnostic cost. Figure 1: A faulty circuit. 1988) and compiled into deterministic decomposable negation normal form (d-DNNF) (Darwiche 2001; Darwiche and Marquis 2002; Darwiche 2003). Second, we extend hierarchical diagnosis, a technique based upon system abstraction (Siddiqi and Huang 2007), to handle probabilities so that it can be applied to sequential diagnosis to allow larger systems to be diagnosed. Finally, when the abstraction of a system is still too large to be compiled, we propose a new method of component cloning that converts the system into one that has a smaller abstraction. We use combinational circuits as an example of the type of systems we wish to diagnose. Our approach, however, applies as well to other types of systems as long as a probabilistic model is given that defines the behavior of the system. We now present the new techniques we have introduced starting with the system modeling and compilation method that underlies our new diangostic system.

IJCAI Conference 2009 Conference Paper

• Jason Jingshi Li
• Jinbo Huang
• Jochen Renz

Deciding consistency of constraint networks is a fundamental problem in qualitative spatial and temporal reasoning. In this paper we introduce a divide-and-conquer method that recursively partitions a given problem into smaller sub-problems in deciding consistency. We identify a key theoretical property of a qualitative calculus that ensures the soundness and completeness of this method, and show that it is satisfied by the Interval Algebra (IA) and the Point Algebra (PA). We develop a new encoding scheme for IA networks based on a combination of our divide-and-conquer method with an existing encoding of IA networks into SAT. We empirically show that our new encoding scheme scales to much larger problems and exhibits a consistent and significant improvement in efficiency over state-of-the-art solvers on the most difficult instances.

IJCAI Conference 2009 Conference Paper

• Sajjad Siddiqi
• Jinbo Huang

In Bayesian networks, a most probable explanation (MPE) is a most likely instantiation of all network variables given a piece of evidence. Recent work proposed a branch-and-boundsearch algorithm that finds exact solutions to MPE queries, where bounds are computed on a relaxed network obtained by a technique known as node splitting. In this work we study the impact of variable and value ordering on such a search algorithm. We study several heuristics based on the entropies of variables and on the notion of nogoods, and propose a new meta-heuristic that combines their strengths. Experiments indicate that search efficiency is significantly improved, allowing many hard problems to be solved for the first time.

IJCAI Conference 2007 Conference Paper

• Elena Kelareva
• Olivier Buffet
• Jinbo Huang
• Sylvie Thi
• eacute; baux

Improving AI planning algorithms relies on the ability to exploit the structure of the problem at hand. A promising direction is that of factored planning, where the domain is partitioned into subdomains with as little interaction as possible. Recent work in this field has led to an detailed theoretical analysis of such approaches and to a couple of high-level planning algorithms, but with no practical implementations or with limited experimentations. This paper presents dTreePlan, a new generic factored planning algorithm which uses a decomposition tree to efficiently partition the domain. We discuss some of its aspects, progressively describing a specific implementation before presenting experimental results. This prototype algorithm is a promising contribution---with major possible improvements---and helps enrich the picture of factored planning approaches.

IJCAI Conference 2007 Conference Paper

• Jinbo Huang

Given the common use of restarts in today's clause learning SAT solvers, the task of choosing a good restart policy appears to have attracted remarkably little interest. On the other hand, results have been reported on the use of different restart policies for combinatorial search algorithms. Such results are not directly applicable to clause learning SAT solvers, as the latter are now understood as performing a form of resolution, something fundamentally different from search (in the sense of backtracking search for satisfying assignments). In this paper we provide strong evidence that a clause learning SAT solver could benefit substantially from a carefully designed restart policy (which may not yet be available). We begin by pointing out that the restart policy works together with other aspects of a SAT solver in determining the sequence of resolution steps performed by the solver, and hence its efficiency. In this spirit we implement a prototype clause learning SAT solver that facilitates restarts at arbitrary points, and conduct experiments on an extensive set of industrial benchmarks using various restart policies, including those used by well-known SAT solvers as well as a universal policy proposed in 1993 by Luby et al. The results indicate a substantial impact of the restart policy on the efficiency of the solver, and provide motivation for the design of better restart policies, particularly dynamic ones.

IJCAI Conference 2007 Conference Paper

• Sajjad Siddiqi
• Jinbo Huang

Due to large search spaces, diagnosis of combinational circuits is often practical for finding only single and double faults. In principle, system models can be compiled into a tractable representation (such as DNNF) on which faults of arbitrary cardinality can be found efficiently. For large circuits, however, compilation can become a bottleneck due to the large number of variables necessary to model the health of individual gates. We propose a novel method that greatly reduces this number, allowing the compilation, as well as the diagnosis, to scale to larger circuits. The basic idea is to identify regions of a circuit, called cones, that are dominated by single gates, and model the health of each cone with a single health variable. When a cone is found to be possibly faulty, we diagnose it by again identifying the cones inside it, and so on, until we reach a base case. We show that results combined from these hierarchical sessions are sound and complete with respect to minimum-cardinality diagnoses. We implement this method on top of the diagnoser developed by Huang and Darwiche in 2005, and present evidence that it significantly improves the efficiency and scalability of diagnosis on the ISCAS-85 circuits.

ICAPS Conference 2006 Conference Paper

Combining Knowledge Compilation and Search for Conformant Probabilistic Planning

• Jinbo Huang

We present a new algorithm for conformant probabilistic planning, which for a given horizon produces a plan that maximizes the probability of success under quantified uncertainty about the initial state and action effects, and absence of sensory information. Recent work has studied systematic search in the space of all candidate plans as a feasible approach to conformant probabilistic planning, but the algorithms proposed require caching of intermediate computations in such a way that memory is often exhausted quickly except for small planning horizons. On the other hand, planning problems in typical formulations generally have treewidths that do not grow with the horizon, as connections between variables are local to the neighborhood of each time step. These existing planners, however, are unable to directly benefit from the bounded treewidth owing to a constraint on the variable ordering which is necessary for correct computation of the optimal plan. We show that lifting such constraint allows one to obtain a compact compilation of the planning problem, from which an upper bound can be efficiently computed on the value of any partial plan generated during search. Coupled with several optimizations, this results in a depth-first branch-and-bound algorithm which on the tested domains runs an order of magnitude faster than its predecessors, and at the same time is able to solve problems for significantly larger horizons thanks to its minimal memory requirements.

AAAI Conference 2006 Conference Paper

Solving MAP Exactly by Searching on Compiled Arithmetic Circuits

• Jinbo Huang

The MAP (maximum a posteriori hypothesis) problem in Bayesian networks is to find the most likely states of a set of variables given partial evidence on the complement of that set. Standard structure-based inference methods for finding exact solutions to MAP, such as variable elimination and jointree algorithms, have complexities that are exponential in the constrained treewidth of the network. A more recent algorithm, proposed by Park and Darwiche, is exponential only in the treewidth and has been shown to handle networks whose constrained treewidth is quite high. In this paper we present a new algorithm for exact MAP that is not necessarily limited in scalability even by the treewidth. This is achieved by leveraging recent advances in compilation of Bayesian networks into arithmetic circuits, which can circumvent treewidth-imposed limits by exploiting the local structure present in the network. Specifically, we implement a branch-and-bound search where the bounds are computed using linear-time operations on the compiled arithmetic circuit. On networks with local structure, we observe orders-of-magnitude improvements over the algorithm of Park and Darwiche. In particular, we are able to efficiently solve many problems where the latter algorithm runs out of memory because of high treewidth.

IJCAI Conference 2005 Conference Paper

DPLL with a Trace: From SAT to Knowledge Compilation

• Jinbo Huang
• Adnan

We show that the trace of an exhaustive DPLL search can be viewed as a compilation of the propositional theory. With different constraints imposed or lifted on the DPLL algorithm, this compilation will belong to the language of d-DNNF, FBDD, and OBDD, respectively. These languages are decreasingly succinct, yet increasingly tractable, supporting such polynomial-time queries as model counting and equivalence testing. Our contribution is thus twofold. First, we provide a uniform framework, supported by empirical evaluations, for compiling knowledge into various languages of interest. Second, we show that given a particular variant of DPLL, by identifying the language membership of its traces, one gains a fundamental understanding of the intrinsic complexity and computational power of the search algorithm itself. As interesting examples, we unveil the “hidden power” of several recent model counters, point to one of their potential limitations, and identify a key limitation of DPLLbased procedures in general.

AAAI Conference 2005 Conference Paper

On Compiling System Models for Faster and More Scalable Diagnosis

• Jinbo Huang

Knowledge compilation is one of the more traditional approaches to model-based diagnosis, where a compiled system model is obtained in an off-line phase, and then used to efficiently answer diagnostic queries on-line. The choice of a suitable representation for the compiled model is critical to the success of this approach, and two of the main proposals have been Decomposable Negation Normal Form (DNNF) and Ordered Binary Decision Diagram (OBDD). The contribution of this paper is twofold. First, we show that in the current state of the art, DNNF dominates OBDD in efficiency and scalability for some typical diagnostic tasks. This result is based on a step-by-step comparison of the complexities of diagnostic algorithms for DNNF and OBDD, together with a known succinctness relation between the two representations. Second, we present a tool for model-based diagnosis, which is based on a state-of-the-art DNNF compiler and our implementations of DNNF diagnostic algorithms. We demonstrate the efficiency of this tool against recent results reported on diagnosis using OBDD.

SAT Conference 2004 Conference Paper

Using DPLL for Efficient OBDD Construction

• Jinbo Huang
• Adnan Darwiche

The DPLL procedure has found great success in SAT, where search terminates on the first solution discovered. We show that this procedure is equally promising in a problem where exhaustive search is used, given that it is augmented with appropriate caching. Specifically, we propose two DPLL-based algorithms that construct OBDDs for CNF formulas. These algorithms have a worst-case complexity that is linear in the number of variables and size of the CNF, and exponential only in the cutwidth or pathwidth of the variable ordering. We show how modern SAT techniques can be harnessed by implementing the algorithms on top of an existing SAT solver. We discuss the advantage of this new construction method over the traditional approach, where OBDDs for subsets of the CNF formula are built and conjoined. Our experiments indicate that on many CNF benchmarks, the new method runs orders of magnitude faster than a comparable implementation of the traditional method.

IJCAI Conference 2003 Conference Paper

A Structure-Based Variable Ordering Heuristic for SAT

• Jinbo Huang
• Adnan Darwiche

We propose a variable ordering heuristic for SAT, which is based on a structural analysis of the SAT problem. We show that when the heuristic is used by a Davis-Putnam SAT solver that employs conflict-directed backtracking, it produces a divide-and-conquer behavior in which the SAT problem is recursively decomposed into smaller problems that are solved independently. We discuss the implications of this divide-and-conquer behavior on our ability to provide structure-based guarantees on the complexity of Davis-Putnam SAT solvers. We also report on the integration of this heuristic with ZChaff— a state-of-the-art SAT solver—showing experimentally that it significantly improves performance on a range of benchmark problems that exhibit structure.