Ateet Bhalla
Technocrats Institute of Technology
Propositional Satisfiability is a well-known NP-complete problem, with theoretical and practical significance, and with extensive applications in many fields of Computer Science and Engineering, including Electronic Design Automation. In computer-aided design, tools for synthesis, optimization, verification, and test pattern generation use variants of SAT solvers as core algorithms. Spurred by the recent advancements in SAT solver technology, SAT algorithms have been successfully applied to problems from a wide variety of EDA applications. In the process of designing and manufacturing of VLSI hardware, various methods for verification are used, basically divided into simulations and formal verification. Verification has provided the richest application domain for use of SAT in EDA. For VLSI design, which have large collection of objects to be constrained, clear sequence of execution of constraints is important using constraint-satisfaction method for proper execution to avoid constraint loop at algorithmic level. The objective of this paper is relaxation based constraint sequence solving technique applied to the backtrack step of backtrack search solver, with the goal of increasing the ability of the solver to search different parts of the search space. The experimental results are promising, and motivate the integration of relaxation based constraint sequence solving in state-of-the-art solvers.