Implementing the Davis–Putnam Method

The method proposed by Davis, Putnam, Logemann, and Loveland for propositional reasoning, often referred to as the Davis–Putnam method, is one of the major practical methods for the satisfiability (SAT) problem of propositional logic. We show how to implement the Davis–Putnam method efficiently using the trie data structure for propositional clauses. A new technique of indexing only the first and last literals of clauses yields a unit propagation procedure whose complexity is sublinear to the number of occurrences of the variable in the input. We also show that the Davis–Putnam method can work better when unit subsumption is not used. We illustrate the performance of our programs on some quasigroup problems. The efficiency of our programs has enabled us to solve some open quasigroup problems.     

Resolution versus Search: Two Strategies for SAT

The paper compares two popular strategies for solving propositional satisfiability, backtracking search and resolution, and analyzes the complexity of a directional resolution algorithm (DR) as a function of the width (w ^*) of the problem"s graph. Our empirical evaluation confirms theoretical prediction, showing that on low-w ^* problems DR is very efficient, greatly outperforming the backtracking-based Davis–Putnam–Logemann–Loveland procedure (DP). We also emphasize the knowledge-compilation properties of DR and extend it to a tree-clustering algorithm that facilitates query answering. Finally, we propose two hybrid algorithms that combine the advantages of both DR and DP. These algorithms use control parameters that bound the complexity of resolution and allow time/space trade-offs that can be adjusted to the problem structure and to the user"s computational resources. Empirical studies demonstrate the advantages of such hybrid schemes.     

Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m)

The goal of this paper is to propose a new technique for developing decision procedures for propositional modal logics. The basic idea is that propositional modal decision procedures should be developed on top of propositional decision procedures. As a case study, we consider satisfiability in modal K(m), that is modal K with m modalities, and develop an algorithm, called K , on top of an implementation of the Davis–Putnam–Longemann–Loveland procedure. K is thoroughly tested and compared with various procedures and in particular with the state-of-the-art tableau-based system K . The experimental results show that K outperforms K and the other systems of orders of magnitude, highlight an intrinsic weakness of tableau-based decision procedures, and provide partial evidence of a phase transition phenomenon for K(m).     

Distributed state space minimization

We present a new algorithm, and its distributed implementation, for reducing labeled transition systems modulo strong bisimulation. The base of this algorithm is the Kanellakis–Smolka “naive method”, which has a high theoretical complexity but is successful in practice and well suited to parallelization. This basic approach is combined with optimizations inspired by the Kanellakis–Smolka algorithm for the case of bounded fanout, which has the best known time complexity. The distributed implementation is improved with respect to previous attempts by a better overlap between communication and computation, which results in an efficient usage of both memory and processing power. We also discuss the time complexity of this algorithm and show experimental results with sequential and distributed prototype tools.     

Satisfiability checking using Boolean Expression Diagrams

In this paper we present an algorithm for determining satisfiability of general Boolean formulas which are not necessarily in conjunctive normal form. The algorithm extends the well-known Davis–Putnam algorithm to work on Boolean formulas represented using Boolean Expression Diagrams (BEDs). The BED data structure allows the algorithm to take advantage of the built-in reduction rules and the sharing of sub-formulas. Furthermore, it is possible to combine the algorithm with traditional BDD construction (using Bryants Apply-procedure). By adjusting a single parameter to the BedSat algorithm, it is possible to control to what extent the algorithm behaves like the Apply-algorithm or like a SAT-solver. Thus, the algorithm can be seen as bridging the gap between standard SAT-solvers and BDDs. We present promising experimental results for 566 non-clausal formulas obtained from the multi-level combinational circuits in the ISCAS85 benchmark suite and from performing model checking of a shift-and-add multiplier.     

Equivariant Unification

Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logic programming, term rewriting, and automated theorem proving techniques that support reasoning about languages with name-binding. These applications often require nominal unification, or equational reasoning and constraint solving in nominal logic. Urban, Pitts and Gabbay developed an algorithm for a broadly applicable class of nominal unification problems. However, because of nominal logic’s equivariance property, these applications also require a different form of unification, which we call equivariant unification. In this article, we first study the complexity of the decision problem for equivariant unification and equivariant matching. We show that these problems are NP-hard in general, as is nominal unification without the ground-name restrictions employed in previous work on nominal unification. Moreover, we present an exponential-time algorithm for equivariant unification that can be used to decide satisfiability, or produce a complete finite set of solutions. We also study special cases that can be solved efficiently. In particular, we present a polynomial time algorithm for swapping-free equivariant matching, that is, for matching problems in which the swapping operation does not appear.     

New Worst-Case Upper Bounds for SAT

In 1980 Monien and Speckenmeyer proved that satisfiability of a propositional formula consisting of K clauses (of arbitrary length) can be checked in time of the order 2 ^{K / 3}. Recently Kullmann and Luckhardt proved the worst-case upper bound 2 ^{L / 9}, where L is the length of the input formula. The algorithms leading to these bounds are based on the splitting method, which goes back to the Davis–Putnam procedure. Transformation rules (pure literal elimination, unit propagation, etc.) constitute a substantial part of this method. In this paper we present a new transformation rule and two algorithms using this rule. We prove that these algorithms have the worst-case upper bounds 2^{0. 30897 K} and 2^{0. 10299 L} , respectively.     

Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT

An analysis of the hardness of resolution of random 3-SAT instances using the Davis–Putnam–Loveland–Logemann (DPLL) algorithm slightly below threshold is presented. While finding a solution for such instances demands exponential effort with high probability, we show that an exponentially small fraction of resolutions require a computation scaling linearly in the size of the instance only. We compute analytically this exponentially small probability of easy resolutions from a large deviation analysis of DPLL with the Generalized Unit Clause search heuristic, and show that the corresponding exponent is smaller (in absolute value) than the growth exponent of the typical resolution time. Our study therefore gives some quantitative basis to heuristic restart solving procedures, and suggests a natural cut-off cost (the size of the instance) for the restart.     

Partial Functions in a Total Setting

We discuss a scheme for defining and reasoning about partial recursive functions within a classical two-valued logic in which all terms denote. We show how a total extension of the partial function introduced by a recursive declaration may be axiomatized within a classical logic, and illustrate by an example the kind of reasoning that our scheme supports. By presenting a naive set-theoretic semantics, we show that the system we propose is logically consistent. Our work is motivated largely by the pragmatic issues arising from mechanical theorem proving – we discuss some of the practical benefits and limitations of our scheme for mechanical verification of software and hardware systems.     

A solver for QBFs in negation normal form

Various problems in artificial intelligence can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula’s structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and describe a solver, $\ensuremath{\sf qpro}Various problems in artificial intelligence can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula’s structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and describe a solver, , which is able to handle arbitrary formulas. To this end, we extend algorithms for QBFs to the non-normal form case and compare with the leading normal form provers on several problems from the area of artificial intelligence. We prove properties of the algorithms generalized to non-clausal form by using a novel approach based on a sequent-style formulation of the calculus. This paper is based on an extended abstract presented at ECAI 2006 (see [16]). This work was supported by the Austrian Science Fund (FWF) under grant P18019, the Austrian Academic Exchange Service (?AD) under grant Amadée 2/2006, and by the Austrian Federal Ministry of Transport, Innovation and Technology BMVIT and the Austrian Research Promotion Agency FFG under grant FIT-IT-810806.     

The Hot List Strategy

Experimentation strongly suggests that, for attacking deep questions and hard problems with the assistance of an automated reasoning program, the more effective paradigms rely on the retention of deduced information. A significant obstacle ordinarily presented by such a paradigm is the deduction and retention of one or more needed conclusions whose complexity sharply delays their consideration. To mitigate the severity of the cited obstacle, I formulated and feature in this article the hot list strategy. The hot list strategy asks the researcher to choose, usually from among the input statements characterizing the problem under study, one or more statements that are conjectured to play a key role for assignment completion. The chosen statements – conjectured to merit revisiting, again and again – are placed in an input list of statements, called the hot list. When an automated reasoning program has decided to retain a new conclusion C – before any other statement is chosen to initiate conclusion drawing – the presence of a nonempty hot list (with an appropriate assignment of the input parameter known as heat) causes each inference rule in use to be applied to C together with the appropriate number of members of the hot list. Members of the hot list are used to complete applications of inference rules and not to initiate applications. The use of the hot list strategy thus enables an automated reasoning program to briefly consider a newly retained conclusion whose complexity would otherwise prevent its use for perhaps many CPU-hours. To give evidence of the value of the strategy, I focus on four contexts: (1) dramatically reducing the CPU time required to reach a desired goal, (2) finding a proof of a theorem that had previously resisted all but the more inventive automated attempts, (3) discovering a proof that is more elegant than previously known, and (4) answering a question that had steadfastly eluded researchers relying on an automated reasoning program. I also discuss a related strategy, the dynamic hot list strategy (formulated by my colleague W. McCune), that enables the program during a run to augment the contents of the hot list. In the Appendix, I give useful input files and interesting proofs. Because of frequent requests to do so, I include challenge problems to consider, commentary on my approach to experimentation and research, and suggestions to guide one in the use of McCunes automated reasoning program OTTER.     

Integrating advanced reasoning into a SAT solver

1 Introduction The SAT (Satisfiability) problem is one of the basic NP problems that have been widely researched. Many problems in EDA (Electronics Design Automation) domain such as ATPG (Automatic Test Pattern Generation), Logic Synthesis, Equivalence Checking[1] and Model Checking[2] can be reduced to the SAT problem. Typical algorithms for SAT can be classified into two categories: incomplete and complete ones. The former, including GSAT[3] and WalkSAT[4], are based on local…     

A parallel algorithm for the 0–1 knapsack problem

Research efforts on parallel exact algorithms for the 0–1 knapsack problem have up to now concentrated on solving small problems (at most 1,000 objects) and in many cases results have only been obtained by simulation of the parallel algorithm. After a brief review of a well known sequential branch-and-bound algorithm we discuss a new parallel algorithm for the 0–1 knapsack problem which exploits the potential parallelism that exists during the backtracking steps of the branch-and-bound algorithm. We report results for our parallel algorithm on a transputer network for problems with up to 20,000 objects. The speedup obtained is nearly linear for 2, 4, and 8 processors except when there is a strong correlation between the profit and weight of the objects.     

Dimension–Adaptive Tensor–Product Quadrature

We consider the numerical integration of multivariate functions defined over the unit hypercube. Here, we especially address the high–dimensional case, where in general the curse of dimension is encountered. Due to the concentration of measure phenomenon, such functions can often be well approximated by sums of lower–dimensional terms. The problem, however, is to find a good expansion given little knowledge of the integrand itself. The dimension–adaptive quadrature method which is developed and presented in this paper aims to find such an expansion automatically. It is based on the sparse grid method which has been shown to give good results for low- and moderate–dimensional problems. The dimension–adaptive quadrature method tries to find important dimensions and adaptively refines in this respect guided by suitable error estimators. This leads to an approach which is based on generalized sparse grid index sets. We propose efficient data structures for the storage and traversal of the index sets and discuss an efficient implementation of the algorithm. The performance of the method is illustrated by several numerical examples from computational physics and finance where dimension reduction is obtained from the Brownian bridge discretization of the underlying stochastic process.     

Complexity of constructing Dixon resultant matrix

Dixon resultant is a fundamental tool of elimination theory in the study and practice of algebraic geometry. It has provided the efficient and practical solutions to some benchmark problems in a variety of application domains, such as automated reasoning, automatic control, and solid modelling. The major task of solutions is to construct the Dixon resultant matrix, the entries of which are more complicated than the entries of other resultant matrices. An existing extended recurrence formula can construct the Dixon resultant matrix fast. In this paper, we present a detailed analysis of the computational complexity of the recurrence formula for the general multivariate setting. Parallel computation can be applied to speed up the recursive procedure. Furthermore, we also generalize the computational complexity of three bivariate polynomials to the general multivariate case by using the construction of standard Dixon resultant matrix. Some experimental results are demonstrated by a range of nontrivial examples.     

Quantitative temporal reasoning

A substantially large class of programs operate in distributed and real-time environments, and an integral part of their correctness specification requires the expression of time-critical properties that relate the occurrence of events of the system. We focus on the formal specification and reasoning about the correctness of such programs. We propose a system of temporal logic, RTCTL (Real-Time Computation Tree Logic), that allows the melding of qualitative temporal assertions together with real-time constraints to permit specification and reasoning at the twin levels of abstraction: qualitative and quantitative. We argue that many practically useful correctness properties of temporal systems, which need to express timing as an essential part of their functionality requirements, can be expressed in RTCTL. We develop a model-checking algorithm for RTCTL whose complexity is linear in the size of the RTCTL specification formula and in the size of the structure. We also present an essentially optimal, exponential time tableau-based decision procedure for the satisfiability of RTCTL formulae. Finally, we consider several variants and extensions of RTCTL for real-time reasoning.The work of E.A. Emerson was supported in part by NSF grant DCR-8511354, ONR URI contract N00014-86-K-0763, and Netherlands NWO grant nf-3/nfb 62-500. The work of A.K.Mok was supported in part by ONR Grant number N00014-89-J-1472 and Texas Advanced Technology Program Grant 003658-250. A summary of these results was presented at the Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, June 12–14, 1989.     

Quantum Mereotopology

While mereotopology – the theory of boundaries, contact and separation built up on a mereological foundation – has found fruitful applications in the realm of qualitative spatial reasoning, it faces problems when its methods are extended to deal with those varieties of spatial and non-spatial reasoning which involve a factor of granularity. This is because granularity cannot easily be represented within a mereology-based framework. We sketch how this problem can be solved by means of a theory of granular partitions, a theory general enough to comprehend not only the familiar sorts of spatial partitions but also a range of coarse-grained partitions of other, non-spatial sorts. We then show how these same methods can be extended to apply to finite sequences of granular partitions evolving over time, or to what we shall call coarse- and fine-grained histories.     

求解QBF 问题的启发式调查传播算法

提出了一种启发式调查传播算法,并基于该算法设计了一种QBF(quantified Boolean formulae)求解器——HSPQBF(heuristic survey propagation algorithm for solving QBF)系统.它将Survey Propagation信息传递方法应用到QBF求解问题中.利用Survey Propagation作为启发式引导DPLL(Davis,Putnam,Logemann and Loveland)算法,选择合适的变量进行分支,从而可以减小搜索空间,并减少算法回退的次数.在分支处理过程中,HSPQBF系统结合了单元传播、冲突学习和满足蕴涵学习等一些优秀的QBF求解技术,从而能够提高QBF问题的求解效率.实验结果表明,HSPQBF无论在随机问题上还是在QBF标准测试问题上都有很好的表现,验证了调查传播技术在QBF问题求解中的实际价值.