Experimental analyses on phase transitions in compiling satisfiability problems  

作　　者：GAO Jian WANG JiaNan YIN MingHao 

机构地区：[1]College of Information Science and Technology, Dalian Maritime University [2]College of Computer Science, Northeast Normal University

出　　处：《Science China(Information Sciences)》2015年第3期77-87,共11页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China(Grant Nos.61370052,61370156,and 61175056);Natural Science Foundation of Jilin Province(GrantNo.201215006);Program for New Century Excellent Talents in University(Grant No.NCET-13-0724);Fundamental Research Funds for the Central Universities(Grant Nos.3132013335,3132014095)

摘　　要：In the past decade, a kind of well-known phenomena in many complex combinatorial problems such as satisfiability problem, called phase transition, have been widely studied. In this paper, the phase transition phenomena are investigated during compiling k-satisfiability problems into tractable languages with empirical methods. Ordered binary decision diagram and deterministic-decomposable negation normal form are selected as the tractable target languages for the compilation. Via intensive experiments, it can be concluded that an easy hard-easy pattern exists during the compilations, which is only related to the ratio of the number of clauses to that of variables if we set k to a fixed value, rather than to the target languages. Moreover, it can be concluded that the space exhausted during the compilations grows exponentially with the number of variables growing, whereas there is also a phase transition separating the polynomial-increment region from the exponential-increment region. Additionally, it can be observed that there is a phase transition of prime implicants around peak points of the easy hard-easy pattern and the ratios of random instances whose average lengths of prime implicants are larger than the threshold 0.5 change sharply. From these analyses, it can be concluded that prime implieant length and solution interchangeability are crucial impacts on sizes of compilation results.In the past decade, a kind of well-known phenomena in many complex combinatorial problems such as satisfiability problem, called phase transition, have been widely studied. In this paper, the phase transition phenomena are investigated during compiling k-satisfiability problems into tractable languages with empirical methods. Ordered binary decision diagram and deterministic-decomposable negation normal form are selected as the tractable target languages for the compilation. Via intensive experiments, it can be concluded that an easy hard-easy pattern exists during the compilations, which is only related to the ratio of the number of clauses to that of variables if we set k to a fixed value, rather than to the target languages. Moreover, it can be concluded that the space exhausted during the compilations grows exponentially with the number of variables growing, whereas there is also a phase transition separating the polynomial-increment region from the exponential-increment region. Additionally, it can be observed that there is a phase transition of prime implicants around peak points of the easy hard-easy pattern and the ratios of random instances whose average lengths of prime implicants are larger than the threshold 0.5 change sharply. From these analyses, it can be concluded that prime implieant length and solution interchangeability are crucial impacts on sizes of compilation results.

关 键 词：phase transition knowledge compilation random k-SAT prime implicants easy-hard-easy pattern 

分 类 号：TP314[自动化与计算机技术—计算机软件与理论]