Optimal CNF Encoding for Representing Adjacency in Boolean Cardinality Constraints
Sa-Choun Park, Gihwon Kwon · Jeongbo gwahaghoe nonmunji. so'peuteuweeo mich eung'yong · 2008
In some applications of software engineering such as the verification of software model or embedded program, SAT solver is used. To practical use a SAT solver, a problem is encoded to a CNF formula, but because the formula has lower expressiveness than software models or source codes, optimal CNF encoding is required. In this paper, we propose optimal encoding techniques for the problem of Selecting adjacent among n objects, Through experimental results we show the proposed constraint is efficient and correct to solve Japanese puzzle. As we know, this paper is the first study about CNF encoding for adjacency in BCC.