1277.83 SAT 기반 유계 모델 검사