This thesis studies two NP-complete problems, {\it Clique} and {\it Boolean Satisfiability} (SAT), under the proof complexity view. For Clique, we study its average-case hardness. We show that with high probability over an Erd\"os-R\'enyi random graph $G$, the proof system under consideration has no short proof of the true statement ``$G$ contains no $k$-clique''. Here $k$ is a suitable parameter, and the shortness of proof is defined by natural complexity measures such as size, width, degree, etc. Specifically, we prove an exponential-in-$k$ size lower bound for the {\it Resolution} system, and an almost optimal degree lower bound for the {\it Sum-of-Squares} (SoS) system. For SAT, we study a different aspect, that is the proof-theoretic power and limitation of {\it Conflict-Driven Clause-Learning Algorithms} (CDCL-solvers), a standard class of modern SAT-solving algorithms whose often surprising performances call for explanation.We define proof systems modeling CDCL-solvers and, for solvers with the ordered-decision strategies, show their equivalence to either resolution or ordered resolution, depending on the learning scheme employed.