Evolving Solutions to Community-Structured Satisfiability Formulas

被引:0
|
作者
Neumann, Frank [1 ]
Sutton, Andrew M. [2 ]
机构
[1] Univ Adelaide, Sch Comp Sci, Optimisat & Logist, Adelaide, SA, Australia
[2] Univ Minnesota, Dept Comp Sci, Duluth, MN 55812 USA
关键词
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
We study the ability of a simple mutation -only evolutionary algorithm to solve propositional satisliability formulas with inherent community structure. We show that the community structure translates to good fitness -distance correlation properties, which implies that the objective function provides a strong signal in the search space for evolutionary algorithms to locate a satisfying assignment efficiently. We prove that when the formula clusters into communities of size s C (log n) fl ()(n (22i) for some constant 0 < < 1, and there is a nonuniform distribution over communities, a simple evolutionary algorithm called the (1+1) 1 i\ finds a satisfying assignment in polynomial time on a 1 ()(1) traction of formulas with at least constant constraint density. This is a significant improvement over recent results on uniform random formulas, on which the same algorithm has only been proven to he efficient on uniform formulas of at least logarithmic density.
引用
收藏
页码:2346 / 2353
页数:8
相关论文
共 50 条
  • [41] MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the ∃*∀* Fragment
    Finkbeiner, Bernd
    Hahn, Christopher
    Hans, Tobias
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2018), 2018, 11138 : 521 - 527
  • [42] Phase Transition in Matched Formulas and a Heuristic for Biclique Satisfiability
    Chromy, Milos
    Kucera, Petr
    THEORY AND PRACTICE OF COMPUTER SCIENCE, SOFSEM 2019, 2019, 11376 : 108 - 121
  • [43] Satisfiability threshold for random XOR-CNF formulas
    Creignou, N
    Daude, H
    DISCRETE APPLIED MATHEMATICS, 1999, 97 : 41 - 53
  • [44] A method to generate formulas for temporal logic satisfiability checkers
    Sekizawa, Toshifusa
    Takai, Toshinori
    Tanabe, Yoshinori
    Takahashi, Koichi
    ELECTRONICS AND COMMUNICATIONS IN JAPAN PART II-ELECTRONICS, 2007, 90 (11): : 99 - 108
  • [45] Satisfiability of Acyclic and almost Acyclic CNF Formulas (II)
    Ordyniak, Sebastian
    Paulusma, Daniel
    Szeider, Stefan
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2011, 2011, 6695 : 47 - 60
  • [46] An algorithm for the satisfiability problem of formulas in conjunctive normal form
    Schuler, R
    JOURNAL OF ALGORITHMS-COGNITION INFORMATICS AND LOGIC, 2005, 54 (01): : 40 - 44
  • [47] An algorithm for solving satisfiability problem based on the structural information of formulas
    Zhang, Zaijun
    Xu, Daoyun
    Zhou, Jincheng
    FRONTIERS OF COMPUTER SCIENCE, 2021, 15 (06)
  • [48] Optimization and probabilistic satisfiability on nested and co-nested formulas
    Pretolani, Daniele
    ANNALS OF OPERATIONS RESEARCH, 2011, 188 (01) : 371 - 387
  • [49] CSiSAT: A Satisfiability Solver for SMT Formulas with Continuous Probability Distributions
    Gao, Yang
    Fraenzle, Martin
    PROCEEDINGS OF THE 2016 WORKSHOP ON SYMBOLIC AND NUMERICAL METHODS FOR REACHABILITY ANALYSIS (SNR), 2016,
  • [50] Approximating the satisfiability threshold for random k-XOR-formulas
    Creignou, N
    Daudé, H
    Dubois, O
    COMBINATORICS PROBABILITY & COMPUTING, 2003, 12 (02): : 113 - 126