A Brief Analogy of NNs and Literal Selection Procedures within SAT Solvers

Neural Networks (NNs) are an important component in analytical solving and heuristic determination of propositional logical statements in current and future methodologies of such statements. There are many devised architectures that predict solutions for given propositional statements as a large data-set (10000-100000 problems) and successfully categorize it’s UN/SAT core predictability to vary degrees of accuracy. This work is the first step towards designing, implementing, and testing a Transformer Neural Network that is capable of handling the generation and solving of First Order Propositional Logic, and can be modified for Higher Order Logic, in a parallel fashion. Understanding the current standards for these systems, such as NeuroSAT and an exploration into other possibilities of approach that are non-conventional, such as TGNs (Typed Graph Networks). Given the ultimate goal to develop and initially theorize a mathematically sound structure for a TNN (Transformer Neural Network) employing parallel multi-head attention processing queues, it is important to gain specific direction in regards to the other tiers of the complete system with the analysis of closely related works. Furthermore, the paradigm of exploring literal based choice analytics and optimization patterns within a prime NN architecture for solving SAT based problems up to k levels will be an important exploration into improving the run-time and accuracy of Boolean Satisfiability using DPLL.



Work Title A Brief Analogy of NNs and Literal Selection Procedures within SAT Solvers
Open Access
  1. Arya Keni
  2. Mahfuza Farooque
  1. Neural Networks, Machine Learning, SAT Solvers, GNN, TNN, RNN
License MIT License
Work Type Journal
Publication Date January 20, 2023
  1. Computer Science, Formal Verification
  1. English
Geographic Area
  1. State College, PA, USA
Deposited January 26, 2023




This resource is currently not in any collection.

Work History

Version 1

  • Created
  • Updated
  • Added Creator Arya Keni
  • Added Creator Mahfuza Farooque
  • Added A_Brief_Analogy_of_NNs_on_SAT_Solvers____Reinvention_Journal_Published_Version__wBooleanExplanations_.pdf
  • Updated License Show Changes
    • https://opensource.org/licenses/MIT
  • Published