Deciding Satisfiability in the Twinkling of an Eye

Okoh Ufuoma *

Department of Mathematics, Southern Maritime Academy, Uwheru, Delta State, Nigeria.

*Author to whom correspondence should be addressed.


Abstract

The question as to whether a CNF Boolean formula is satisfiable is referred to as Boolean satisfiability problem (SAT). For decades now, this problem has attracted a great deal of attention. A well-known algorithm for solving this problem is the DPLL algorithm. However, this algorithm may run in an exponential (long) time. The great plan embraced in this work is to show how the satisfiability of any CNF Boolean formula can be decided in a very short time. This is achieved by the modification of the DPLL algorithm and the introduction of a quick algorithm.

Keywords: SAT, satisfiable, satisfiability rules, quick algorithm, DPLL approach


How to Cite

Ufuoma, Okoh. 2024. “Deciding Satisfiability in the Twinkling of an Eye”. Asian Research Journal of Mathematics 20 (6):15-29. https://doi.org/10.9734/arjom/2024/v20i6804.

Downloads

Download data is not yet available.

References

Mironov, Ilya; Zhang, Lintao. Biere, Armin; Gomes, Carla P. (eds.). "Applications of SAT Solvers to Cryptanalysis of Hash Functions". Theory and Applications of Satis ability Testing | SAT 2006. Lecture Notes in Computer Science. Springer. Mathematics Handbook for Science and Engineering, Springer, New York, 2006, 5th ed; 2006.

Cook SA. The complexity of theorem proving procedures, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. 1971;151-158.

Baker TP, Gill J, Solovay R. Relativizations of the P=?NP question, SIAM Journal on Computing. 1975;4(4):431-442.

Aaronson S, Wigderson A. Algebrization: a new barrier in complexity theory. in STOC. 2008;731{740.

Aho, Alfred V, Hopcroft, John E, Ullman, Je rey D. The Design and Analysis of Computer Algorithms. Addison-Wesley. Theorem 10.40.; 1974.

Davis M, Logemann G, Loveland D. Communications of the ACM. 1962;5:394{397.

Ufuoma O. Boolean Subtraction and Division with Application in the Design of Digital Circuits. Journal of Engineering Research and Reports. 2021 Apr 24;20(5):95-117. DOI: 10.9734/JERR/2021/v20i517316

Rajendra P. Fundamentals of electrical engineering. Prentice-Hall of India.

Rajaraman, Radhakrishnan. Introduction to digital computer design. PHI Learning Pvt. Ltd.

Henryk Greniewski, Krystyn Bochenek, Romuald Marczynski. Application of Bi-elemental Boolean algebra to electronic circuits. Studia Logica: An International Journal for Symbolic Logic. T. 1955;2:7-76.

Okoh U., A Novel, Efficient and Generalised Approach to Boolean Satis ability, Journal of Engineering Research and Reports, Volume 26, Issue 3, Page 91-103, 2024; Article no.JERR.110430 ISSN: 2582-2926.