The empirical success of Transformer-based Large Language Models (LLMs) has elicited significant interest in their application for security domains such as formal verification and program analysis. However, their application in formal domains, such as formal verification and program analysis, is constrained by the lack of mechanical understanding and the risk of hallucinations. To address these challenges, we present a robust theoretical construction establishing that transformer-LLMs with CoT can solve an NP-Hard logical reasoning problem, specifically 3-SAT. Our construction provides theoretical guarantees that these models can either simulate the deductive search processes of SAT-solving or probabilistically generate correct solutions as the most likely completion. Empirically, we demonstrate that transformers can generalize these procedures across different formula distributions, reinforcing their potential for reliable formal reasoning.