As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
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.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.