This is a memo of complexity analysis of "checking the existence of counter-example at bound k using bounded model checking with SAT". (And this is different from the complexity of bounded model checking using SAT). In BMC using SAT, model…

SAT: Typical-Case Complexity Sanjit A. Seshia EECS, UC Berkeley