Fill-a-Pix Puzzle as a SAT Problem

Aye Myint Myat, Khine Khine Htwe, Nobuo Funabiki

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

Fill-a-Pix Puzzle is a Picture Logic Puzzle that has not been solved as a SAT Problem as well as there is no SAT Conjunctive Normal Form (CNF) Encoding Method to solve this puzzle yet. There are several practical SAT problems in various fields such as Artificial Intelligence (AI), Automatic Theorem Proving, Circuit Design, etc. Fill-a-Pix puzzle is also one of the SAT problems. This research proposes the SAT CNF Encoding Method to solve Fill-a-Pix Puzzle as a SAT Problem using SAT Solvers. The proposed SAT CNF Encoding Method will be executed on different standard SAT solvers - MiniSAT, CryptoMiniSAT and RSAT. The evaluation is presented regarding the CPU Execution Times of each solver for executing the proposed SAT CNF Encoding, the Number of Variables and Clauses produced by the proposed SAT CNF Encoding as well as the Comparison of Fill-a-Pix Puzzle with the other Similar Puzzles such as Sudoku and Slitherlink based on the Number of Variables and Clauses produced by the proposed SAT CNF Encoding when executing Puzzle Sizes above 50 × 50.

Original languageEnglish
Title of host publication2019 International Conference on Advanced Information Technologies, ICAIT 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages244-249
Number of pages6
ISBN (Electronic)9781728151731
DOIs
Publication statusPublished - Nov 2019
Externally publishedYes
Event2019 International Conference on Advanced Information Technologies, ICAIT 2019 - Yangon, Myanmar
Duration: Nov 6 2019Nov 7 2019

Publication series

Name2019 International Conference on Advanced Information Technologies, ICAIT 2019

Conference

Conference2019 International Conference on Advanced Information Technologies, ICAIT 2019
Country/TerritoryMyanmar
CityYangon
Period11/6/1911/7/19

Keywords

  • CryptoMiniSAT
  • Fill-a-Pix Puzzle
  • MiniSAT
  • RSAT
  • SAT CNF Encoding

ASJC Scopus subject areas

  • Computer Vision and Pattern Recognition
  • Signal Processing
  • Modelling and Simulation
  • Artificial Intelligence
  • Computer Networks and Communications
  • Computer Science Applications

Fingerprint

Dive into the research topics of 'Fill-a-Pix Puzzle as a SAT Problem'. Together they form a unique fingerprint.

Cite this