SAT Encodings for SudokuBug Catching in 2006 FallSep. 26, 2006Gi-Hwon Kwon22Agenda•Introduction•Background and Previous Encodings•Optimized Encoding• Experimental Results• Conclusions33What is Sudoku ?482395716719682453536417892928564371673129584154738269867943125241856937395271648235719451986317814329441935216Given a problem, the objectvie is to find a satisfying assignment w.r.t. Sudoku rules.ProblemSolution There is a number in each cell. A number appears once in each row. A number appears once in each column. A number appears once in each block.Sodoku rules44Sudoku as SAT ProblemEncoderSAT SolverDecoderCNFSAT?yesnoSudokusymbol tablemodelNo solution foundSolution found55Previous EncodingsEncoderSAT SolverDecoderCNFSAT?yesSudokusymbol tablemodelMinimal encoding [Lynce & Ouaknine, 2006]Extended encoding [Lynce & Ouaknine, 2006]Efficient encoding [Weber, 2005]66Analysis of Previous EncodingsExtendedEfficientMinimalNumber of ClausesNumber of VariablesEncodingN∗NN∗N∗N∗ N−12∗3kN∗NN∗N∗N∗ N− 12∗4kN∗NN∗N∗N∗ N−12∗4kN3N3N377Exponential Growth in Clauses637794812477670484731292450736563125924168829minimal850371213303424011296705326721675062512313611745efficient850568043304652811303908327110475250012390411988extended81x8164x6449x4936x3625x2516x169x9size010,000,00020,000,00030,000,00040,000,00050,000,00060,000,00070,000,00080,000,00090,000,0009x9 16x16 25x25 36x36 49x49 64x64 81x81sizeNumber of clausesminimalefficientextended88Experimental Results5314412621441176494665646656156251562540964096729729varsefficient encoding850411043303662411297986326788032678607509037509171232341232401177511770clausesstackstacktimetimetimetime17.480.210.090.000.00time5314412621441176494665646656156251562540964096729729varsminimal encoding63783464 24779088 8474410 2451400 2451380 563403 563417 92514 92520 8859 8854 clausesstackstacktimetimetimetime9.070.460.100.000.00timestack85060787531441easy81x81stack33048912262144easy64x641.4711305189117649easy49x490.67327176846656hard36x360.50327174846656easy36x360.2175277815625hard25x250.0775279215625easy25x250.011240024096hard16x160.011240084096easy16x160.0012018729hard9x90.0012013729easy9x9timeclausesvarslevelsizeextended encoding99Experimental Results5314412621441176494665646656156251562540964096729729varsefficient encoding850411043303662411297986326788032678607509037509171232341232401177511770clausesstackstacktimetimetimetime17.480.210.090.000.00time5314412621441176494665646656156251562540964096729729varsminimal encoding63783464 24779088 8474410 2451400 2451380 563403 563417 92514 92520 8859 8854 clausesstackstacktimetimetimetime9.070.460.100.000.00timestack85060787531441easy81x81stack33048912262144easy64x641.4711305189117649easy49x490.67327176846656hard36x360.50327174846656easy36x360.2175277815625hard25x250.0775279215625easy25x250.011240024096hard16x160.011240084096easy16x160.0012018729hard9x90.0012013729easy9x9timeclausesvarslevelsizeextended encodingNo solution foundSolution found1010Motivations•Sudoku was regarded as SAT problemW Weber, A SAT-based Sudoku Solver, Nov. 2005.Lynce & Ouaknine, Sudoku as a SAT Problem, Jan. 2006. Extended encoding shows the best performance in our experiments• Problems in previous worksToo many clauses are generated (e.g. 85,056,804 clauses)Thus, large size puzzles are not solved The extended encoding must be optimized for large size puzzles•Our objectivesTo propose an optimization for the extended encoding1111Agenda• Introduction•Background and Previous Encodings• Optimized Encoding• Experimental Results• Conclusions1212Encoding•Kowledge compilation into a target language• Knowlede about SudokuA number appears once in each cellA number appears once in each rowA number appears once in each colA number appears once in each blockA pre-assigned numberrulesfactsCNFCNFCNFproblem knowlege91313Glance at CNF•CNF represented by boolean variables •Literal is a variable or its negation•Clause is a disjunction of literals•CNF is a conjunction of clauses x1, x2,...,xnx101¿xi=¿{¿ ¿¿¿x1=1¬x1∨x2∨¬x3x1=0 or x2=1 or x3=0 ¬x1∨x2∧ x1∨¬x3 x1=0 or x2=1and  x1=1 or x3=01414Variables•Each cell has one number from 1..N[1,1]=1 or [1,1]=2 or …… or [1,1]=NEach cell needs N boolean variables to consider all cases•Total number of variablesN3•Boolean variable name as a triple(r,c,v) iff [r,c] = v¬(r,c,v) iff [r,c] ≠ vN1515Set Notation•Indexed generalized disjunction and union operators•Re-definitions of clause and CNF using the operators¿i=1nCi={C1}∪...∪{Cn}={C1,...,Cn}C=¿i=1nli=l1∨...∨ln¿i=1n∪j=1mCij={C11,...,C1m,...,Cn1,...,Cnm}φ =¿i=1nCi={C1,...,Cn}¿i=1nli=l1∨...∨ln1616Cell Rule  CNFA number appears once in each cellThere is at least one number in each cellCelld=¿r=1N∪c=1N{¿v=1Nr ,c ,v}(definedness)There is at most one number in each cell(uniqueness)¬r ,c ,vi¿∨¬ r ,c ,vj¿¿Cellu=¿r =1N∪c=1N¿vi=1N−1¿vj=vi1N¿¿1717Row Rule  CNFEach number appears at least in each row(definedness)Each number appears at most in each row(uniqueness)Rowd=¿r=1N∪v=1N{¿c=1Nr ,c ,v}¬r ,ci¿,v,v∨¬r ,cj¿¿Rowu= ¿r =1N∪v=1N¿ci=1N− 1¿cj=ci1N¿¿A number appears once in each row1818Column Rule  CNFEach number appears at least in each column(definedness)Each number appears at most in each column(uniqueness)Cold=¿c=1N∪v=1N{¿r=1Nr ,c ,v}¬ri¿,c ,v ,c ,v ∨¬rj¿¿Colu=¿c=1N∪v=1N¿ri=1N− 1¿rj=ri1N¿¿A number appears once in each column1919Block Rule  CNFEach number appears at least in each block(definedness)Each number appears at most in each block(uniqueness)¿r=1subN¿¿subNc ,v¿c=1subNroffs¿subNr ,coffs¿¿Blockd=¿roffs=1subN¿coffs=1subN¿v=1N¿¿Blocku=¿roffs=1subN¿coffs=1subN¿v=1N¿r=1N¿c=r1N¬roffs∗subNr mod subN  ,coffs∗subNr mod subN  ,v¿ {¿ ∨¬roffs∗subNc mod subN  ,coffs∗subNc mod subN ,v}¿A number appears once in each block2020Pre-Assigned Fact  CNF3where k is a number of pre-assigned numbersAs a constant; the number is never changedIt can be represented as a unit clauseAssigned=¿i=1k{r ,c ,a∣∃1≤a≤N⋅[r ,c]=a}A pre-assigned number2121Previous