선택한 단어 수는 입니다.
최소 단어 이상 선택하여야 합니다.
최소 단어 이상 선택하여야 합니다.
선택한 단어 수는 30입니다.
최대 10 단어까지만 선택 가능합니다.
최대 10 단어까지만 선택 가능합니다.
문제 정의
- 왜냐하면 비에르 (Biere)는 인공지능의 결정적 계획 문제에서 바운디드 모델 검증의 아이디어를 얻었기 때문이다. 거듭 강조 하지만, 본 논문에서는 새로운 아이디어를 제안하기 보다는 사례 연구를 충실히 다루어, 독자들로 하여금 주어진 문제를 SAT 으로 변환하는 방법을 이해시키고자 한다.
- 특히, 바운디드 모델 검증의 핵심인 SAT(Satisfiability)변환에 대한 상세한 이해 없이는 바운디드 모델 검증을 이해하거나 활용하기 어렵다. 본 논문에서는 독자들이 바운디드 모델 검증을 쉽게 이해하는 것을 돕기 위해서 만족가능성 문제의 사례 연구를 상세히 기술코자 한다. 여기에서 사례로 선정한 것은 루빅 큐브[2]이다.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.