Unsheathing input to SAT solver from logic circuit in DIMAC format

Abstract

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.