# satisfiability – 3SAT formula with only positive variables

Suppose I'm trying to reduce grid generation to 3-SAT

Here is my attempt to create a SAT instance for an algorithm that creates grids. The grid follows the permuted pattern. I'm trying to represent the pattern with a formula.

(1∨𝑥9∨𝑥8) (2∨𝑥1∨𝑦9) (3∨𝑥2∨𝑦1) (𝑙4∨𝑥3∨𝑦2) (5∨𝑥4∨𝑦3) (6∨𝑥5∨𝑦4) (𝑙7 ∨𝑦6∨𝑦5) ( ∨𝑥8∨𝑥7∨𝑦6) (9∨𝑥8∨𝑦7) (𝑙1∨𝑥9∨𝑦8) (2∨𝑥1∨𝑦9)

l = [8, 5, 9, 6, 1, 2, 4, 3, 7]

``````[5, 9, 6, 1, 2, 4, 3, 7, 8]-l1
[9, 6, 1, 2, 4, 3, 7, 8, 5]-l2
[6, 1, 2, 4, 3, 7, 8, 5, 9]-L3
[1, 2, 4, 3, 7, 8, 5, 9, 6]L4
[2, 4, 3, 7, 8, 5, 9, 6, 1]-L5
[4, 3, 7, 8, 5, 9, 6, 1, 2]-L6
[3, 7, 8, 5, 9, 6, 1, 2, 4]-L7
[7, 8, 5, 9, 6, 1, 2, 4, 3]-l8
[8, 5, 9, 6, 1, 2, 4, 3, 7]-l9
``````

x = [5, 9, 6, 1, 2, 4, 3, 7, 8]

``````[9, 6, 1, 2, 4, 3, 7, 8, 5]-x1
[6, 1, 2, 4, 3, 7, 8, 5, 9]-x2
[1, 2, 4, 3, 7, 8, 5, 9, 6]-x3
[2, 4, 3, 7, 8, 5, 9, 6, 1]-x4
[4, 3, 7, 8, 5, 9, 6, 1, 2]-X5
[3, 7, 8, 5, 9, 6, 1, 2, 4]-x6
[7, 8, 5, 9, 6, 1, 2, 4, 3]-X7
[8, 5, 9, 6, 1, 2, 4, 3, 7]-x8
[5, 9, 6, 1, 2, 4, 3, 7, 8]-X9
``````

y = [9, 6, 1, 2, 4, 3, 7, 8, 5]

``````[6, 1, 2, 4, 3, 7, 8, 5, 9]-y1
[1, 2, 4, 3, 7, 8, 5, 9, 6]-y2
[2, 4, 3, 7, 8, 5, 9, 6, 1]-y3
[4, 3, 7, 8, 5, 9, 6, 1, 2]-Y 4
[3, 7, 8, 5, 9, 6, 1, 2, 4]-y5
[7, 8, 5, 9, 6, 1, 2, 4, 3]-y6
[8, 5, 9, 6, 1, 2, 4, 3, 7]-y7
[5, 9, 6, 1, 2, 4, 3, 7, 8]-y8
[9, 6, 1, 2, 4, 3, 7, 8, 5]-y9
``````

(l1 x9 y8) (l2 x1 y9)

``````l1 = [5, 9, 6, 1, 2, 4, 3, 7, 8]

x9 = [5, 9, 6, 1, 2, 4, 3, 7, 8]

y8 = [5, 9, 6, 1, 2, 4, 3, 7, 8]
``````

The formula should always generate this grid.

``````    [5, 9, 6, 1, 2, 4, 3, 7, 8]-l1
[9, 6, 1, 2, 4, 3, 7, 8, 5]-l2
[6, 1, 2, 4, 3, 7, 8, 5, 9]-L3
[1, 2, 4, 3, 7, 8, 5, 9, 6]L4
[2, 4, 3, 7, 8, 5, 9, 6, 1]-L5
[4, 3, 7, 8, 5, 9, 6, 1, 2]-L6
[3, 7, 8, 5, 9, 6, 1, 2, 4]-L7
[7, 8, 5, 9, 6, 1, 2, 4, 3]-l8
[8, 5, 9, 6, 1, 2, 4, 3, 7]-l9
``````

Is this a correct 3-SAT reduction of the hypothetical problem?

Would not I need to extend it?