21
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: not found

      Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers

      chapter-article

      Read this article at

      ScienceOpenPublisherPMC
      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been well-established empirically, a theoretical understanding of whether restarts are indeed crucial to the power of CDCL solvers is missing.

          In this paper, we prove a series of theoretical results that characterize the power of restarts for various models of SAT solvers. More precisely, we make the following contributions. First, we prove an exponential separation between a drunk randomized CDCL solver model with restarts and the same model without restarts using a family of satisfiable instances. Second, we show that the configuration of CDCL solver with VSIDS branching and restarts (with activities erased after restarts) is exponentially more powerful than the same configuration without restarts for a family of unsatisfiable instances. To the best of our knowledge, these are the first separation results involving restarts in the context of SAT solvers. Third, we show that restarts do not add any proof complexity-theoretic power vis-a-vis a number of models of CDCL and DPLL solvers with non-deterministic static variable and value selection.

          Related collections

          Most cited references14

          • Record: found
          • Abstract: not found
          • Article: not found

          GRASP: a search algorithm for propositional satisfiability

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Hard examples for resolution

              Bookmark
              • Record: found
              • Abstract: found
              • Article: not found

              Towards Understanding and Harnessing the Potential of Clause Learning

              Efficient implementations of DPLL with the addition of clause learning are the fastest complete Boolean satisfiability solvers and can handle many significant real-world problems, such as verification, planning and design. Despite its importance, little is known of the ultimate strengths and limitations of the technique. This paper presents the first precise characterization of clause learning as a proof system (CL), and begins the task of understanding its power by relating it to the well-studied resolution proof system. In particular, we show that with a new learning scheme, CL can provide exponentially shorter proofs than many proper refinements of general resolution (RES) satisfying a natural property. These include regular and Davis-Putnam resolution, which are already known to be much stronger than ordinary DPLL. We also show that a slight variant of CL with unlimited restarts is as powerful as RES itself. Translating these analytical results to practice, however, presents a challenge because of the nondeterministic nature of clause learning algorithms. We propose a novel way of exploiting the underlying problem structure, in the form of a high level problem description such as a graph or PDDL specification, to guide clause learning algorithms toward faster solutions. We show that this leads to exponential speed-ups on grid and randomized pebbling problems, as well as substantial improvements on certain ordering formulas.
                Bookmark

                Author and article information

                Contributors
                lpulina@uniss.it
                martina.seidl@jku.at
                chunxiao.ian.li@gmail.com
                Journal
                978-3-030-51825-7
                10.1007/978-3-030-51825-7
                Theory and Applications of Satisfiability Testing – SAT 2020
                Theory and Applications of Satisfiability Testing – SAT 2020
                23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings
                978-3-030-51824-0
                978-3-030-51825-7
                26 June 2020
                : 12178
                : 233-249
                Affiliations
                [8 ]GRID grid.11450.31, ISNI 0000 0001 2097 9138, University of Sassari, ; Sassari, Italy
                [9 ]GRID grid.9970.7, ISNI 0000 0001 1941 5140, Johannes Kepler University of Linz, ; Linz, Austria
                [10 ]GRID grid.46078.3d, ISNI 0000 0000 8644 1405, University of Waterloo, ; Waterloo, Canada
                [11 ]GRID grid.17063.33, ISNI 0000 0001 2157 2938, University of Toronto, ; Toronto, Canada
                [12 ]GRID grid.6451.6, ISNI 0000000121102151, Technion, ; Haifa, Israel
                Article
                17
                10.1007/978-3-030-51825-7_17
                7326553
                8ca2f768-c73e-42b9-8e18-4bcff8912d11
                © Springer Nature Switzerland AG 2020

                This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.

                History
                Categories
                Article
                Custom metadata
                © Springer Nature Switzerland AG 2020

                Comments

                Comment on this article

                scite_
                0
                0
                0
                0
                Smart Citations
                0
                0
                0
                0
                Citing PublicationsSupportingMentioningContrasting
                View Citations

                See how this article has been cited at scite.ai

                scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.

                Similar content168

                Most referenced authors72