17
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      A Model of Random Industrial SAT

      Preprint
      , ,

      Read this article at

      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

          One of the most studied models of SAT is random SAT. In this model, instances are composed from clauses chosen uniformly randomly and independently of each other. This model may be unsatisfactory in that it fails to describe various features of SAT instances, arising in real-world applications. Various modifications have been suggested to define models of industrial SAT. Here, we focus on community-structured SAT. Namely, the set of variables consists of a number of disjoint communities, and clauses tend to consist of variables from the same community. Thus, we suggest a model of random community-structured SAT. There has been a lot of work on the satisfiability threshold of random k-SAT, starting with the calculation of the threshold of 2-SAT, up to the recent result that the threshold exists for sufficiently large k. In this paper, we endeavor to study the satisfiability threshold for random industrial SAT. Our main result is that the threshold of random community-structured SAT tends to be smaller than its counterpart for random SAT. Moreover, under some conditions, this threshold even vanishes.

          Related collections

          Most cited references18

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

          Random K-satisfiability problem: from an analytic solution to an efficient algorithm.

          We study the problem of satisfiability of randomly chosen clauses, each with K Boolean variables. Using the cavity method at zero temperature, we find the phase diagram for the K=3 case. We show the existence of an intermediate phase in the satisfiable region, where the proliferation of metastable states is at the origin of the slowdown of search algorithms. The fundamental order parameter introduced in the cavity method, which consists of surveys of local magnetic fields in the various possible states of the system, can be computed for one given sample. These surveys can be used to invent new types of algorithms for solving hard combinatorial optimizations problems. One such algorithm is shown here for the K=3 satisfiability problem, with very good performances.
            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Threshold values of randomK-SAT from the cavity method

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

              Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem

                Bookmark

                Author and article information

                Journal
                31 July 2019
                Article
                1908.00089
                8972c407-a40c-4115-a644-aa8226df4f88

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                30 pages
                cs.DS math.PR

                Data structures & Algorithms,Probability
                Data structures & Algorithms, Probability

                Comments

                Comment on this article