Computer systems have become omnipresent in our daily lives. Ensuring the reliability and robustness of these systems is an absolute necessity. Model-Checking is one of the approaches dedicated to this purpose. Its objective is to either prove the absence of failures or identify potential ones. Model-Checking is declined into several technique. Among these, there is Bounded Model Checking (BMC), a technique that relies on Boolean satisfiability (SAT). The core idea behind BMC is to verify that a model, restricted to executions bounded by some integer k, satisfies its specification, often defined as a set of temporal logic expressions. In this approach, system behaviors are expressed as SAT problems. Unlike other formal verification methods, SAT-based BMC is generally not prone to the state space explosion problem, which can be problematic when dealing with designs involving millions of variables and constraints. However, the trade-off lies in the time complexity, as SAT problems are known to be NP-complete. Over the past few decades, significant advancements have been made in sequential SAT solving. These developments have mainly focused on utilizing dynamic information, acquired during the solving process (e.g., Learning Binary Clauses), or static information, extracted from the inherent structure of the SAT problem (e.g., community structure). However, less attention has been given to the structural information embedded within the original problem. For instance, when a BMC problem is reduced to SAT, critical information is lost in the translation. As this thesis emphasizes, reintegrating this lost information can greatly enhance the solving process. This work explores ways to improve SAT-based BMC problem-solving, both in sequential and parallel settings, by harnessing and leveraging pertinent information extracted from the problem's inherent characteristics. This may involve improving existing generic heuristics or effectively breaking down the formula into partitions.