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