75705

Автор(ы): 

Автор(ов): 

1

Параметры публикации

Тип публикации: 

Статья в журнале/сборнике

Название: 

Empirical evaluation of the asymptotic behavior of the analysis complexity of hard random 3-cnf formulas.

Электронная публикация: 

Да

ISBN/ISSN: 

0000

DOI: 

DOI: 10.3233/FAIA220420

Наименование источника: 

  • Machine Learning and Artificial Intelligence

Обозначение и номер тома: 

Vol. 360

Город: 

  • Пекин

Издательство: 

  • IOS press

Год издания: 

2022

Страницы: 

28-34
Аннотация
This paper continued the study of the complexity behavior of the satisfiability analysis of hard random formulas given in the conjunctive normal form (CNF). In the 3-CNF formula, each clause contains three literals of logical variables. The number of logical variables in the formula is N. In this paper, the SAT solver is improved by introducing equality reduction and pure literal identification procedures. The solver improvement reduced the exponent (with base 2) from N/20.86 to N/21.41 with an R=4.6 ratio of the number of clauses to the number of variables. The results show that the efficiency of the pure literals identification procedure decreases as R increases. An important part of the study is an empirical estimation of the algorithmic complexity of the SAT problem with large number of variables. The proposed method gives a convenient lower bound on the complexity of analysis for random 3-CNF formulas. We estimated the algorithmic complexity for the range N=256÷8192. The exponential dependence of complexity on N for random 3-CNF formulas at a fixed value of R is demonstrated in this range.

Библиографическая ссылка: 

Уваров С.И. Empirical evaluation of the asymptotic behavior of the analysis complexity of hard random 3-cnf formulas. // Machine Learning and Artificial Intelligence. 2022. Vol. 360. С. 28-34.