WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:   || 2 | 3 |

«Abstract. Execution of most of the modern DPLL-based SAT solvers is guided by a number of heuristics. Decisions made during the search pro- cess are ...»

-- [ Page 1 ] --

Instance-Based Selection of Policies for SAT

Solvers

Mladen Nikoli´, Filip Mari´, Predrag Janiˇi´

c c cc

Faculty of Mathematics, University of Belgrade,

Belgrade, Studentski Trg 16, Serbia

{nikolic, filip, janicic}@matf.bg.ac.rs

Abstract. Execution of most of the modern DPLL-based SAT solvers is

guided by a number of heuristics. Decisions made during the search pro-

cess are usually driven by some fixed heuristic policies. Despite the out-

standing progress in SAT solving in recent years, there is still an appeal- ing lack of techniques for selecting policies appropriate for solving specific input formulae. In this paper we present a methodology for instance- based selection of solver’s policies that uses a data-mining classification technique. The methodology also relies on analysis of relationships be- tween formulae, their families, and their suitable solving strategies. The evaluation results are very good, demonstrate practical usability of the methodology, and encourage further efforts in this direction.

1 Introduction The propositional satisfiability problem (SAT) is one of the fundamental prob- lems in computer science. It is the problem of deciding if there is a truth assign- ment under which a given propositional formula (in conjunctive normal form) evaluates to true. SAT was the first problem proved to be NP-complete [Coo71] and it still has a central position in the field of computational complexity. SAT problem is also very important in many practical domains such as electronic de- sign automation, software and hardware verification, artificial intelligence, and operations research. Thanks to recent advances in propositional solving technol- ogy, SAT solvers (procedures that solve the SAT problem) are becoming a tool for attacking more and more practical problems.

A number of SAT solvers have been developed. The majority of state-of-the- art complete SAT solvers are based on the branch and backtrack algorithm called Davis-Putnam-Logemann-Loveland or the DPLL algorithm [DP60,DLL62]. Spec- tacular improvements in the performance of DPLL-based SAT solvers achieved in the last few years are due to (i) several conceptual enhancements on the orig- inal DPLL procedure, aimed at reducing the amount of explored search space (e.g., backjumping, conflict-driven lemma learning, restarts), (ii) better imple- mentation techniques (e.g., two-watched literals scheme for unit propagation), and (iii) smart heuristic components (which we focus on in this work). These This work was partially supported by Serbian Ministry of Science grant 144030.

advances make possible to decide the satisfiability of industrial SAT problems with tens of thousands of variables andmillions of clauses.

Complex policies, heuristics that guide the search process, represent important parts of modern SAT solvers and are crucial for solver’s efficiency. These include policies for literal selection, for determining the clause database size, for choosing restart points, etc. Specific policies are usually parametrized by a number of numerical and categorial parameters. Single policy with different parameter values can be treated as different policies. SAT solving process is completely determined only when all its heuristic policies are set. Selected combinations of policies specify the solving strategy (or simply strategy).

Typically, every SAT solver uses a predetermined, hard-coded strategy and applies it on all its input formulae. However, in recent times, SAT solvers tend to implement multiple policies and the question arises as to how to choose a strategy that would give good performance for a specific SAT instance. Addressing this question is of crucial importance because the solving time for the same input formula can vary for several orders of magnitude depending on the solving strategy used. The problem of adapting a SAT solver to the input formula has been addressed for the first time only recently. Our approach significantly differs from the only existing related approach we are aware of (as discussed in Sect. 5).

Propositional formulae can be clustered in families of formulae by their origin — hardware verification problems (e.g., FPGA routing), manually crafted problems (e.g., graph coloring, Hanoi towers), or random generated problems (e.g., k-SAT). It is interesting to explore the behaviour of different policies and solving strategies on families of formulae. The important question is whether one strategy shows the same or similar behaviour on similar formulae. If this is the case, and if one can automatically guess a family to which a given formula belongs, then this could be used for selecting an appropriate strategy for this particular formula. To implement this approach, one needs (i) a technique for classifying formulae based only on their syntax; (ii) information about behaviour of different policies on various families of formulae.

The main message of this work is that intelligent selecting of solving policies, based on the syntax of the input formula, can significantly improve efficiency of a SAT solver. The proposed methodology will not lead to optimal performance on each input formula, but the solving performance will be significantly improved in average on multiple input formulae. Here, by improving efficiency of a SAT solver we mean increasing the number of formulae solvable within some time limit and decreasing the solving time.





The proposed methodology relies on several hypotheses that will be investigated in the rest of the paper:

(H1) Formulae of the same family (i.e., of similar origin) share some syntactical properties that can be used for automated formula classification;

(H2) For each family of formulae there is only a small number of solving strategies that are appropriate — that show better performance on formulae belonging to that family then all other available strategies.

(H3) For formulae that are syntactically similar, the best strategies are also (in some sense) similar.

If the above hypotheses hold, then our methodology will be practically applicable. Namely, if the formula is correctly classified then it will be solved by a solving strategy suitable for a family that the formula belongs to. However, even if the formula is misclassified, it will be solved using a strategy similar to the optimal one.

The rest of the paper is organized as follows: in Sect. 2, a brief background information on SAT problem, SAT solvers, and their heuristic components is given. In Sect. 3, the proposed methodology is described. The experimental results are given in Sect. 4. In Sect. 5 related work is discussed. In Sect. 6 final conclusions are drawn and some directions of possible further work are discussed.

2 Background Most of today’s state-of-the-art solvers are complex variations of the DPLL procedure. In the rest of the paper, we shall assume that the reader is familiar with the modern SAT solving techniques. More on these topics can be found, for example, in [NOT06,KG07,Mar08,GKSS07]. Although modern SAT solvers share common underlying algorithms and implementation techniques, their operation is guided by a number of heuristic policies that have to be selected in order to obtain deterministic solving strategies. The most important heuristic policies determine: (i) which literals to choose for branching, (ii) when to apply restarting, and (iii) when to forget some clauses that are learnt during the solving process.

In the rest of this section, policies that were used in our experiments will be described.

Literal selection policies. During the DPLL backtrack-search, literals used for branching should be somehow selected. This is the role of literal selection policies.

Most literal selection policies separately select a variable v (by using a variable selection policy) and only then choose its polarity, i.e., choose if it should be negated or not (by using a polarity selection policy).

Some variable selection policies are the following1 :

VSrandom — This policy randomly chooses a variable among all variables of the initial formula that are not defined in the current valuation, i.e., assertion trail.

VSb,d,init — The goal of this policy (introduced in the solver MiniSAT [ES04]) minisat is to select a variable that was active in recent conflicts. In order to implement this, an activity score is assigned to each variable. On every conflict, the scores of the variables that occur in the conflict clause are bumped, i.e., increased by a bump factor given by the parameter b. Also, during the conict analysis process, on each resolution step all variables that occur in the 1 The policy names will be printed in subscripts and their parameters in superscripts.

explanation clause are bumped. To stimulate recent conflicts, on each conict all the scores are decayed, i.e., decreased by a decay factor given by the parameter d.

An important aspect of the MiniSAT variable selection policy is how to assign initial scores to variables. If the parameter init has the value zero, scores of all variables are set to zero, hence all variables have the same chance to be selected. If the parameter init has the value freq, the initial score of each variable is set to its number of occurrences in the initial formula F0.

VSp random ◦ VSx — This compound policy chooses a random variable with probability p and with probability 1 − p uses a given policy here denoted by VSx.

Some polarity selection policies are the following:

PSpositive — Always selects a non-negated literal.

PSnegative — Always selects a negated literal.

PSp random — A random selection which chooses a non-negated literal with probability p.

PSinit polarity caching — When using this policy (introduced in the solver RSAT [PD07] as phase caching), a preferred polarity is assigned to each variable and it is used for polarity selection. Whenever a literal is asserted to the current assertion trail (either as a decision or as a propagated literal), its polarity defines the future preferred polarity of its variable. When a literal is removed from the trail (during backjumping or restarting) its preferred polarity is not changed. If the parameter init has the value pos, then initial polarities of all variables are positive, it has the value neg then they are set to negative, and if it has the value freq, then preferred polarity of each variable is set to the polarity which is more frequent of the two in the initial formula.

Restart policies. Restart policies determine when to apply restarting. Most restart policies are based on conflict counting. On each conflict, the counter is increased. Restarting is applied whenever the counter reaches a certain threshold value. When this happens, the counter is reset and a new threshold is selected according to some specific policy. The sequence of threshold values must contain an increasing subsequence in order to ensure termination and completeness of

the procedure. Some possible restart policies are the following:

Rno restart — Restarting is not applied.

Rc0,q minisat — The initial threshold value is set to c0 and the threshold values form a geometric sequence with a quotient q [ES04].

Rk

luby — Threshold values are positive integer multiples of the Luby series [LSZ93]:

–  –  –

Forget policies. Forget policies determine (i) when to remove some clauses learnt during the solving process and (ii) which clauses to forget. In the rest of the paper, only the following policy will be used.

Fc0,q,p — When using this policy (introduced by the solver MiniSAT [ES04]), minisat forgetting is done when the current number of clauses in the clause database reaches a threshold value. Threshold values form a geometric sequence whose initial value is c0 percent of the number of clauses in the initial formula and whose coefficient is q. It is interesting that the threshold value is not updated after the forgetting itself, but instead it is updated on each restart.

Another important aspect of a forget policy is what clauses to forget. The MiniSAT policy forgets p percent of learnt clauses that are allowed to be forgotten. Clauses are assigned activity scores which reflect their participation in conflicts, very similar to variable activity scores used in the MiniSAT variable selection policy. Clauses with the smallest activity scores are the ones that are being forgotten.

3 Methodology

Our methodology, when applied to a given SAT solver, selects an appropriate solving strategy (i.e., combination of policies) for each input formula. The proposed methodology can be applied to any DPLL-based SAT solver, provided it supports multiple policies. In our experiments, the ArgoSAT solver2 was used since it implements a large number of policies and since its modular architecture allows easy modification of existing and implementation of new policies [Mar09].

The overall methodology consists of two phases.

Training phase. This phase consists of systematic solving of all formulae from a representative corpus, by using all candidate solving strategies. This allows selecting the best solving strategy (the one that solves the most formulae) for each family of formulae from the corpus. Profiles of all formulae from the corpus (i.e., their representation suitable for classification) are also computed in this phase.

Exploitation phase. In this phase, the family of a given formula is guessed and the strategy that showed the best results on that family during the training phase is used for its solving. After the training, the system implementing the 2 http://argo.matf.bg.ac.yu/software/ methodology can be applied both to the formulae from the training corpus and to some other formulae.

Several issues still need to be addressed, as discussed below.

The choice of candidate solving strategies. In our case candidate strategies are defined as all (60 = 3 · 5 · 4 · 1) possible combinations of the given policies. They are listed in the Table 1.

–  –  –

where P and P are instance profiles.

4 Experiments and Evaluation Experiments described in this section test the hypotheses that our approach relies on (given in Sect. 1), and also demonstrate a good overall quality of our methodology.



Pages:   || 2 | 3 |


Similar works:

«Automatic Extraction of Generic House Roofs from High Resolution Aerial Imagery ? Frank Bignone, Olof Henricsson, Pascal Fua+ and Markus Stricker Communications Technology Laboratory Swiss Federal Institute of Technology ETH CH-8092 Zurich, Switzerland + SRI International, Menlo Park, CA 94025, USA Abstract. We present a technique to extract complex suburban roofs from sets of aerial images. Because we combine 2-D edge information, photometric and chromatic attributes and 3-D information, we...»

«NEVADA LEGISLATURE NEVADA SILVER HAIRED LEGISLATIVE FORUM (Nevada Revised Statutes 427A.320 through 427A.400) SUMMARY MINUTES AND ACTION REPORT The sixth meeting of the Nevada Silver Haired Legislative Forum (NSHLF) for the 2007-2008 interim period was held on Tuesday, May 13, 2008, at 10 a.m. in Room 4401 of the Grant Sawyer State Office Building, 555 East Washington Avenue, Las Vegas, Nevada. The meeting was also videoconferenced to Room 3138 of the Legislative Building, 401 South Carson...»

«December 2014 Glistening particles of industrial silver A report prepared for The Silver Institute CRU International Limited’s responsibility is solely to its direct client (The Silver Institute). Its liability is limited to the amount of the fees actually paid for the professional services involved in preparing this report. We accept no liability to third parties, howsoever arising. Although reasonable care and diligence has been used in the preparation of this report, we do not guarantee...»

«Journal of Artificial Intelligence Research 42 (2011) 851-886 Submitted 07/11; published 12/11 Dr.Fill: Crosswords and an Implemented Solver for Singly Weighted CSPs Matthew L. Ginsberg On Time Systems, Inc. 355 Goodpasture Island Road, Suite 200 Eugene, Oregon 97401 Abstract We describe Dr.Fill, a program that solves American-style crossword puzzles. From a technical perspective, Dr.Fill works by converting crosswords to weighted csps, and then using a variety of novel techniques to find a...»

«Tight-fitting Clothes in Antiquity and the Renaissance1 Dagmar Drinkler Abstract: A great number of ancient works of art depict figures who wear tight-fitting and strikingly patterned garments, particularly hose. These elastic textiles that cling to the body cannot be reproduced by any of the weaving techniques known to us. And there is no evidence that the textile technique of knitting was already known in antiquity. So the garments must have been made in a different technique. By reproducing...»

«THE BEST SOFTWARE WRITING I Selected and Introduced by Joel Spolsky The Best Software Writing I: Selected and Introduced by Joel Spolsky Copyright © 2005 Edited by Joel Spolsky All rights reserved. No part of this work may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopying, recording, or by any information storage or retrieval system, without the prior written permission of the copyright owner and the publisher. ISBN (pbk): 1-59059-500-9...»

«Packing Tips Good packing is essential for a good move. If you choose to do some or all of your own packing in preparation for your relocation, it's especially important that you be familiar with the techniques and boxes that will best protect your possessions. Ready, Set, Pack! Good Packing Means. Limiting cartons, when possible, to a maximum weight of 50 pounds to make handling easier. Wrapping items carefully. Providing plenty of cushioning to absorb shock. Using sturdy cartons that close....»

«UMTRI-2001-3 FIELD MEASUREMENTS OF DIRECT A N D REARVIEW-MIRROR GLARE FROM LOW-BEAM HEADLAMPS Michael Sivak Michael J. Flannagan Brandon Schoettle Yoshihiro Nakata January 2001 FIELD MEASUREMENTS OF DIRECT AND REARVIEW-MIRROR GLARE FROM LOW-BEAM HEADLAMPS Michael Sivak Michael J. Flannagan Brandon Schoettle Yoshihiro Nakata The University of Michigan Transportation Research Institute Ann Arbor, Michigan 48109-2150 U.S.A. Report No. UMTRI-2001-3 January 2001 Technical Report Documentation Page...»

«Robert L. Jackson Associate Professor Department of Mechanical Engineering Auburn University Professional Preparation Ph.D. Mechanical Engineering, Georgia Institute of Technology, Thesis Title: The Wear and Thermo-elastohydrodynamic Behavior of Thrust Washer Bearings Under Non-Axisymmetric Loads Major: Friction, Lubrication and Wear Minor: Dynamics and Vibrations Advisor: Itzhak Green M.S. Mechanical Engineering, Georgia Institute of Technology B.S. Mechanical Engineering, Georgia Institute of...»

«Old Norse Myths, Literature and Society Proceedings of the 11th International Saga Conference 2-7 July 2000, University of Sydney Edited by Geraldine Barnes and Margaret Clunies Ross Centre for Medieval Studies, University of Sydney Sydney, Australia July 2000 © 2000, Contributors All rights reserved. No part of this publication may be reproduced, stored in a retrieval system, or transmitted, in any form or by any means, electronic, mechanical, photocopying, recording, or otherwise, without...»

«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...»

«EXPERIMENTAL AND THEORETICAL ASSESSMENT OF THIN GLASS PANELS AS INTERPOSERS FOR MICROELECTRONIC PACKAGES A Thesis Presented to The Academic Faculty by Scott R. McCann In Partial Fulfillment of the Requirements for the Degree Master's of Science in the School of Mechanical Engineering Georgia Institute of Technology May 2014 COPYRIGHT 2014 BY SCOTT MCCANN EXPERIMENTAL AND THEORETICAL ASSESSMENT OF THIN GLASS PANELS AS INTERPOSERS FOR MICROELECTRONIC PACKAGES Approved by: Dr. Suresh K. Sitaraman,...»





 
<<  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.