SAT solver를 이용해서 스도쿠 풀이하는 프로그램을 만들어라고 과제를 내줬는데
(정확히는 DPLL 알고리즘을 이용해서)

어떻게 짜야할지 감이 안잡힌다

일단 저 DPLL을 직접 만들어봐야 감이 좀 잡힐꺼같은데 자료 찾아보는것 조차도 머리가 아픔

An Extensible SAt-solver 라는 pdf 구해서 읽어보면서 따라하려했는데

내가 영어라 딸리는지 머리가 빠가인지는 모르겠지만 ㅠㅠ 할려니 힘드네

스도쿠에 필요한 조건들을 CNF형으로 바꾸는건 하겠는데 그걸 어떻게 만들어야할지ㅡ감이 안잡힘


과제 제출도 파이썬으로 해라고 해서 골치아픈데... 뭐 조언 해줄수 있는거 없냐 갤러들아??