Satisfiability probability(SAT) solvers are algorithms that take well-formed formulas and return true if satisfiable and false otherwise. They are significantly useful in various tasks in-circuit verification and have prominent importance in various fields such as automated verification, Electronic Design Automation (EDA) which include formal checking of equivalence, artificial intelligence planning, and so on. The input to these SAT solvers is generally accepted in DIMAC CNF (conjunctive normal form), which is a textual representation of the equation in CNF form. Most verification tasks are commenced from a description of problem instances at the logic circuit level, deducing DIMAC CNF format from the given logic circuit could be tedious and time-consuming if done manually as the conversion includes complex formulas. This paper aims to present an effective code that could easily convert any given logic circuit to DIMAC CNF format just by selecting gate and proper variable names to operate upon according to the heuristic presented by a logic circuit. The output thus formed could be directly given as input to any SAT solver that uses DIMAC format readily, abating time and conversion efforts. The final part of the paper also demonstrates an example for the acyclic circuit and compares the result of generated output to manually derived formula for the same circuit on various parameters

DIMAC, CNF, SAT solvers, input generator

[1] C Gomes, H Kautz, A Sabharwal, B Selman. "Satisfiability Solvers"2008.https://www.cs.cornell.edu/gomes/pdf/2008_gomes_knowledge_satisfiability.pdf
[2] A.Gilles, S Laurent. "Predicting Learnt Clauses Quality in Modern SAT Solvers". IJCAI International Joint Conference on Artificial Intelligence., pp 399-404 2009.
[3] F Zhaohui, Y Yinlei, M Sharad ." Considering Circuit Observability Don?t Care in CNF Satisfiability". DATE?05, Mar 2005, Munich, Germany. pp.1108-1113. ?hal-00181279?
[4] R Klimek, K Grobler-Dębska, E Kucharska . "System for automatic generation of logical formulas". MATEC Web of Conferences.,pp 252:03005,2019;.
[5] S Gopalakrishnan, V Durairaj, P Kalla. "Integrating CNF and BDD based SAT solvers". Eighth IEEE International High-Level Design Validation and Test Workshop; 2003.
[6] A Smith ." Diagnosis of combinational logic circuits using Boolean satisfiability". Ottawa: Library and Archives Canada = Bibliothèque et Archives Canada; 2005.
[7] N E?n, N S?rensson ." Translating Pseudo-Boolean Constraints into SAT". Journal on Satisfiability, Boolean Modeling, and Computation. pp 2(1-4):1-26.,2006.
[8] Ifat Jahangir, Anindya Das, Masud Hasan, ?Facile Algebric Representation of a Novel Quaternary Logic?.International Journal of Computer Sciences and Engineering Vol.4 Issue 5,pp 1-15, 2016.