Abstract
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.
(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.
| Original language | English |
|---|---|
| Article number | 012057 |
| Number of pages | 8 |
| Journal | Journal of Physics: Conference Series |
| Volume | 855 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 2017 |
| Event | International Conference on Mathematics: Education, Theory and Application, 6–7 December 2016, Surakarta, Indonesia - Surakarta, Indonesia Duration: 6 Dec 2016 → 7 Dec 2016 http://iopscience.iop.org/issue/1742-6596/855/1 |