臺灣國際科展

Do SAT Problems Have Boiling Points?

科展類別
臺灣國際科展作品
屆次
2012年
科別
電腦科學
得獎情形
二等獎
學校名稱
McClintock High School
作者
Soumya C. Kambhampati
關鍵字
SAT solvers , Boolean Satisfiability problem

摘要或動機

The Boolean Satisfiability problem, called SAT for short, is the problem of determining if a set of constraints involving Boolean (True/False) variables can be simultaneously satisfied. SAT solvers have become an integral part in many computations that involve making choices subject to constraints, such as scheduling software, chip design, decision making for robots (and even Sudoku!). Given their practical applications, one question is when SAT problems become hard to solve. The problem difficulty depends on the constrainedness of the SAT instance, which is defined as the ratio of the number of constraints to the number of variables. Research in the early 90’s showed that SAT problems are easy to solve both when the constrainedness is low and when it is high, abruptly transitioning (“boiling over” ) from easy to hard in a very narrow region in the middle. My project is aimed at verifying this surprising finding. I wrote a basic SAT solver in Python and used it to solve a large number of randomly generated 3SAT problems with given level of constrainedness. My experimental results showed that the percentage of problems with satisfying assignment transitions sharply from 100% to 0% as constrainedness varies between 4 and 5. Right at this point, the time taken to solve the problems peaks sharply. Similar behavior also holds for 2SAT and 4SAT. Thus, SAT problems do seem to exhibit phase transition behavior; my experimental data supported my hypothesis.


「為配合國家發展委員會「推動ODF-CNS15251為政府為文件標準格式實施計畫」,以及 提供使用者有文書軟體選擇的權利,本館檔案下載部分文件將公布ODF開放文件格式, 免費開源軟體可至LibreOffice 下載安裝使用,或依貴慣用的軟體開啟文件。」

檔案名稱 檔案大小 格式
Do SAT Problems Have Boiling Points? 509 KB Adobe Reader(Pdf)檔案