Satisfiability modulo theory and binary puzzle

P.H. Utomo

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
90 Downloads (Pure)


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.
Original languageEnglish
Article number012057
Number of pages8
JournalJournal of Physics: Conference Series
Issue number1
Publication statusPublished - 2017
EventInternational Conference on Mathematics: Education, Theory and Application, 6–7 December 2016, Surakarta, Indonesia - Surakarta, Indonesia
Duration: 6 Dec 20167 Dec 2016


Dive into the research topics of 'Satisfiability modulo theory and binary puzzle'. Together they form a unique fingerprint.

Cite this