FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:   || 2 | 3 | 4 |

«Abstract. State-of-the-art solvers for Quantified Boolean Formulas (QBF) have employed many techniques from the field of Boolean Satisfiability ...»

-- [ Page 1 ] --

Beyond CNF: A Circuit-Based QBF Solver

Alexandra Goultiaeva, Vicki Iverson, and Fahiem Bacchus

Department of Computer Science

University of Toronto


Abstract. State-of-the-art solvers for Quantified Boolean Formulas (QBF) have

employed many techniques from the field of Boolean Satisfiability (SAT) includ-

ing the use of Conjunctive Normal Form (CNF) in representing the QBF formula.

Although CNF has worked well for SAT solvers, recent work has pointed out some inherent problems with using CNF in QBF solvers.

In this paper, we describe a QBF solver, called CirQit (Cir-Q-it) that utilizes a circuit representation rather than CNF. The solver can exploit its circuit repre- sentation to avoid many of the problems of CNF. For example, we show how this approach generalizes some previously proposed techniques for overcoming the disadvantages of CNF for QBF solvers. We also show how important techniques like clause and cube learning can be made to work with a circuit representation.

Finally, we empirically compare the resulting solver against other state-of-the-art QBF solvers, demonstrating that our approach can often outperform these solvers.

1 Introduction QBF is a powerful generalization of SAT in which the variables can be universally or existentially quantified. While any problem in NP can be encoded in SAT, QBF allows us to encode any problem in PSPACE. This opens a much wider range of poten- tial application areas for a QBF solver, including problems from areas like automated planning (particularly conformant and conditional planning), non-monotonic reasoning, electronic design automation, scheduling, model checking and verification, strategic de- cision making, and multi-agent scenarios, see for, e.g., [1,2,3].

State-of-the-art QBF solvers have utilized a number of techniques inherited from SAT solving technology. This has included the use of DPLL search augmented with clause learning along with additional QBF-specific techniques like solution backtrack- ing and cube learning. Besides DPLL the original Davis-Putnam SAT solving technique [4] of ordered resolution has also been utilized [5], as well as methods involving the use of Skolemization to convert the QBF formula to SAT [6]. One constant in almost all of this work, however, has been the utilization of conjunctive normal form (CNF) in representing the QBF formula.

It has long been noted that conversion to CNF can lead to losing structure that could potentially be exploited computationally. As a result there has been some work on non- CNF SAT solvers, e.g., [7,8]. This work has shown that non-clausal representations can be effective for solving SAT. Nevertheless, the allure of CNF is that it can lead to very high performance implementations since it is a very simple and uniform representation.

–  –  –

Hence, the extra structure that can be exploited in a non-clausal representation has not been able to significantly outweigh the practical advantages of CNF in SAT solvers, and most SAT solvers continue to utilize CNF.

In QBF however the situation is different. In particular, for a similarly sized problem the search space explored by a QBF solver tends to be much larger than that explored by a SAT solver. Hence, there is much more potential for savings from exploiting the extra structure contained in non-clausal representations. In fact, there have been a number of papers that have identified various inadequacies of the CNF representation for QBF and proposed alternate representations aimed at addressing these problems, e.g., [9,10].

One of the most general and structure laden non-clausal representations is a circuit representation. Circuit representations have been used before in SAT solvers, e.g., [7,8], and in this paper we explore the use of this representation in a QBF solver.

One advantage of circuits is that they are more compatible with real problems— typically CNFs are generated from more structured representations like circuits. We also investigate ways of exploiting within our solver some of the extra structural information contained in the circuit. One particular example is the exploitation of don’t care reasoning. We explain why don’t care reasoning has more potential for efficiency gains when solving a QBF than when solving SAT. We also demonstrate how the essential techniques of unit propagation, clause learning, and cube learning used in CNF solvers can be adapted to a circuit representation. Finally, we explain how a circuit representation generalizes some of the key previously proposed techniques for addressing the inadequacies of CNF in the context of QBF.

We have implemented a solver we call CirQit (pronounced Cir-Q-it) that is based on our approach of utilizing a circuit representation. We are able to show empirically that it is very competitive with current state-of-the-art QBF solvers, and that on some problem suites it exhibits superior performance.

In the rest of the paper we first provide some essential background on QBF and the circuit representation of a QBF. We present some of the details of our circuit-based solver. Our solver utilizes a DPLL search procedure running on a circuit representation rather than on a CNF representation. We describe how propagation can be performed, and how clause and cube learning can be implemented. We discuss related work on QBF solvers based on non-clausal representations. Finally, we present various experimental results demonstrating the merit of our approach, and close with some conclusions.

2 Background

2.1 QBF A QBF has the form Q.φ, where φ is an arbitrary propositional formula and Q is a sequence of quantified variables (∀x or ∃x). We require that the set of variables in φ be contained in Q so that Q.φ has no free variables, and that φ contain only the connectives AND (∧), OR (∨), and NOT (¬).

A quantifier block qb of Q is a maximal contiguous subsequence of Q where every variable in qb has the same quantifier type. The quantifier blocks are ordered by their appearance in Q: qb 1 ≤ qb2 iff qb 1 is equal to or appears before qb 2 in Q. Each variable 414 A. Goultiaeva, V. Iverson, and F. Bacchus x in φ appears in some quantifier block qb(x). For two variables x and y we say that y is downstream of x (x is upstream of y) if qb(y) qb(x) (qb(x) qb(y)). We also say that x is universal (existential) if its quantifier in Q is ∀ (∃).

A QBF instance can be reduced by a literal (i.e., an assignment to one of its variables). The reduction of a formula Q.φ by is denoted by Q.φ|. The reduction is the new formula Q.φ where φ is φ with v replaced by the constant TRUE (if = v) or FALSE (if = ¬v), and optionally simplified according to standard logical rules: e.g., for any formula ψ, FALSE ∧ ψ is equivalent to FALSE and ∀x.ψ is equivalent to ψ if the variable x does not appear in ψ. A specific example is ∀xz.∃y.(¬y ∨ (x ∧ z)) ∧ ¬(x ∨ z)|¬x which is equal to ∀xz.∃y.(¬y ∨ (FALSE ∧ z)) ∧ ¬(FALSE ∨ z) which simplifies to ∀z.∃y.¬y ∧ ¬z.

Semantically, the truth or falsity of a QBF formula (with no free variables) can be dened recursively: (1) ∀xQ.φ is true iff both Q.φ|x and Q.φ|¬x are true, and (2) ∃xQ.φ is true iff at least one of Q.φ|x or Q.φ|¬x is true. By instantiating the quantified variables one by one, following the quantifier ordering, and substituting true or false into φ we arrive at either a QBF where φ simplifies to FALSE (which is a false QBF) or a QBF where φ simplifies to TRUE (which is a true QBF).

A circuit is a directed acyclic graph with a single sink where the nodes are logical gates and the edges are signal lines connecting the gates. Each gate is either an AND, OR, or NOT gate, has a single outgoing output line, and one or more incoming input lines. The output line of the sink gate is the circuit output, and the lines that are not outputs of any gate are the circuit inputs. A circuit representation Q.C for the QBF formula Q.φ is a circuit C where the variables in Q are in 1-1 correspondence with the circuit inputs. C can be constructed recursively as follows. If φ is a variable x, then C has only one line labeled by the variable x and no gates. If φ = ¬ψ, then C consists of the circuit representing ψ with the output of this circuit connected to the input of a NOT gate. If φ = ψ1 ∧ · · · ∧ ψi (ψ1 ∨ · · · ∨ ψi ), then C consists of the outputs of the circuits representing ψ1 to ψi connected as inputs of an AND (OR) gate. One key feature of the circuit representation is that duplicated sub-formulas in φ can be represented by a single subcircuit—the output line of that subcircuit can be used as an input in all places the sub-formula appears.

The lines of a circuit can take on the values TRUE or FALSE, and these values can be propagated to other lines of the circuit using standard rules of Boolean logic.

For example, if an input line of an AND gate has value FALSE then FALSE can be propagated to the output line of the gate. A circuit Q.C represents a formula Q.φ when for any setting of the variables in φ, φ will simplify to TRUE (FALSE) if and only if TRUE (FALSE) is propagated to the output of C given the same setting for its corresponding input lines. The construction described above yields a circuit C that represents φ.

Hence, we can evaluate a QBF formula Q.φ by constructing a circuit Q.C representing it, and then evaluating the previously given definition of truth for a QBF formula by propagating values in C. That is, we can detect when φ simplifies to TRUE or FALSE by detecting when TRUE or FALSE is propagated to the output line of C.

Beyond CNF: A Circuit-Based QBF Solver 415 3 A Circuit-Based Solver Similar to previous circuit based SAT solvers, e.g., [7,8], our solver utilizes DPLL search to determine the truth or falsity of the QBF Q.φ. Specifically, φ is represented as a circuit C with the variables in Q being the inputs to C. During DPLL search, these variables are branched on in an order respecting the quantifier ordering (i.e., if x is upstream of y then the search must branch on x before y). Each branch sets a variable of φ and hence a corresponding input line of C. The input line values are propagated through C, and the search verifies that at least one side each existential branch and both sides of each universal branch lead to a true circuit output (i.e., satisfies φ).

However, to make this process more efficient, e.g., to detect when certain input lines must take on a particular value for the circuit output to be TRUE, the solver initially sets the circuit output line to TRUE and propagates values backwards in the circuit as well as forwards. Backwards propagation, like forward propagation, follows the rules of Boolean logic, e.g., if an OR gate’s output line is set to FALSE then FALSE can be propagated to all of its input lines. With backward propagation from a TRUE output we can detect when φ is falsified (i.e., when a setting of the input lines would lead to FALSE being propagated to the output line) by the occurrence of a conflict where both TRUE and FALSE is propagated to some line in the circuit. Such conflicts also allow us to employ 1UIP clause learning techniques on the circuit representation.

One negative aspect of fixing the circuit output line to TRUE, however, is that we can no longer use the propagation of TRUE to the circuit output to detect when the formula φ has become satisfied by the current setting of its variables—the output line always has that value. We discuss below how this problem is resolved in our solver by utilizing information gathered during don’t care propagation.

3.1 Propagation Our implementation of forward and backward propagation in the circuit is based on a previous circuit based SAT solver described in [7]. In that paper Thiffault et al. showed that this kind of propagation in the circuit corresponds in a precise way to Unit Propagation (UP) on an equivalent CNF encoding of the formula. In particular, if the circuit was converted to CNF using the standard Tseitin encoding [11], then corresponding to each circuit line l there would be a new variable v in the CNF encoding such that a value would be propagated to the line l in the circuit if and only if UP in the CNF forces v to take the same value. Besides this basic mechanism, however, our QBF solver differs from previous circuit based SAT solvers in a number of ways.

Representing internal lines. The CNF encoding of a formula introduces additional variables that correspond to the sub-formulas of the formula. These additional variables are very useful in a SAT solver as they can be branched on in a DPLL search (implicitly positing a truth value for an entire sub-formula), and they can be included in learnt clauses increasing the effectiveness of clause learning.

A key feature of our circuit based QBF solver is that it also utilizes the learning techniques common in DPLL based QBF solvers that employ CNF [12] i.e., clause and cube learning. Hence, to facilitate the power of the learnt clauses we introduce additional variables to label the internal lines of the circuit, as is done in circuit based SAT solvers. (The 416 A. Goultiaeva, V. Iverson, and F. Bacchus input lines are all labeled with a variable of the original formula Q.φ). Formally, all of these new variables are existential, and we place them as early in the quantifier ordering as possible. Specifically, each internal line l in the circuit is the output line of a sub-circuit c that has some set of input lines representing a set of variables V of φ. We place the new variable representing l in the quantifier prefix immediately after the last variable of V in the prefix. By placing these new variables as early as possible in the quantifier prefix we enable more effective universal reduction during clause learning and propagation.

Note however that in QBF, unlike SAT, these new variables are never branched on during the DPLL search. The DPLL search must respect the quantification order when selecting variables to branch on, so by the time it can select a variable v representing the output of sub-circuit c all of the inputs to c must have already been assigned, and hence v would already be assigned by propagation.

Pages:   || 2 | 3 | 4 |

Similar works:

«IOSR Journal of Mechanical and Civil Engineering (IOSR-JMCE) e-ISSN: 2278-1684,p-ISSN: 2320-334X, Volume 12, Issue 2 Ver. VI (Mar Apr. 2015), PP 34-41 www.iosrjournals.org Ductility of Outrigger Typologies for Highrise Structures MSc. Rafael Shehu Post graduated student, School Fratelli Pesenti, Polytechnic University of Milan, Italy Abstract: This research paper focuses on aspects of the building performance designed or retrofited by means of conventional or virtual Outriggers. The purpose of...»

«University of Miami Scholarly Repository Open Access Dissertations Electronic Theses and Dissertations 2008-04-27 Solo Techniques for Unaccompanied Pizzicato Jazz Double Bass Larry James Ousley University of Miami, ousley@bellsouth.net Follow this and additional works at: http://scholarlyrepository.miami.edu/oa_dissertations Recommended Citation Ousley, Larry James, Solo Techniques for Unaccompanied Pizzicato Jazz Double Bass (2008). Open Access Dissertations. Paper 96. This Open access is...»

«Pour citer cet article : LE BRETON, D. « Concepts et significations majeures des conduites à risque », Journal des socio-anthropologues de l'adolescence et de la jeunesse, Revue en-ligne. Date de publication : janvier 2012. [http://anthropoado.com/le-journal-des-socio-anthropologues-de-l-adolescence-et-de-lajeunesse-textes-en-ligne/] Concepts et significations majeures des conduites à risque Par David Le Breton Significations des conduites à risque Paradoxalement les conduites à risque...»

«How to Reverse Your Cataracts Naturally. 5 Ways to Do It How to Reverse Your Cataracts Naturally: 5 Ways to Do It William Bodri The Skeptical Nutritionist Naturopathic Educator 1 How to Reverse Your Cataracts Naturally. 5 Ways to Do It Copyright Copyright © 2003, William Bodri All rights reserved in all media First edition 2003. Top Shape Publishing, LLC 1135 Terminal Way Suite 209 Reno, Nevada 89502 No part of this book may be reproduced, stored in a retrieval system, or transmitted by any...»

«How-To Guide CUSTOMER Document Version: 1.5 – 2015-12-28 How to Scramble Data Using SAP Test Data Migration Server Release 4.0 Typographic Conventions Type Style Description Example Words or characters quoted from the screen. These include field names, screen titles, pushbuttons labels, menu names, menu paths, and menu options. Textual cross-references to other documents. Example Emphasized words or expressions. Technical names of system objects. These include report names, program names,...»

«SELECTION OF SEGMENTAL LINING SYSTEM AND REPAIR CLASSIFICATION Jodl Hans Georg*, Kolić Davorin** * O.Univ.Prof. Dipl.-Ing. Dr.techn. Hans Georg Jodl Institute for Construction Process and Construction Management University of Technology Vienna, Karlsplatz 13/234, A-1041 Wien, Austria E-mail: jodl@ibb.tuwien.ac.at ** Davorin Kolić M.Sc. PE Neuron Consult ZT, Pelikanstraße 18, A-4061 Pasching, Austria E-mail: office@neuron.at Key words: Segmental lining, durability requirements, repair...»

«Web Site: www.parallax.com Office: (916) 624-8333 Forums: forums.parallax.com Fax: (916) 624-8003 Sales: sales@parallax.com Sales: (888) 512-1024 Technical: support@parallax.com Tech Support: (888) 997-8267 Hackable Electronic Badge Guest (blue, #20000); Staff (white, #20100); Speaker (black, #20200) Energize your events by using the Badges to store and distribute schedules, identify participants, share contact info, and play interactive games. In educational environments, Badges encourage...»

«About the Authors Christina Amcoff Nyström is presently an Assistant Professor in Informatics at Mid Sweden University, Sweden. She is sharing her professional interests between tutoring master courses and researching technical communication, including communication in organizations and virtual collaboration among project members. Hans Andersin was born in 1930. In 1954-1955 he took part in building the first electronic computer in Finland. In 1956 he joined IBM and worked in various sales,...»

«Bibliotheca Hagiotheca ∙ Series Colloquia II Saintly Bishops and Bishops’ Saints: Proceedings of the 3rd Hagiography Conference organized by Croatian Hagiography Society 'Hagiotheca' and International Hagiography Society, Poreč, 27-30 May 2010 Edited by John S. Ott and Trpimir Vedriš Copy-editing: Marina Miladinov Bibliotheca Hagiotheca ∙ Series Colloquia, vol. 2. Series editors: Ana Marinković and Trpimir Vedriš First published 2012 Croatian Hagiography Society 'Hagiotheca',...»

«Solar Glare Hazard Analysis Tool (SGHAT) Technical Reference Manual Clifford K. Ho, Cianan A. Sims, Julius Yellowhair, and Evan Bush Sandia National Laboratories (505) 844-2384, ckho@sandia.gov SAND2014-18360 O September 2014 Contents 1. Requirements 2. Introduction 3. Assumptions and Limitations 4. Determination of Glare Occurrence 4.1 Sun Position 4.2 Reflected Sun Vector 4.3 Scattering and Subtended Beam Angle 4.4 Beam Projection onto PV Array Plane 4.5 PV Single-Axis Tracking 4.6 PV...»


«Istation's Indicators of Progress (ISIP) Advanced Reading Technical Report Version 4 Computer Adaptive Testing System for Continuous Progress Monitoring of Reading Growth for Students Grade 4 through Grade 8 Patricia Mathes, Ph.D. 2000 Campbell Centre II 8150 North Central Expressway Dallas, Texas 75206 866.883.7323 www.istation.com Copyright ©2016 Istation. All rights reserved. Istation's Indicators of Progress (ISIP) Advanced Reading Technical Manual (2016) by Patricia Mathes, Ph.D....»

<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

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.