-
Sudoku and Nonogram with z3
서론 이전에 z3와 Boolector를 비교하는 글을 올린 적이 있습니다. (Link) 그런데 정작 z3에 대해서 글이 잘 없어서, 이번에 z3로 퍼즐을 푸는 글을 작성해보게 되었습니다. 스도쿠는 이미 충분히 유명하고, 노노그램은 네모네모 로직이나 피크로스 등을 통해서 많은 분들이 알고 계신 퍼즐이기 때문에 고르게 되었습니다. 이번 글에서는 스도쿠랑 노노그램의 솔버를 하나씩 설명해가면서 작성해보려고 합니다. 본론 Sudoku 스도쿠는 9x9개의 정수를 맞추는 퍼즐 게임입니다. 정수는 모두 1부터 9로 구성되며, 9x9개의 정수 중 몇 개의 값이 고정되어 있습니다. Wikipedia에 있는 sudoku...
-
SMT Solver in CTF - z3 vs Boolector
서론 SMT (Satisfiability modulo theories) Solver는 CTF에서 빠질 수 없는 존재입니다. SMT Solver가 무엇인지 구체적으로 설명하기 보다는, 다음 z3py 예시를 보는 것이 더 직관적일 것입니다. (Link) x = Int('x') y = Int('y') s = Solver() print s s.add(x > 10, y == x + 2) print s print "Solving constraints in the solver s ..." print s.check() print "Create a new scope..." s.push() s.add(y < 11) print s print "Solving updated set of constraints..." print...