ALGORITHMIC APPROACH FOR OPTIMIZATION OF SAT ENCODING OF SUDOKU PUZZLE
Keywords:
Non-deterministic Polynomial Complete, Satisfiability problem, Sudoku puzzle, SAT Clauses, SAT Solver.Abstract
Sudoku puzzle is an eminent Non-deterministic Polynomial Complete (NPC) problem thathas been achieved remarkable contribution in different research fields. SAT formulation of
Sudoku puzzle produces huge number of SAT Clauses. It is noticed that SAT solving time is
directly proportional to number of SAT Clauses. Therefore, we have performed the
optimization of SAT formula before solving with the use of pre-assigned numbers that are
already given in Sudoku puzzle. In this way, we designed an algorithm minSAT to optimize
the SAT clauses generated from SAT formulation of Sudoku puzzle. Our approach for
optimizing the SAT formula provides a way to improve the SAT solving time.
References
Claessen Koen, et.al., 2008. SAT-Solving in Practice. IEEE 9th International Conference on
Discrete Event Systems, 61-67.
Joao Marques-Silva, 2008. Practical applications of Boolean Satisfiability. IEEE
International Workshop on Discrete Event Systems, 74-80.
Rai Deepika, Chaudhari N.S., Ingle M., 2010. SAT Based Algorithmic Approach for Sudoku
puzzle. International Journal of Computer Engineering & Technology, 9, 6, 38-45.
Clause Elimination. International Conference on Theory and Applications of Satisfiability
Testing, Springer, LNCS, 3569, 61-75.
MJH Heule, et.al., 2011. Efficient CNF Simplification based on Binary Implication Graphs.
International Conference on Theory and Applications of Satisfiability Testing-SAT,
Springer, LNCS, 6695, 201-212.
Osama Muhammad and Anton Wijs, 2012. Parallel SAT simplification on GPU
architectures. International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Springer, Cham, 21-40.
Heule Marijn, et.al., 2011. Clause elimination for SAT and QSAT. Journal of Artificial
Intelligence Research, 53, 127-168.
Published
Issue
Section
License
Submission Preparation ChecklistSubmission Preparation Checklist
Before proceeding with your submission, please ensure that you have completed the following checklist. All items on the list must have a checkmark before you can submit your manuscript:
