Community-based 3-SAT formulas with a predefined solution

被引：0

作者：

Hu Y. ^{[1
]}

Luo W. ^{[1
,2
]}

Wang J. ^{[1
]}

机构：

[1] School of Computer Science and Technology, University of Science and Technology of China, Anhui, Hefei

[2] School of Computer Science and Technology, Harbin Institute of Technology, Shenzhen, Harbin

来源：

International Journal of Wireless and Mobile Computing | 2021年 / 21卷 / 04期

基金：

中国国家自然科学基金;

关键词：

community structure; predefined solution; SAT generator;

D O I：

10.1504/IJWMC.2021.121603

中图分类号：

学科分类号：

摘要：

It is crucial to generate SAT formulas with predefined solutions for the development of SAT solvers since many SAT formulas from real-world applications have solutions. Although some algorithms have been proposed to generate SAT formulas with predefined solutions, community structures of SAT formulas are not considered in these algorithms. Consequently, we propose a 3-SAT formula generating algorithm that not only guarantees the existence of a predefined solution, but also simultaneously considers community structures and clause distributions. To study the effect of community structures and clause distributions on the hardness of SAT formulas, we measure solving runtimes of two solvers, gluHack and CPSparrow, on the generated SAT formulas under different parameter settings. Through extensive experiments, we obtain some noteworthy observations. For example, the community structure has few or no effects on the hardness of SAT formulas with regard to CPSparrow but a strong effect with regard to gluHack. Copyright © 2021 Inderscience Enterprises Ltd.

引用

页码：310 / 322

页数：12

共 40 条

[1] Achlioptas D., Gomes C., Kautz H., Selman B., Generating satisfiable problem instances, National Conference on Artificial Intelligence, pp. 256-261, (2000)
[2] Achlioptas D., Jia H., Moore C., Hiding satisfying assignments: two are better than one, Journal of Artificial Intelligence Research, 24, pp. 623-639, (2005)
[3] Ansotegui C., Bonet M.L., Levy J., Random SAT instances à la carte, Proceedings of the 11th International Conference of the Catalan Association for Artificial Intelligence, 184, pp. 1-23, (2008)
[4] Ansotegui C., Bonet M.S., Levy J., Towards industrial-like random SAT instances, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pp. 387-392, (2009)
[5] Ansotegui C., Giraldez-Cru J., Levy J., The community structure of SAT formulas, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, pp. 410-423, (2012)
[6] Audemard G., Simon L., Extreme cases in SAT problems, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, pp. 87-103, (2016)
[7] Balint A., Henn M., Gableske O., A novel approach to combine a SLS-and a DPLL-solver for the satisfiability problem, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, pp. 284-297, (2009)
[8] Balyo T., Heule M.J.H., Jarvisalo M., SAT competition 2016: recent developments, Proceedings of the 31st AAAI Conference on Artificial Intelligence, pp. 5061-5063, (2017)
[9] Belov A., Diepold D., Heule M.J.H., Jarvisalo M., Proceedings of SAT Competition 2014, (2014)
[10] Burg S., Kottler S., Kaufmann M., Creating industrial-like SAT instances by clustering and reconstruction, Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, pp. 471-472, (2012)

← 1 2 3 4 →