Exploring Full Adder Design using SAT-Based Approach

Computational techniques called SAT (Boolean Satisfiability Problem) solvers are employed to resolve Boolean Satisfiability Problem cases. Finding a way to assign truth values (true or false) to variables in a Boolean formula so that the formula evaluates to true is the task at hand. Algorithms and heuristics are used by SAT solver programs to quickly search the universe of potential variable assignments and assess if a satisfied assignment is possible. A Boolean formula in conjunctive normal form (CNF) or another appropriate representation is usually entered into SAT solver software. SAT solver tools are available in several versions, with variations in functionality, usability, and performance, including both open-source and commercial options. This study investigates the utility of SAT solvers in the context of digital logic circuit design. Full adder circuits are explored using Mini SAT solver tool. The solve objective of this study is to build a step-by-step guide in solving Boolean expressions using SAT solver tool.