Proofdoku is an AI-based game design that extends Sudoku. In addition to playing by the rules of the traditional logic puzzle, players must explain their reasoning. An AI system checks this reasoning and provides hints that guide the player to discover new reasoning patterns for themselves. Co-developing the game design and the AI system, implemented using the technology of Answer Set Programming (ASP), guided us to include features that depend on high-complexity combinatorial search and optimization. We developed Proofdoku to better understand the implications of designing and deploying game systems that depend on ASP for live interaction. This paper offers design tradeoffs and makes suggestions for future deployments of ASP-backed game designs.