Satisfiability modulo theory and binary puzzle

[摘要] The binary puzzle is a sudoku-like puzzle with values in each cell taken from the set {0, 1}. We look at the mathematical theory behind it. A solved binary puzzle is an n × n binary array where n is even that satisfies the following conditions: (1) No three consecutive ones and no three consecutive zeros in each row and each column, (2) Every row and column is balanced, that is the number of ones and zeros must be equal in each row and in each column, (3) Every two rows and every two columns must be distinct. The binary puzzle had been proven to be an NP-complete problem [5]. Research concerning the satisfiability of formulas with respect to some background theory is called satisfiability modulo theory (SMT). An SMT solver is an extension of a satisfiability (SAT) solver. The notion of SMT can be used for solving various problem in mathematics and industries such as formula verification and operation research [1, 7]. In this paper we apply SMT to solve binary puzzles. In addition, we do an experiment in solving different sizes and different number of blanks. We also made comparison with two other approaches, namely by a SAT solver and exhaustive search.

[发布机构] Department of Mathematics and Computer Science, Eindhoven University of Technology, Faculty of Mathematics and Natural Science, Sebelas Maret University, Indonesia^1

[效力级别] 教育 [学科分类] 发展心理学和教育心理学

[关键词] Background theory;Consecutive ones;Different sizes;Mathematical theory;Operation research;Satisfiability;Satisfiability modulo Theories;Satisfiability solvers