WWW.THESIS.DISLIB.INFO
FREE ELECTRONIC LIBRARY - Online materials, documents
 
<< HOME
CONTACTS



Pages:   || 2 | 3 | 4 | 5 |   ...   | 8 |

«David A. Plaisted Computer Science Department, University of North Carolina Chapel Hill, NC 27599-3175, USA Armin Biere ETH Z¨rich, Computer Systems ...»

-- [ Page 1 ] --

A Satisfiability Procedure for

Quantified Boolean Formulae

David A. Plaisted

Computer Science Department, University of North Carolina

Chapel Hill, NC 27599-3175, USA

Armin Biere

ETH Z¨rich, Computer Systems Institute

u

8092 Z¨rich, Switzerland

u

Yunshan Zhu

Advanced Technology Group, Synopsys Inc.

Mountain View, CA 94040, USA

Abstract

We present a satisfiability tester Qsat for quantified Boolean formulae and a restriction QsatCNF of Qsat to unquantified conjunctive normal form formulae. Qsat makes use of procedures which replace subformulae of a formula by equivalent formulae. By a sequence of such replacements, the original formula can be simplified to true or false. It may also be necessary to transform the original formula to generate a subformula to replace. QsatCNF eliminates collections of variables from an unquantified clause form formula until all variables have been eliminated. Qsat and QsatCNF can be applied to hardware verification and symbolic model checking.

Results of an implementation of QsatCNF are described, as well as some complexity results for Qsat and QsatCNF. Qsat runs in linear time on a class of quantified Boolean formulae related to symbolic model checking. We present the class of “long and thin” unquantified formulae and give evidence that this class is common in applications. We also give theoretical and empirical evidence that QsatCNF is often faster than Davis and Putnam-type satisfiability checkers and ordered binary decision diagrams (OBDDs) on this class of formulae. We give an example where QsatCNF is exponentially faster than BDDs.

Key words: QBF, Satisfiability, Davis & Putnam Procedure, BDDs, Cut Width, Circuit Verification, Model Checking.

Preprint submitted to Discrete Applied Mathematics 26 March 2002 Qsat is a new decision procedure for satisfiability of quantified Boolean formulae with potential applications to hardware verification and symbolic model checking. The philosophy of Qsat is to test satisfiability of a formula by repeatedly replacing subformulae by simpler equivalent subformulae. QsatCNF is an application of Qsat to unquantified clause form formulae, interpreted as quantified Boolean formulae by considering all free variables to be existentially quantified. Qsat and QsatCNF test satisfiability of a formula by successively eliminating variables from it, producing an equivalent formula, until all variables have been eliminated. The motivation for Qsat and QsatCNF is that satisfiability testers for unquantified formulae such as Davis and Putnam’s method seem tobe more efficient than BDDs (ordered BDDs, OBDDs) when there is not too much backtracking. BDDs can process large (unquantified) formulae because they make use of an ordering of the variables which breaks the processing down into smaller steps that are easier to perform. The idea of Qsat and QsatCNF is to import this BDD philosophy into satisfiability testing, by applying a modification of Davis and Putnam’s method not to the whole formula at once, but piece by piece, where each application of the modified Davis and Putnam method to a piece of the formula simplifies the formula. This reduces the amount of backtracking. Qsat and QsatCNF can be built on top of any satisfiability tester for unquantified Boolean formulae, including St˚almarck’s method [1].

It appears (see section 11) that BDDs are good for systems that are long and thin, such as adders. These are also systems for which QsatCNF should be efficient, because such systems can be broken into parts having a limited amount of communication between them. Each part corresponds to a subformula of the original formula. QsatCNF can simplify one such subformula, and then be applied recursively to the remaining formula. Thus it may be that QsatCNF is efficient on a large number of applications where BDDs are currently used.

Similarly, Qsat should be efficient for quantified Boolean formulae that are long and thin, in a certain sense. BDDs can also be efficient on problems that are not long and thin, such as some versions of barrel shifters. QsatCNF may not be as fast on such problems.

The general method by which Boolean formulae are used for system testing is

the following:

(1) A Boolean formula G is constructed from a system S and its specification, expressing that the system does not satisfy its specification. Methods for generating G are well known.

(2) The formula G is tested for satisfiability (consistency).

(3) If G is unsatisfiable, then S is correct. If G is satisfiable, then there is an Email addresses: plaisted@cs.unc.edu (David A. Plaisted), biere@inf.ethz.ch (Armin Biere), yunshan@synopsys.com (Yunshan Zhu).

error in S, and the nature of the satisfiability of G can help to identify the error in S.

The system S can be a computer circuit or some system containing interconnected objects, which can be defined as a component or part of a physical system, such as a gate in a circuit. The formula G can be obtained by defining the formula A as a Boolean formula representing the system S and B as a Boolean formula representing the statement that S fails to satisfy its specification. Then G can be taken to be the conjunction A ∧ B of these two formulae, expressing that S fails to satisfy its specification.





Binary decision diagrams (BDDs) [2] have been widely used in CAD applications such as logic synthesis, testing and formal verification. BDDs transform a circuit into a canonical form, depending on an ordering of the Boolean variables, and two circuits are equivalent if and only if they have the same canonical form. For many kinds of circuits, BDDs work very well, especially when a good ordering of the variables can be found. Equivalence checking [3,4] is important, because one can verify a new or optimized circuit by showing that it is equivalent to an old and trusted circuit. Commercial equivalence checkers can now verify circuits with millions of gates which are clearly out of reach for traditional simulation.

Satisfiability algorithms for Boolean formulae in clause form can also be used for hardware verification[5]. In this approach, the formula G above is in clause form, which is a special form of unquantified Boolean formula. An efficient method such as Davis and Putnam’s method can then be applied to test if the formula G is satisfiable. Davis and Putnam’s method was first described in the paper [6], though modern implementations differ in some ways. Most modern implementations use the method of DPLL [7], which eliminates variables by case analysis rather than ordered resolution. A recent, very efficient implementation of DPLL is described in [8]. [9] combined BDDs and satisfiability testers to solve verification problems. Another method for satisfiability testing of unquantified Boolean formulae, not necessarily in clause form, is disclosed in [1]. This method works breadth-first, trying all possible truth assignments to small subsets of the variables of a formula. From these assignments, information about dependencies between variables is obtained which can aid in determining satisfiability.

Automatic test pattern generation (ATPG) is another important problem in CAD. Given a combinational circuit, a stuck-at fault causes a wire to have a constant value. The task of ATPG is to generate input patterns that detect such stuck-at faults. It was well known that ATPG is equivalent to propositional satisfiability. Efficient SAT-based ATPG techniques have been developed[10].

Symbolic model checking [11,12,13] is concerned with verifying sequential systems. The use of BDDs for symbolic model checking was a breakthrough, because it permitted much larger systems to be verified than was possible before. BDDs permit the state of a system to be represented and manipulated efficiently, in many cases. However, the paper [14] gives some Boolean formulae obtained from symbolic model checking problems on which satisfiability algorithms such as DPLL and Stalmarck’s method are more efficient than BDDs. Other examples are given in [5] in which the smallest BDD for a Boolean function is of exponential size, regardless of the variable ordering used. There is therefore also an interest in seeing how far satisfiability-based approaches can extend in symbolic model checking applications.

Boolean satisfiability has been extensively studied. See [15] for an excellent survey of a wide range of satisfiability techniques. However some important problems in hardware verification cannot be expressed with quantifier-free Boolean formulae. Computing fixed points in symbolic model checking is one such example. Therefore there is a need for satisfiability testers for quantified Boolean formulae. There has been some work in decision procedures for quantified boolean formulae [16,17]. Our technique differs from the previous work in that it modifies the quantified Boolean formula from the inside out, rather from the outside in. That is, Qsat can choose to process a quantifier other than one of the outermost quantifiers of the formula.

The same flexibility in the processing of quantifiers is inherent in QsatCNF.

This flexibility enables QsatCNF to exploit structures in the hardware verification domain. In particular, QsatCNF is very efficient in handling long and thin circuits. Note that the propositional satisfiability problem without quantifiers is a special case of quantified Boolean formulae where all variables are assumed to be existentially or universally quantified. Since QsatCNF resembles the behaviors of BDDs, it complements the traditional DPLL style SAT solvers. An interesting future research direction is to combine the two approaches.

Many of the problems mentioned in [18] are “long and thin,” meaning that they have small cut widths. Actually, the definition of cut width differs somewhat from one paper to another, but all such definitions capture approximately the same idea. We will show below that many of the problems from [19] are also long and thin, as well as several other benchmark problems we constructed.

In fact all problems we tried from [19] have an average cut width of 19 or less. This suggests that the class of long and thin problems is fairly common in applications. It turns out that the worst-case time bound for QsatCNF on this class of long and thin problems is better than that of BDD’s and Davis and Putnam’s method by an exponential factor. We also have examples where the QsatCNF implementation is faster than BDD’s and Davis and Putnam’s method on this class of problems. This gives empirical and theoretical evidence that QsatCNF will be faster on many problems from this class.

The first author has obtained US patent 6,131,078 on Qsat.

1 Terminology

1.1 Boolean quantifiers and operators ∃ is used for existential quantification and ∀ for universal quantification. ∧ is used for logical conjunction (and), ∨ for logical disjunction (or), and ¬ for logical negation. The symbol ↔ is used for equivalence and + for exclusive or.

The constants true and false are called truth values. The Boolean operators are defined on truth values in standard ways, so that x ∧ y is true if and only if x is true and y is true, x ∨ y is true if and only if x is true or y is true, ¬x is true if and only if x is false, x ↔ y is true if and only if x and y have the same truth value, and (x + y) is true if and only if x and y have different truth values. Capital letters (like X and Y ) refer to sets or sequences of Boolean variables.

1.2 Formulae

A quantified Boolean formula is a formula built up from Boolean variables and the Boolean operators of conjunction, disjunction, negation, and other Boolean operators. Thus (x ∧ (y ∨ z)) is a quantified Boolean formula. Boolean quantifiers are also allowed to occur in quantified Boolean formulae. Thus if B is a quantified Boolean formula and X is a set of Boolean variables, then ∃X[B] and ∀X[B] are also quantified Boolean formulae, where ∃X is considered an existential quantifier and ∀X is considered a universal quantifier. ∀X[B] is often considered to abbreviate ¬∃X[¬B]. If X is the set or list {x, y, z}, then ∃X[A] abbreviates the quantified Boolean formula ∃x[∃y[∃z[A]]]. An example of a quantified Boolean formula is ∃x[x ∧ ¬∃y[y ∨ z]]. Often the term “quantified” is dropped. A quantified Boolean formula without any occurrences of quantifiers is said to be unquantified. An occurrence of a variable x in a formula A is called free if this occurrence is not within the scope of a quantifier ∃x or ∀x. Only the occurrence of z is free in the example formula. Variable occurrences that are not free are called bound. If A is a quantified Boolean formula and X is a set of variables, then A[X] denotes a formula A that contains the free variables X. A formula B having the free variables X is often taken to abbreviate ∃X[B] or ∀X[B]. A literal is a Boolean variable or its negation.

If y is a variable, it is assumed that ¬¬y is identical to y. The literal ¬y is the complement of y, and likewise y is the complement of ¬y. The literals y and ¬y are said to be complementary. A clause is a disjunction of literals, as, x ∨ ¬y ∨ z. A set of clauses, also termed a conjunctive normal form formula, is a conjunction of clauses, such as C ∧ D ∧ E, where C, D, and E are clauses.

1.3 Subformulae Each Boolean formula A is a subformula of itself. Also, if A is of the form B ⊗ C, where ⊗ is a Boolean operator, and D is a subformula of B or C, then D is also a subformula of A. Likewise, if D is a subformula of B, then D is a subformula of ¬B and a subformula of ΩX[B] where Ω is ∃ or ∀.

1.4 Simplifications For a Boolean formula A, A|y refers to A with all free occurrences of the Boolean variable y replaced by true, and the resulting formula simplified as many times as possible with respect to usual Boolean simplifications. These are the following: B ∧ true simplifies to B, B ∧ false simplifies to false, and other standard simplifications for eliminating true and false from Boolean expressions. Also, ∃x[B] and ∀x[B] simplify to B if there are no free occurrences of the variable x in B. Let A|¬y refers to A with all free occurrences of the variable y replaced by false, and the resulting formula likewise simplified.



Pages:   || 2 | 3 | 4 | 5 |   ...   | 8 |


Similar works:

«WHAT CAN ELIZABETHAN PAMPHLETS AND BALLADS TELL US ABOUT ELIZABETHAN MILITARY CULTURE? DONG-HA SEO In the early part of the sixteenth century, print culture in England was dominated by the publication of religious texts. In 1588, however, after the defeat of the Spanish Armada, England saw a proliferation of both religious and secular print. Some of the secular pamphlets were war-oriented ballads and some newsbooks. This explosion of interest in contemporary war-oriented ballads and news...»

«Relationship between Trader Types and Their Long-run Wealths in an Artificial Financial Market Akira Namatame1,Kazuya konno2, Taisei Kaizouji 3 1,2 National Defense Academy e-mail: nama@nda.ac.jp International Christian University Abstract In this paper, we study the long-run wealth distribution regarding different trading strategies in an artificial stock market. An artificial stock market is designed consisting with two broad types of agents, rational traders” and imitators. Rational...»

«Directory of Sport Science 6th Edition | International Council of Sport S. https://www.icsspe.org/bookshop/latest-publications-individual-publicati. Like 1 of 1 23/04/2014 2:35 PM 0 ICSSPE ISBN 0-99-006293-7 ~HUMAN KINETICS British Library Cataloguing in Publication Data A catalogue record for this book is available from the British Library Directory of Sport Science, 6th Edition All rights reserved. Except for use in a review, no part of this publication may be reproduced, stored in a...»

«TREDEGAR & DISTRICT CANINE SOCIETY Chairman: Mr. Clive Evans Vice Chairman: Mr. Trevor Jones Treasurer: Mrs. Lilian Evans Committee: Mrs. Cynthia. Crossley, Mr. Jon Crossley, Mrs. Linda David, Mrs. Jane Humphries, Mrs. Janet Saunders SCHEDULE OF UNBENCHED 73 CLASS MEMBERS LIMITED SHOW (Held under Kennel Club Rules & Show Regulation) Not judged on the Group System At TREDEGAR LEISURE CENTRE, STABLE LANE TREDEGAR, GWENT, NP22 4BH On SATURDAY 2nd APRIL 2016 Show Opens 9.30 a.m. Judging in both...»

«Colonel Frank CFS NEWS Seely School Issue : 34 June A Specialist College for Excellence in Mathematics & Computing 2011 ECO GREEN FLAG AWARD! CALVERTON SCHOOL GETS IT’S SECOND TOP ECO-SCHOOL AWARD Colonel Frank Seely School in Calverton received its second top environmental award – which is uncommon for secondary schools, especially in this region. The school was assessed on 1st July and has now been awarded the top Eco-Schools Green Flag Award for the second time in three years by the...»

«Introduction This annual report presents the activities and results of various agencies in managing drinking water in Saskatchewan for the fiscal year ending March 31, 2012. It reports to the public and elected officials on public commitments made and other key accomplishments of ministries and agencies engaged in drinking water management in Saskatchewan. Although a renewed vision and set of goals were introduced as a result of the 2011 provincial election, the 2011-12 Annual Report on the...»

«United States Court of Appeals for the Federal Circuit 01-1201 SPECIAL DEVICES, INC., Plaintiff-Appellee, v. OEA, INC., Defendant-Appellant. Robert M. Taylor, Jr., Lyon & Lyon LLP, of Irvine, California, argued for plaintiff-appellee. On the brief were Robert C. Weiss and Thomas J. Brindisi, of Los Angeles, California. Edward F. O’Connor, Stradling, Yocca, Carlson & Rauth, of Newport Beach, California, argued for defendant-appellant. Appealed from: United States District Court for the Central...»

«The MESSENGER A Quarterly Newsletter for the Faithful of Saint George Orthodox Christian Church in Houston, Texas Summer 2009 Volume XII, Issue II What's With All The Repetition, “Again and Again Let us pray to the Lord”? There's a joke that goes, Question: “How do you know that you are in an Orthodox Church?” Answer: “You are still worshipping 45 minutes after you've already heard 'Let us depart in peace!'” There's another one, Question: “How many times should you make the sign...»

«THIS DOCUMENT IS IMPORTANT AND REQUIRES YOUR IMMEDIATE ATTENTION. If you are in any doubt as to the action you should take, you are recommended to seek your own financial advice from your stockbroker, bank manager, solicitor, accountant or other independent financial adviser duly authorised under the Financial Services and Markets Act 2000, as amended, (“FSMA”) who specialises in advising on the acquisition of shares and other securities. This document, which has been drawn up in accordance...»

«Compliance A Guide for Grandfathered Persons www.iii.ie Am I compliant? The Central Bank of Ireland’s Minimum Competency Code (MCC, 2011) enhances the minimum professional standards for all persons who provide consumers with financial advice on products or undertake certain specified functions. These standards are essential for the protection of consumers who place their trust in those working in the industry. Therefore, those who work in an accredited role or are engaged in a specified...»

«2012 Mid-Continent transportation researCh ForuM September 6-7, 2012 Madison, Wisconsin Madison Concourse Hotel & Governor's Club 2012 Mid-continent transportation research ForuM F e at u r e d S p e a k e r S tereSa adamS Teresa Adams is a Professor of Transportation Engineering and City Planning in the Department of Civil and Environmental Engineering at the University of Wisconsin–Madison, and is Director and Principal Investigator of the National Center for Freight and Infrastructure...»

«The Impact of Lord Burghley and the Earl of Leicester’s Spanish-Speaking Secretariats Hannah Leah Crummé University College London | King's College London ABSTRACT Whilst the literature of the Spanish Golden Age is itself filled with problems of representation, I will argue in this paper that the greatest misrepresentation of all did not occur in fiction but rather in the English court. During Elizabeth’s reign Lord Burghley, working with his secretary Sir Francis Walsingham,...»





 
<<  HOME   |    CONTACTS
2017 www.thesis.dislib.info - Online materials, documents

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.