The paper presents a fully SAT-based method for unbounded symbolic model checking using Craig interpolants. This method is more efficient than BDD-based symbolic model checking and compares favorably with some recent SAT-based model checking methods on positive instances. The approach leverages the ability of SAT solvers to produce refutations, which can be used to generate interpolants. These interpolants are then used to perform finite-state reachability analysis and LTL model checking. The paper outlines the theoretical foundations of resolution proofs and interpolation, and provides a detailed algorithm for unbounded model checking based on interpolation. Practical benchmarks from commercial microprocessor designs demonstrate the effectiveness of the method, showing that it can verify properties that standard symbolic model checking cannot. The method is also compared with other SAT-based and BDD-based approaches, highlighting its advantages in terms of efficiency and scalability.The paper presents a fully SAT-based method for unbounded symbolic model checking using Craig interpolants. This method is more efficient than BDD-based symbolic model checking and compares favorably with some recent SAT-based model checking methods on positive instances. The approach leverages the ability of SAT solvers to produce refutations, which can be used to generate interpolants. These interpolants are then used to perform finite-state reachability analysis and LTL model checking. The paper outlines the theoretical foundations of resolution proofs and interpolation, and provides a detailed algorithm for unbounded model checking based on interpolation. Practical benchmarks from commercial microprocessor designs demonstrate the effectiveness of the method, showing that it can verify properties that standard symbolic model checking cannot. The method is also compared with other SAT-based and BDD-based approaches, highlighting its advantages in terms of efficiency and scalability.