布爾可滿足性(SAT) 問題是確定現有的賦值是否可以讓命題公式被評估為真，針對布林可滿足性問題的解法，一般分為完整演算法以及不完整演算法兩類。而解SAT 問題的工具我們稱為SAT solver (求解器)。許多實際的問題，包括SoC 驗證問題，已被證明能夠映射到SAT 問題。隨著EDA 和人工智能技術的快速發展，我們現在看到的SAT 問題規模越來越大。但是，並沒有一個特定的SAT solver 能夠有效地解決每個SAT 問題，即使是最廣泛使用的基於完整演算法的SAT solver 也未必能在每個SAT 問題上都有良好的表現。因此，我們的目標是建立一個相對小型且可以快速分類SAT 問題適合哪種SAT solver 的神經網路。
我們從SATzilla 中選擇出數個instance features，並進行修改以及分析。經過多次分析以及fine-tune 後，最成功的神經網絡的準確率為80.04%。實驗結果顯示，我們的模型準確率優於過去的研究，且平均執行時間方面仍具有競爭力。且與單一SAT solver 比較執行時間時，速度上有著明顯的差異。這代表我們提出的模型不僅可以成功預測SAT 問題最適合的SAT solver，而且總執行時間也不會太耗時。

Boolean satisfiability (SAT) problem is to determine whether existing an assignment can let propositional formula be evaluated as true. However, there is no specific SAT solver be able to solve every SAT problem effectively. This motivate to the algorithm portfolio.
There are lots of approaches to algorithm portfolios for SAT, and the most successful one is SATzilla. SATzilla is most successful, but is a very complicated mechanism, not easy to understand and modify. Our goal is to create a relatively small and fast classification
system - Neural network-based SAT instances classification system. In our system,selected instance features are all derived from SATzilla by modifying parts of its features,using two hardware SAT solvers in our previous works and Minisat as candidate solvers, and SAT instances are all chosen from SATLIB as well as SAT competitions.
The most successful neural network accuracy was 80.04%. Experimental result shows that our proposed method is competitive with previous works in terms of average execution time, and the model accuracy is better than the previous work. And while comparing the execution time with a single SAT solver, there is a significant difference in speed.
It represents that our proposed that our proposed model can not only predict the best solver required by the input CNF instance, but the total execution time would not be too time-consuming.

[1] Yean-Ru Chen Chin-Wei Lien. A hardware sat solver with efficient bcp. Masters thesis, National Cheng Kung University, 2019.
[2] Stephen A Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, pages 151–158, 1971.
[3] Martin Davis, George Logemann, and Donald Loveland. A machine program for
theorem-proving. Communications of the ACM, 5(7):394–397, 1962.
[4] Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? arXiv preprint arXiv:1802.08535, 2018.
[5] Carla P Gomes and Bart Selman. Algorithm portfolios. Artificial Intelligence, 126(1-2):43–62, 2001.
[6] Holger H Hoos and Thomas Stützle. Stochastic local search: Foundations and applications. Elsevier, 2004.
[7] Samuel H Huang. Supervised feature selection: A tutorial. Artif. Intell. Res., 4(2):22–37, 2015.
[8] Frank Hutter, Holger H Hoos, Kevin Leyton-Brown, and Thomas Stützle. Paramils: an automatic algorithm configuration framework. Journal of Artificial Intelligence Research,36:267–306, 2009.
[9] Michail G Lagoudakis and Michael L Littman. Learning to select branching rules in the dpll procedure for satisfiability. Electronic Notes in Discrete Mathematics, 9:344–359, 2001.
[10] D Mitchell, B Selman, and H Leveque. A new method for solving hard satisfiability problems. In Proceedings of the tenth national conference on artificial intelligence (AAAI-92), pages 440–446, 1992.
[11] Mladen Nikolić, Filip Marić, and Predrag Janičić. Instance-based selection of policies for sat solvers. In International Conference on Theory and Applications of Satisfiability Testing, pages 326–340. Springer, 2009.
[12] Mladen Nikolić, Filip Marić, and Predrag Janičić. Simple algorithm portfolio for sat. Artificial Intelligence Review, 40(4):457–465, 2013.
[13] Eugene Nudelman, Kevin Leyton-Brown, Holger H Hoos, Alex Devkar, and Yoav Shoham. Understanding random sat: Beyond the clauses-to-variables ratio. In International Conference on Principles and Practice of Constraint Programming, pages 438–452. Springer, 2004.
[14] Paul Walton Purdom, Jr and Cynthia A Brown. The pure literal rule and polynomial average time. SIAM Journal on Computing, 14(4):943–953, 1985.
[15] Philip Sedgwick. Pearson＇s correlation coefficient. Bmj, 345, 2012.
[16] Bart Selman, Henry A Kautz, and Bram Cohen. Noise strategies for improving local search. In AAAI, volume 94, pages 337–343, 1994.
[17] Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L Dill. Learning a sat solver from single-bit supervision. arXiv preprint arXiv:1802.03685, 2018.
[18] Yean-Ru Chen Shi-Wei Wu. A non-exhaustive hardware sat solver with deeper state exploration capability. Master’s thesis, National Cheng Kung University, 2019.
[19] Dave AD Tompkins and Holger H Hoos. Ubcsat: An implementation and experimentation environment for sls algorithms for sat and max-sat. In International conference on theory and applications of satisfiability testing, pages 306–320. Springer, 2004.
[20] Dave AD Tompkins, Frank Hutter, and Holger H Hoos. Scaling and probabilistic
smoothing (saps). SAT, 2004.
[21] Lin Xu, Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. Satzilla: portfoliobased algorithm selection for sat. Journal of artificial intelligence research, 32:565–606, 2008.
[22] Lin Xu, Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. Satzilla2009: an
automatic algorithm portfolio for sat. SAT, 4:53–55, 2009.