Conjunctive normal form of Game Of life

Question

I want to use minisat to solve a 7 * 7 size game of life, to get the stable generations.

Here I simplify the rule of live and death: Von Neumann de rayon 1 The cell who has south, east and north neighbors alive will be alive. (xin : north neighbor; xie : east neighbors; xis : south neighbors) My formule But I don't know to to change this to CNF(Conjunctive normal form)

Can someone help me? T

Answer 1

The way I learned CNF, the "dead" formula is a single disjunctive term:

~xin V ~xie V ~xis

... which is simply the application of DeMorgan's theorem to the "live" case, which is already in CNF.

Remember, any expression whose operators are all disjuctions or all conjunctions, is already in both CNF and DNF.