COUNTING SOLUTIONS TO RANDOM CNF FORMULAS

被引:6
|
作者
Galanis, Andreas [1 ]
Goldberg, Leslie Ann [1 ]
Guo, Heng [2 ]
Yang, Kuan [3 ]
机构
[1] Univ Oxford, Dept Comp Sci, Oxford OX1 3QD, England
[2] Univ Edinburgh, Sch Informat, Informat Forum, Edinburgh EH8 9AB, Midlothian, Scotland
[3] Shanghai Jiao Tong Univ, John Hoperoft Ctr Comp Sci, Shanghai 200240, Peoples R China
基金
欧洲研究理事会;
关键词
random k-SAT; approximate counting; satisfiability; RANDOM K-SAT; NUMBER; THRESHOLDS; UNIQUENESS; COLORINGS; ALGORITHM; WALKSAT;
D O I
10.1137/20M1351527
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We give the first efficient algorithm to approximately count the number of solutions in the random k-SAT model when the density of the formula scales exponentially with k. The best previous counting algorithm for the permissive version of the model was due to Montanari and Shah and was based on the correlation decay method, which works up to densities (1 + o(k)(1)) 2 log k/k , the Gibbs uniqueness threshold for the model. Instead, our algorithm harnesses a recent technique by Moitra to work for random formulas with much higher densities. The main challenge in our setting is to account for the presence of high-degree variables whose marginal distributions are hard to control and which cause significant correlations within the formula.
引用
收藏
页码:1701 / 1738
页数:38
相关论文
共 50 条
  • [1] Improved Bounds for Sampling Solutions of Random CNF Formulas
    He, Kun
    Wu, Kewen
    Yang, Kuan
    PROCEEDINGS OF THE 2023 ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, SODA, 2023, : 3330 - 3361
  • [2] Model Counting for CNF Formulas of Bounded Modular Treewidth
    Daniel Paulusma
    Friedrich Slivovsky
    Stefan Szeider
    Algorithmica, 2016, 76 : 168 - 194
  • [3] Understanding Model Counting for β-acyclic CNF-formulas
    Brault-Baron, Johann
    Capelli, Florent
    Mengel, Stefan
    32ND INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2015), 2015, 30 : 143 - 156
  • [4] Model Counting for CNF Formulas of Bounded Modular Treewidth
    Paulusma, Daniel
    Slivovsky, Friedrich
    Szeider, Stefan
    ALGORITHMICA, 2016, 76 (01) : 168 - 194
  • [5] Satisfiability threshold for random XOR-CNF formulas
    Creignou, Nadia
    Daude, Herve
    Discrete Applied Mathematics, 1999, 96-97 : 41 - 53
  • [6] Satisfiability threshold for random XOR-CNF formulas
    Creignou, N
    Daude, H
    DISCRETE APPLIED MATHEMATICS, 1999, 97 : 41 - 53
  • [7] A spectral technique for random satisfiable 3CNF formulas
    Flaxman, Abraham
    RANDOM STRUCTURES & ALGORITHMS, 2008, 32 (04) : 519 - 534
  • [8] A spectral technique for random satisfiable 3CNF formulas
    Flaxman, A
    PROCEEDINGS OF THE FOURTEENTH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, 2003, : 357 - 363
  • [9] Mapping many-valued CNF formulas to boolean CNF formulas
    Ansótegui, C
    Manyà, F
    35TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC, PROCEEDINGS, 2005, : 290 - 295
  • [10] Short Propositional Refutations for Dense Random 3CNF Formulas
    Mueller, Sebastian
    Tzameret, Iddo
    2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 501 - 510