%------------------------------------------------------------------------------ % File : PUZ005-0 : TPTP v7.2.0. Released v3.2.0. % Domain : Puzzles (Sudoku) % Axioms : Sudoku axioms % Version : [Bau06] axioms : Especial. % English : % Refs : [Bau06] Baumgartner (2006), Email to G. Sutcliffe % Source : [Bau06] % Names : % Status : Satisfiable % Syntax : Number of clauses : 79 ( 4 non-Horn; 54 unit; 79 RR) % Number of atoms : 161 ( 39 equality) % Maximal clause size : 11 ( 2 average) % Number of predicates : 4 ( 0 propositional; 1-3 arity) % Number of functors : 2 ( 1 constant; 0-1 arity) % Number of variables : 75 ( 0 singleton) % Maximal term depth : 10 ( 3 average) % SPC : % Comments : %------------------------------------------------------------------------------ %----Regarding equality, (un)equality is syntactic (un)equality %----The domain is the numbers from n1 to n9. cnf(dom_1,axiom, ( dom(s(n0)) )). cnf(dom_2,axiom, ( dom(s(s(n0))) )). cnf(dom_3,axiom, ( dom(s(s(s(n0)))) )). cnf(dom_4,axiom, ( dom(s(s(s(s(n0))))) )). cnf(dom_5,axiom, ( dom(s(s(s(s(s(n0)))))) )). cnf(dom_6,axiom, ( dom(s(s(s(s(s(s(n0))))))) )). cnf(dom_7,axiom, ( dom(s(s(s(s(s(s(s(n0)))))))) )). cnf(dom_8,axiom, ( dom(s(s(s(s(s(s(s(s(n0))))))))) )). cnf(dom_9,axiom, ( dom(s(s(s(s(s(s(s(s(s(n0)))))))))) )). %----The domain elements are pairwise different; %----This is the negative part of equality. cnf(dom_1_not_2,axiom, ( s(n0) != s(s(n0)) )). cnf(dom_1_not_3,axiom, ( s(n0) != s(s(s(n0))) )). cnf(dom_1_not_4,axiom, ( s(n0) != s(s(s(s(n0)))) )). cnf(dom_1_not_5,axiom, ( s(n0) != s(s(s(s(s(n0))))) )). cnf(dom_1_not_6,axiom, ( s(n0) != s(s(s(s(s(s(n0)))))) )). cnf(dom_1_not_7,axiom, ( s(n0) != s(s(s(s(s(s(s(n0))))))) )). cnf(dom_1_not_8,axiom, ( s(n0) != s(s(s(s(s(s(s(s(n0)))))))) )). cnf(dom_1_not_9,axiom, ( s(n0) != s(s(s(s(s(s(s(s(s(n0))))))))) )). cnf(dom_2_not_3,axiom, ( s(s(n0)) != s(s(s(n0))) )). cnf(dom_2_not_4,axiom, ( s(s(n0)) != s(s(s(s(n0)))) )). cnf(dom_2_not_5,axiom, ( s(s(n0)) != s(s(s(s(s(n0))))) )). cnf(dom_2_not_6,axiom, ( s(s(n0)) != s(s(s(s(s(s(n0)))))) )). cnf(dom_2_not_7,axiom, ( s(s(n0)) != s(s(s(s(s(s(s(n0))))))) )). cnf(dom_2_not_8,axiom, ( s(s(n0)) != s(s(s(s(s(s(s(s(n0)))))))) )). cnf(dom_2_not_9,axiom, ( s(s(n0)) != s(s(s(s(s(s(s(s(s(n0))))))))) )). cnf(dom_3_not_4,axiom, ( s(s(s(n0))) != s(s(s(s(n0)))) )). cnf(dom_3_not_5,axiom, ( s(s(s(n0))) != s(s(s(s(s(n0))))) )). cnf(dom_3_not_6,axiom, ( s(s(s(n0))) != s(s(s(s(s(s(n0)))))) )). cnf(dom_3_not_7,axiom, ( s(s(s(n0))) != s(s(s(s(s(s(s(n0))))))) )). cnf(dom_3_not_8,axiom, ( s(s(s(n0))) != s(s(s(s(s(s(s(s(n0)))))))) )). cnf(dom_3_not_9,axiom, ( s(s(s(n0))) != s(s(s(s(s(s(s(s(s(n0))))))))) )). cnf(dom_4_not_5,axiom, ( s(s(s(s(n0)))) != s(s(s(s(s(n0))))) )). cnf(dom_4_not_6,axiom, ( s(s(s(s(n0)))) != s(s(s(s(s(s(n0)))))) )). cnf(dom_4_not_7,axiom, ( s(s(s(s(n0)))) != s(s(s(s(s(s(s(n0))))))) )). cnf(dom_4_not_8,axiom, ( s(s(s(s(n0)))) != s(s(s(s(s(s(s(s(n0)))))))) )). cnf(dom_4_not_9,axiom, ( s(s(s(s(n0)))) != s(s(s(s(s(s(s(s(s(n0))))))))) )). cnf(dom_5_not_6,axiom, ( s(s(s(s(s(n0))))) != s(s(s(s(s(s(n0)))))) )). cnf(dom_5_not_7,axiom, ( s(s(s(s(s(n0))))) != s(s(s(s(s(s(s(n0))))))) )). cnf(dom_5_not_8,axiom, ( s(s(s(s(s(n0))))) != s(s(s(s(s(s(s(s(n0)))))))) )). cnf(dom_5_not_9,axiom, ( s(s(s(s(s(n0))))) != s(s(s(s(s(s(s(s(s(n0))))))))) )). cnf(dom_6_not_7,axiom, ( s(s(s(s(s(s(n0)))))) != s(s(s(s(s(s(s(n0))))))) )). cnf(dom_6_not_8,axiom, ( s(s(s(s(s(s(n0)))))) != s(s(s(s(s(s(s(s(n0)))))))) )). cnf(dom_6_not_9,axiom, ( s(s(s(s(s(s(n0)))))) != s(s(s(s(s(s(s(s(s(n0))))))))) )). cnf(dom_7_not_8,axiom, ( s(s(s(s(s(s(s(n0))))))) != s(s(s(s(s(s(s(s(n0)))))))) )). cnf(dom_7_not_9,axiom, ( s(s(s(s(s(s(s(n0))))))) != s(s(s(s(s(s(s(s(s(n0))))))))) )). cnf(dom_8_not_9,axiom, ( s(s(s(s(s(s(s(s(n0)))))))) != s(s(s(s(s(s(s(s(s(n0))))))))) )). %----Generator: %----At least one number in each field %----el(I,J,X) means on row I, column J is the natural number X cnf(number_in_each_position,axiom, ( ~ dom(I) | ~ dom(J) | el(I,J,s(n0)) | el(I,J,s(s(n0))) | el(I,J,s(s(s(n0)))) | el(I,J,s(s(s(s(n0))))) | el(I,J,s(s(s(s(s(n0)))))) | el(I,J,s(s(s(s(s(s(n0))))))) | el(I,J,s(s(s(s(s(s(s(n0)))))))) | el(I,J,s(s(s(s(s(s(s(s(n0))))))))) | el(I,J,s(s(s(s(s(s(s(s(s(n0)))))))))) )). %----Restriction: %----No two same numbers on a field (dual of previous) %----This is in fact redundant in combination of the previous generator and %----already one of the following constraints cnf(only_one_number_in_each_position,axiom, ( ~ el(I,J,X) | ~ el(I,J,X1) | X = X1 )). %----Restriction: %----No number occurs twice in a row: %----(J = J1) :- el(I,J,X), el(I,J1,X1), (X = X1). %----slightly simpler: cnf(no_duplicates_in_a_row,axiom, ( ~ el(I,J,X) | ~ el(I,J1,X) | J = J1 )). %----Restriction: %----No number occurs twice in a column: cnf(no_duplicates_in_a_column,axiom, ( ~ el(I,J,X) | ~ el(I1,J,X) | I = I1 )). %----where different(I,J,I1,J1) means that the field elements at %----(I,J) and at (I1,J1) are different %---- different(I,J,I1,J1) -> % ( el(I,J,X) & el(I1,J1,X1) -> -(X = X1)). %----Now, the n3x3 subfields. cnf(subfield_1_1,hypothesis, ( subfield(s(n0),s(n0)) )). cnf(subfield_1_4,hypothesis, ( subfield(s(n0),s(s(s(s(n0))))) )). cnf(subfield_1_7,hypothesis, ( subfield(s(n0),s(s(s(s(s(s(s(n0)))))))) )). cnf(subfield_4_1,hypothesis, ( subfield(s(s(s(s(n0)))),s(n0)) )). cnf(subfield_4_4,hypothesis, ( subfield(s(s(s(s(n0)))),s(s(s(s(n0))))) )). cnf(subfield_4_7,hypothesis, ( subfield(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))) )). cnf(subfield_7_1,hypothesis, ( subfield(s(s(s(s(s(s(s(n0))))))),s(n0)) )). cnf(subfield_7_4,hypothesis, ( subfield(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0))))) )). cnf(subfield_7_7,hypothesis, ( subfield(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(n0)))))))) )). %----Each subfield contains no number twice: %----Note: It is sufficient to specify only along the diagonals, %----as along the row and columns the general row and column restrictions %----above subsume the corresponding ones for the subfields. %----Notice we do a little bit of integer arithmetic (+1 and +2) to talk %----about the fields in a given subfield. %----Perhaps more readable formulation of the axioms is like %----subfield(I,J) -> %---- ( el(I,J,X) & el(s(I),s(J),X1) -> -(X = X1)). %----which translates to cnf(subfield_diagonal_1,hypothesis, ( ~ subfield(I,J) | ~ el(I,J,X) | ~ el(s(I),s(J),X) )). cnf(subfield_diagonal_2,hypothesis, ( ~ subfield(I,J) | ~ el(I,J,X) | ~ el(s(I),s(s(J)),X) )). cnf(subfield_diagonal_3,hypothesis, ( ~ subfield(I,J) | ~ el(I,J,X) | ~ el(s(s(I)),s(J),X) )). cnf(subfield_diagonal_4,hypothesis, ( ~ subfield(I,J) | ~ el(I,J,X) | ~ el(s(s(I)),s(s(J)),X) )). cnf(subfield_diagonal_5,hypothesis, ( ~ subfield(I,J) | ~ el(I,s(J),X) | ~ el(s(I),J,X) )). cnf(subfield_diagonal_6,hypothesis, ( ~ subfield(I,J) | ~ el(I,s(J),X) | ~ el(s(I),s(s(J)),X) )). cnf(subfield_diagonal_7,hypothesis, ( ~ subfield(I,J) | ~ el(I,s(J),X) | ~ el(s(s(I)),J,X) )). cnf(subfield_diagonal_8,hypothesis, ( ~ subfield(I,J) | ~ el(I,s(J),X) | ~ el(s(s(I)),s(s(J)),X) )). cnf(subfield_diagonal_9,hypothesis, ( ~ subfield(I,J) | ~ el(I,s(s(J)),X) | ~ el(s(I),J,X) )). cnf(subfield_diagonal_10,hypothesis, ( ~ subfield(I,J) | ~ el(I,s(s(J)),X) | ~ el(s(I),s(J),X) )). cnf(subfield_diagonal_11,hypothesis, ( ~ subfield(I,J) | ~ el(I,s(s(J)),X) | ~ el(s(s(I)),J,X) )). cnf(subfield_diagonal_12,hypothesis, ( ~ subfield(I,J) | ~ el(I,s(s(J)),X) | ~ el(s(s(I)),s(J),X) )). cnf(subfield_diagonal_13,hypothesis, ( ~ subfield(I,J) | ~ el(s(I),J,X) | ~ el(s(s(I)),s(J),X) )). cnf(subfield_diagonal_14,hypothesis, ( ~ subfield(I,J) | ~ el(s(I),J,X) | ~ el(s(s(I)),s(s(J)),X) )). cnf(subfield_diagonal_15,hypothesis, ( ~ subfield(I,J) | ~ el(s(I),s(J),X) | ~ el(s(s(I)),J,X) )). cnf(subfield_diagonal_16,hypothesis, ( ~ subfield(I,J) | ~ el(s(I),s(J),X) | ~ el(s(s(I)),s(s(J)),X) )). cnf(subfield_diagonal_17,hypothesis, ( ~ subfield(I,J) | ~ el(s(I),s(s(J)),X) | ~ el(s(s(I)),J,X) )). cnf(subfield_diagonal_18,hypothesis, ( ~ subfield(I,J) | ~ el(s(I),s(s(J)),X) | ~ el(s(s(I)),s(J),X) )). %----Some additional constraints. They are redundant but help %----to solve the Sudoku in a deterministic way quite often. %----I think the underlying heuristics used by people is called %----'crosshatching'. %----In every subfield, every value must be put somewhere cnf(value_somewhere_in_subfield,hypothesis, ( ~ subfield(I,J) | ~ dom(X) | el(I,J,X) | el(I,s(J),X) | el(I,s(s(J)),X) | el(s(I),J,X) | el(s(I),s(J),X) | el(s(I),s(s(J)),X) | el(s(s(I)),J,X) | el(s(s(I)),s(J),X) | el(s(s(I)),s(s(J)),X) )). %----In every row, every value must be put somewhere cnf(value_somewhere_in_row,hypothesis, ( ~ dom(I) | ~ dom(X) | el(I,s(n0),X) | el(I,s(s(n0)),X) | el(I,s(s(s(n0))),X) | el(I,s(s(s(s(n0)))),X) | el(I,s(s(s(s(s(n0))))),X) | el(I,s(s(s(s(s(s(n0)))))),X) | el(I,s(s(s(s(s(s(s(n0))))))),X) | el(I,s(s(s(s(s(s(s(s(n0)))))))),X) | el(I,s(s(s(s(s(s(s(s(s(n0))))))))),X) )). %----In every column, every value must be put somewhere cnf(value_somewhere_in_column,hypothesis, ( ~ dom(J) | ~ dom(X) | el(s(n0),J,X) | el(s(s(n0)),J,X) | el(s(s(s(n0))),J,X) | el(s(s(s(s(n0)))),J,X) | el(s(s(s(s(s(n0))))),J,X) | el(s(s(s(s(s(s(n0)))))),J,X) | el(s(s(s(s(s(s(s(n0))))))),J,X) | el(s(s(s(s(s(s(s(s(n0)))))))),J,X) | el(s(s(s(s(s(s(s(s(s(n0))))))))),J,X) )). %------------------------------------------------------------------------------