API tools faq
paste
Advertisement
partyboy1a

Tetris-test1.lua

partyboy1a
Jan 17th, 2013
77
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Lua 20.35 KB | None | 0 0
raw download clone embed print report
  1. dofile("SAT-solver-framework.lua")
  2.  
  3. rows = 20
  4. cols = 10
  5. steps = 15
  6.  
  7. vrows = rows + 4 + 4
  8. vcols = cols + 6
  9. vrow_offset = 4
  10. vcol_offset = 3
  11.  
  12. NewVar("playingfield", {steps + 1, vrows, vcols})
  13. NewVar("piece_type_bin", {steps, 3})
  14. NewVar("piece_type", {steps, 7})
  15. NewVar("new_block_path", {steps, vrows, vcols})
  16. NewVar("new_block_path_vcon", {steps, vrows, vcols})
  17. NewVar("final_col_bin", {steps,5})
  18. NewVar("final_col", {steps,vcols})
  19. NewVar("final_row_bin", {steps,5})
  20. NewVar("final_row", {steps,vrows})
  21. NewVar("intermediate_playingfield", {steps, vrows, vcols})
  22. NewVar("delete_row", {steps,vrows})
  23. NewVar("connected_deleted_rows", {steps, vrows, 4})
  24. NewVar("move_row_down_by", {steps, vrows, 4})
  25. NewVar("dont_move_row", {steps,vrows})
  26. local helper_count = 0
  27.  
  28. prefilled_field = {
  29. --row 1 to 5
  30. {0,0,0,0,0,0,0,0,0,0},
  31. {0,0,0,0,0,0,0,0,0,0},
  32. {0,0,0,0,0,0,0,0,0,0},
  33. {0,0,0,0,0,0,0,0,0,0},
  34. {0,0,0,0,0,0,0,0,0,0},
  35. --row 6 to 10
  36. {0,0,0,0,0,0,0,0,0,0},
  37. {0,0,0,0,0,0,0,0,0,0},
  38. {0,0,0,0,0,0,0,0,0,0},
  39. {0,0,0,0,0,0,0,0,0,0},
  40. {0,0,0,0,0,0,0,0,0,0},
  41. --row 11 to 15
  42. {0,0,0,0,0,0,0,0,0,0},
  43. {0,0,0,0,0,0,0,0,0,0},
  44. {0,0,0,0,0,0,0,0,0,0},
  45. {0,0,0,0,0,0,0,0,0,0},
  46. {0,0,1,1,0,0,0,0,0,0},
  47. --row 16 to 20
  48. {0,0,1,1,0,0,0,0,0,0},
  49. {1,1,0,0,1,1,0,0,1,1},
  50. {1,1,0,0,1,1,0,0,1,1},
  51. {0,0,0,0,0,0,1,1,0,0},
  52. {0,0,0,0,0,0,1,1,0,0}
  53. }
  54.  
  55. -- initialization for very first step
  56. for r = 1, rows do
  57.     local b
  58.     for c = 1, cols do 
  59.         if prefilled_field[r][c]==1 then b = true else b = false end
  60.         AddSimpleClause{Var.playingfield[1][r + vrow_offset][c + vcol_offset], b}
  61.     end
  62. end
  63.  
  64. for r = 1, vrows do
  65.     for c = 1, vcol_offset do
  66.         AddSimpleClause{Var.playingfield[1][r][c], true}
  67.     end
  68.     -- should be possible, but there are some bugs
  69.     -- left which do render this impossible...
  70.     -- for c = vcol_offset + 1, cols + vcol_offset do
  71.     --  AddSimpleClause{Var.playingfield[1][r][c], false}
  72.     -- end
  73.     for c = cols + vcol_offset + 1, vcols do
  74.         AddSimpleClause{Var.playingfield[1][r][c], true}
  75.     end
  76. end
  77. for r = rows + vrow_offset + 1, vrows do
  78.     for c = 1, vcols do
  79.         AddSimpleClause{Var.playingfield[1][r][c], true}
  80.     end
  81. end
  82.  
  83. -- now a REALLY large loop!!
  84. ------------------------------------------------------
  85. ------------------------------------------------------
  86. ------------------------------------------------------
  87. ----                                              ----
  88. ----                                              ----
  89. ----                                              ----
  90. ----                LARGE LOOP START              ----
  91. ----                                              ----
  92. ----                                              ----
  93. ----                                              ----
  94. ------------------------------------------------------
  95. ------------------------------------------------------
  96. ------------------------------------------------------
  97. for step = 1, steps do
  98.  
  99. AddSimpleClause{
  100.     Var.piece_type_bin[step][1], true,
  101.     Var.piece_type_bin[step][2], true,
  102.     Var.piece_type_bin[step][3], true
  103. }
  104.  
  105. for b1 = 0, 1 do for b2 = 0, 1 do for b3 = 0, 1 do
  106.     n = 4*b1 + 2*b2 + b3
  107.     if b1 == 1 then bool1 = true else bool1=false end
  108.     if b2 == 1 then bool2 = true else bool2=false end
  109.     if b3 == 1 then bool3 = true else bool3=false end
  110.     if n > 0 then
  111.         AddIfAndOnlyIfClause(
  112.             "ALL of", {
  113.                 Var.piece_type_bin[step][1], bool1,
  114.                 Var.piece_type_bin[step][2], bool2,
  115.                 Var.piece_type_bin[step][3], bool3
  116.             }, "if and only if",
  117.             "ALL of", {
  118.                 Var.piece_type[step][n], true
  119.             })
  120.     end
  121. end end end
  122.  
  123. for r = 1, vrows-1 do for c = 1, vcols do
  124.     AddIfAndOnlyIfClause(
  125.         "ALL of", {
  126.             Var.new_block_path[step][r][c], true,
  127.             Var.new_block_path[step][r+1][c], true
  128.         }, "if and only if",
  129.         "ALL of", {
  130.             Var.new_block_path_vcon[step][r][c], true
  131.         })
  132. end end
  133.  
  134. for r = vrow_offset + 1, rows + vrow_offset do
  135.     local p = {}
  136.     for c = 1, vcols do
  137.         p[#p + 1] = Var.new_block_path[step][r][c]
  138.         p[#p + 1] = true
  139.     end
  140.     local t = {}
  141.     for c = 1, vcols do
  142.         t[#t + 1] = Var.new_block_path_vcon[step][r-1][c]
  143.         t[#t + 1] = true
  144.     end
  145.    
  146.     AddIfThenClause("if ONE", p, "then ONE", t)
  147. end
  148.  
  149. AddSimpleClause{Var.new_block_path[step][vrow_offset + 1][vcol_offset + 5], true}
  150. for r = 1, vrows do
  151.     for left = 1, vcols - 2 do for middle = left + 1, vcols - 1 do for right = middle + 1, vcols do
  152.         AddSimpleClause{
  153.             Var.new_block_path[step][r][left], false,
  154.             Var.new_block_path[step][r][middle], true,
  155.             Var.new_block_path[step][r][right], false
  156.         }
  157.     end end end
  158. end
  159.  
  160. for b1 = 0, 1 do for b2 = 0, 1 do for b3 = 0, 1 do for b4 = 0, 1 do for b5 = 0, 1 do
  161.     if b1 == 1 then bool1 = true else bool1=false end
  162.     if b2 == 1 then bool2 = true else bool2=false end
  163.     if b3 == 1 then bool3 = true else bool3=false end  
  164.     if b4 == 1 then bool4 = true else bool4=false end
  165.     if b5 == 1 then bool5 = true else bool5=false end
  166.     c = 16*b1 + 8*b2 + 4*b3 + 2*b4 + b5
  167.     if c <= vcol_offset or c > cols + vcol_offset then
  168.         AddSimpleClause{
  169.             Var.final_col_bin[step][1], not bool1,
  170.             Var.final_col_bin[step][2], not bool2,
  171.             Var.final_col_bin[step][3], not bool3,
  172.             Var.final_col_bin[step][4], not bool4,
  173.             Var.final_col_bin[step][5], not bool5}
  174.     end
  175.     if c > 0 and c <= vcols then
  176.         AddIfAndOnlyIfClause(
  177.             "ALL of", {
  178.             Var.final_col_bin[step][1], bool1,
  179.             Var.final_col_bin[step][2], bool2,
  180.             Var.final_col_bin[step][3], bool3,
  181.             Var.final_col_bin[step][4], bool4,
  182.             Var.final_col_bin[step][5], bool5},
  183.             "if and only if",
  184.             "ALL of", {
  185.             Var.final_col[step][c], true})
  186.     end
  187. end end end end end
  188.  
  189. for b1 = 0, 1 do for b2 = 0, 1 do for b3 = 0, 1 do for b4 = 0, 1 do for b5 = 0, 1 do
  190.     if b1 == 1 then bool1 = true else bool1=false end
  191.     if b2 == 1 then bool2 = true else bool2=false end
  192.     if b3 == 1 then bool3 = true else bool3=false end  
  193.     if b4 == 1 then bool4 = true else bool4=false end
  194.     if b5 == 1 then bool5 = true else bool5=false end
  195.     r = 16*b1 + 8*b2 + 4*b3 + 2*b4 + b5
  196.     if r >= rows + vrow_offset + 1 or r <= vrow_offset then
  197.         AddSimpleClause{
  198.             Var.final_row_bin[step][1], not bool1,
  199.             Var.final_row_bin[step][2], not bool2,
  200.             Var.final_row_bin[step][3], not bool3,
  201.             Var.final_row_bin[step][4], not bool4,
  202.             Var.final_row_bin[step][5], not bool5}
  203.     end
  204.     if r >= vrow_offset + 1 and r <= rows + vrow_offset then AddIfAndOnlyIfClause(
  205.             "ALL of", {
  206.             Var.final_row_bin[step][1], bool1,
  207.             Var.final_row_bin[step][2], bool2,
  208.             Var.final_row_bin[step][3], bool3,
  209.             Var.final_row_bin[step][4], bool4,
  210.             Var.final_row_bin[step][5], bool5},
  211.             "if and only if",
  212.             "ALL of", {
  213.             Var.final_row[step][r], true})
  214.     end
  215. end end end end end
  216.  
  217.  
  218. AddSimpleClause{
  219.     Var.piece_type_bin[step][1], true,
  220.     Var.piece_type_bin[step][2], true,
  221.     Var.piece_type_bin[step][3], true
  222. }
  223.  
  224. for b1 = 0, 1 do for b2 = 0, 1 do for b3 = 0, 1 do
  225.     n = 4*b1 + 2*b2 + b3
  226.     if b1 == 1 then bool1 = true else bool1=false end
  227.     if b2 == 1 then bool2 = true else bool2=false end
  228.     if b3 == 1 then bool3 = true else bool3=false end
  229.     if n > 0 then
  230.         AddIfAndOnlyIfClause(
  231.             "ALL of", {
  232.                 Var.piece_type_bin[step][1], bool1,
  233.                 Var.piece_type_bin[step][2], bool2,
  234.                 Var.piece_type_bin[step][3], bool3
  235.             }, "if and only if",
  236.             "ALL of", {
  237.                 Var.piece_type[step][n], true
  238.             })
  239.     end
  240. end end end
  241.  
  242. for r = 1, vrows - 2 do for c = 1, vcols - 1 do
  243.     AddIfThenClause(
  244.         "if ALL", {
  245.             Var.final_row[step][r], true,
  246.             Var.final_col[step][c], true,
  247.         }, "then ALL", {
  248.             Var.new_block_path[step][r][c], true
  249.         })
  250.     AddIfThenClause(
  251.         "if ALL", {
  252.             Var.final_row[step][r], true,
  253.             Var.final_col[step][c], true,
  254.             Var.piece_type[step][1], true
  255.         }, "then ONE", {
  256.             Var.playingfield[step][r+2][c], true,
  257.             Var.playingfield[step][r+2][c+1], true
  258.         })
  259. end end
  260.  
  261. for r = 1, vrows-1 do for c = 1, vcols-1 do
  262.     AddIfThenClause(
  263.         "if ALL", {
  264.             Var.new_block_path[step][r][c], true,
  265.             Var.piece_type[step][1], true
  266.         }, "then ALL", {
  267.             Var.playingfield[step][r][c], false,
  268.             Var.playingfield[step][r][c+1], false,
  269.             Var.playingfield[step][r+1][c], false,
  270.             Var.playingfield[step][r+1][c+1], false
  271.         })
  272. end end
  273.  
  274. for r_aim = 1, vrows do for c_aim = 1, vcols do
  275.     local t = {Var.playingfield[step][r_aim][c_aim], true}
  276.     for r = vrow_offset + 1, rows + vrow_offset do for c = vcol_offset + 1, cols + vcol_offset do
  277.         if (r == r_aim and c == c_aim)
  278.         or (r == r_aim and c+1 == c_aim)
  279.         or (r+1 == r_aim and c == c_aim)
  280.         or (r+1 == r_aim and c+1 == c_aim)
  281.         then
  282.             helper_count = helper_count + 1
  283.             v = "h"..helper_count
  284.             NewVar(v)
  285.             AddIfAndOnlyIfClause(
  286.                 "ALL of", {
  287.                 Var[v], true},
  288.                 "if and only if",
  289.                 "ALL of", {
  290.                 Var.final_row[step][r], true,
  291.                 Var.final_col[step][c], true,
  292.                 Var.piece_type[step][1], true}
  293.             )
  294.             t[#t + 1] = Var[v]
  295.             t[#t + 1] = true
  296.         end
  297.     end end
  298.    
  299.     AddIfAndOnlyIfClause(
  300.         "ALL of",
  301.         {Var.intermediate_playingfield[step][r_aim][c_aim], true},
  302.         "if and only if",
  303.         "ONE of",
  304.         t
  305.     )
  306. end end
  307.  
  308. for r = 1, vrows do
  309.     if r >= vrow_offset + 1 and r <= rows + vrow_offset then
  310.         local t = {}
  311.    
  312.         for c = vcol_offset + 1, cols + vcol_offset do
  313.             t[#t+1] = Var.intermediate_playingfield[step][r][c]
  314.             t[#t+1] = true
  315.         end
  316.    
  317.         AddIfAndOnlyIfClause(
  318.             "ALL of", {
  319.             Var.delete_row[step][r], true},
  320.             "if and only if",
  321.             "ALL of",
  322.             t
  323.         )
  324.     else
  325.         AddSimpleClause{Var.delete_row[step][r], false}
  326.     end
  327. end
  328.  
  329. for r = vrow_offset + 1, vrows do
  330.     AddIfAndOnlyIfClause(
  331.         "ALL of", {
  332.         Var.connected_deleted_rows[step][r][1], true},
  333.         "if and only if",
  334.         "ALL of", {
  335.         Var.delete_row[step][r], true,
  336.         Var.delete_row[step][r-1], false}
  337.     )
  338.  
  339.     AddIfAndOnlyIfClause(
  340.         "ALL of", {
  341.         Var.connected_deleted_rows[step][r][2], true},
  342.         "if and only if",
  343.         "ALL of", {
  344.         Var.delete_row[step][r], true,
  345.         Var.delete_row[step][r-1], true,
  346.         Var.delete_row[step][r-2], false}
  347.     )
  348.  
  349.     AddIfAndOnlyIfClause(
  350.         "ALL of", {
  351.         Var.connected_deleted_rows[step][r][3], true},
  352.         "if and only if",
  353.         "ALL of", {
  354.         Var.delete_row[step][r], true,
  355.         Var.delete_row[step][r-1], true,
  356.         Var.delete_row[step][r-2], true,
  357.         Var.delete_row[step][r-3], false}
  358.     )
  359.  
  360.     AddIfAndOnlyIfClause(
  361.         "ALL of", {
  362.         Var.connected_deleted_rows[step][r][4], true},
  363.         "if and only if",
  364.         "ALL of", {
  365.         Var.delete_row[step][r], true,
  366.         Var.delete_row[step][r-1], true,
  367.         Var.delete_row[step][r-2], true,
  368.         Var.delete_row[step][r-3], true}
  369.     )
  370. end
  371.  
  372. -- that's REALLY complicated stuff here...
  373. for r = vrows, rows + vrow_offset + 1, -1 do
  374.     for k = 1, 4 do
  375.         AddSimpleClause{Var.move_row_down_by[step][r][k], false}
  376.     end
  377. end
  378. for r = rows + vrow_offset, vrow_offset + 1, -1 do
  379.     --1/0  
  380.     helper_count = helper_count + 1
  381.     v = "h"..helper_count
  382.     NewVar(v)
  383.  
  384.     AddIfAndOnlyIfClause(
  385.         "ALL of", {
  386.         Var[v], true},
  387.         "if and only if",
  388.         "ALL of",{
  389.         Var.move_row_down_by[step][r + 1][1], true,
  390.         Var.delete_row[step][r], false}
  391.     )
  392.  
  393.     t = {Var[v], true}
  394.  
  395.     -- 0/1
  396.     helper_count = helper_count + 1
  397.     v = "h"..helper_count
  398.     NewVar(v)
  399.  
  400.     AddIfAndOnlyIfClause(
  401.         "ALL of", {
  402.         Var[v], true},
  403.         "if and only if",
  404.         "ALL of",{
  405.         Var.move_row_down_by[step][r + 1][1], false,
  406.         Var.move_row_down_by[step][r + 1][2], false,
  407.         Var.move_row_down_by[step][r + 1][3], false,
  408.         Var.move_row_down_by[step][r + 1][4], false,
  409.         Var.connected_deleted_rows[step][r][1], true}
  410.     )
  411.  
  412.     t[#t + 1] = Var[v]
  413.     t[#t + 1] = true
  414.  
  415.     -- 1
  416.     AddIfAndOnlyIfClause(
  417.         "ALL of", {
  418.         Var.move_row_down_by[step][r][1], true},
  419.         "if and only if",
  420.         "ONE of",
  421.         t
  422.     )
  423.  
  424.     -- 2/0
  425.     helper_count = helper_count + 1
  426.     v = "h"..helper_count
  427.     NewVar(v)
  428.  
  429.     AddIfAndOnlyIfClause(
  430.         "ALL of", {
  431.         Var[v], true},
  432.         "if and only if",
  433.         "ALL of",{
  434.         Var.move_row_down_by[step][r + 1][2], true,
  435.         Var.delete_row[step][r], false}
  436.     )
  437.  
  438.     t = {Var[v], true}
  439.  
  440.     -- 1/1
  441.     helper_count = helper_count + 1
  442.     v = "h"..helper_count
  443.     NewVar(v)
  444.  
  445.     AddIfAndOnlyIfClause(
  446.         "ALL of", {
  447.         Var[v], true},
  448.         "if and only if",
  449.         "ALL of",{
  450.         Var.move_row_down_by[step][r + 1][1], true,
  451.         Var.connected_deleted_rows[step][r][1], true}
  452.     )
  453.  
  454.     t[#t + 1] = Var[v]
  455.     t[#t + 1] = true
  456.  
  457.     -- 0/2
  458.     helper_count = helper_count + 1
  459.     v = "h"..helper_count
  460.     NewVar(v)
  461.  
  462.     AddIfAndOnlyIfClause(
  463.         "ALL of", {
  464.         Var[v], true},
  465.         "if and only if",
  466.         "ALL of",{
  467.         Var.move_row_down_by[step][r + 1][1], false,
  468.         Var.move_row_down_by[step][r + 1][2], false,
  469.         Var.move_row_down_by[step][r + 1][3], false,
  470.         Var.move_row_down_by[step][r + 1][4], false,
  471.         Var.connected_deleted_rows[step][r][2], true}
  472.     )
  473.  
  474.     t[#t + 1] = Var[v]
  475.     t[#t + 1] = true
  476.  
  477.     -- 2
  478.     AddIfAndOnlyIfClause(
  479.         "ALL of", {
  480.         Var.move_row_down_by[step][r][2], true},
  481.         "if and only if",
  482.         "ONE of",
  483.         t
  484.     )
  485.  
  486.     -- 3/0
  487.     helper_count = helper_count + 1
  488.     v = "h"..helper_count
  489.     NewVar(v)
  490.  
  491.     AddIfAndOnlyIfClause(
  492.         "ALL of", {
  493.         Var[v], true},
  494.         "if and only if",
  495.         "ALL of",{
  496.         Var.move_row_down_by[step][r + 1][3], true,
  497.         Var.delete_row[step][r], false}
  498.     )
  499.  
  500.     t = {Var[v], true}
  501.  
  502.     -- 2/1
  503.     helper_count = helper_count + 1
  504.     v = "h"..helper_count
  505.     NewVar(v)
  506.  
  507.     AddIfAndOnlyIfClause(
  508.         "ALL of", {
  509.         Var[v], true},
  510.         "if and only if",
  511.         "ALL of",{
  512.         Var.move_row_down_by[step][r + 1][2], true,
  513.         Var.connected_deleted_rows[step][r][1], true}
  514.     )
  515.  
  516.     t[#t + 1] = Var[v]
  517.     t[#t + 1] = true
  518.  
  519.     -- 1/2
  520.     helper_count = helper_count + 1
  521.     v = "h"..helper_count
  522.     NewVar(v)
  523.  
  524.     AddIfAndOnlyIfClause(
  525.         "ALL of", {
  526.         Var[v], true},
  527.         "if and only if",
  528.         "ALL of",{
  529.         Var.move_row_down_by[step][r + 1][1], true,
  530.         Var.connected_deleted_rows[step][r][2], true}
  531.     )
  532.  
  533.     t[#t + 1] = Var[v]
  534.     t[#t + 1] = true
  535.  
  536.     -- 0/3
  537.     helper_count = helper_count + 1
  538.     v = "h"..helper_count
  539.     NewVar(v)
  540.  
  541.     AddIfAndOnlyIfClause(
  542.         "ALL of", {
  543.         Var[v], true},
  544.         "if and only if",
  545.         "ALL of",{
  546.         Var.move_row_down_by[step][r + 1][1], false,
  547.         Var.move_row_down_by[step][r + 1][2], false,
  548.         Var.move_row_down_by[step][r + 1][3], false,
  549.         Var.move_row_down_by[step][r + 1][4], false,
  550.         Var.connected_deleted_rows[step][r][3], true}
  551.     )
  552.  
  553.     t[#t + 1] = Var[v]
  554.     t[#t + 1] = true
  555.  
  556.     -- 3
  557.     AddIfAndOnlyIfClause(
  558.         "ALL of", {
  559.         Var.move_row_down_by[step][r][3], true},
  560.         "if and only if",
  561.         "ONE of",
  562.         t
  563.     )
  564.  
  565.     -- 4/0
  566.     helper_count = helper_count + 1
  567.     v = "h"..helper_count
  568.     NewVar(v)
  569.  
  570.     AddIfAndOnlyIfClause(
  571.         "ALL of", {
  572.         Var[v], true},
  573.         "if and only if",
  574.         "ALL of",{
  575.         Var.move_row_down_by[step][r + 1][4], true,
  576.         Var.delete_row[step][r], false}
  577.     )
  578.  
  579.     t = {Var[v], true}
  580.  
  581.     -- 3/1
  582.     helper_count = helper_count + 1
  583.     v = "h"..helper_count
  584.     NewVar(v)
  585.  
  586.     AddIfAndOnlyIfClause(
  587.         "ALL of", {
  588.         Var[v], true},
  589.         "if and only if",
  590.         "ALL of",{
  591.         Var.move_row_down_by[step][r + 1][3], true,
  592.         Var.connected_deleted_rows[step][r][1], true}
  593.     )
  594.  
  595.     t[#t + 1] = Var[v]
  596.     t[#t + 1] = true
  597.  
  598.     -- 2/2
  599.     helper_count = helper_count + 1
  600.     v = "h"..helper_count
  601.     NewVar(v)
  602.  
  603.     AddIfAndOnlyIfClause(
  604.         "ALL of", {
  605.         Var[v], true},
  606.         "if and only if",
  607.         "ALL of",{
  608.         Var.move_row_down_by[step][r + 1][2], true,
  609.         Var.connected_deleted_rows[step][r][2], true}
  610.     )
  611.  
  612.     t[#t + 1] = Var[v]
  613.     t[#t + 1] = true
  614.  
  615.     -- 1/3
  616.     helper_count = helper_count + 1
  617.     v = "h"..helper_count
  618.     NewVar(v)
  619.  
  620.     AddIfAndOnlyIfClause(
  621.         "ALL of", {
  622.         Var[v], true},
  623.         "if and only if",
  624.         "ALL of",{
  625.         Var.move_row_down_by[step][r + 1][1], true,
  626.         Var.connected_deleted_rows[step][r][3], true}
  627.     )
  628.  
  629.     t[#t + 1] = Var[v]
  630.     t[#t + 1] = true
  631.  
  632.     -- 0/4
  633.     helper_count = helper_count + 1
  634.     v = "h"..helper_count
  635.     NewVar(v)
  636.  
  637.     AddIfAndOnlyIfClause(
  638.         "ALL of", {
  639.         Var[v], true},
  640.         "if and only if",
  641.         "ALL of",{
  642.         Var.move_row_down_by[step][r + 1][1], false,
  643.         Var.move_row_down_by[step][r + 1][2], false,
  644.         Var.move_row_down_by[step][r + 1][3], false,
  645.         Var.move_row_down_by[step][r + 1][4], false,
  646.         Var.connected_deleted_rows[step][r][4], true}
  647.     )
  648.  
  649.     t[#t + 1] = Var[v]
  650.     t[#t + 1] = true
  651.  
  652.     -- 4
  653.     AddIfAndOnlyIfClause(
  654.         "ALL of", {
  655.         Var.move_row_down_by[step][r][4], true},
  656.         "if and only if",
  657.         "ONE of",
  658.         t
  659.     )
  660. end
  661.  
  662. for r = 1, vrows do
  663.     AddIfAndOnlyIfClause(
  664.         "ALL of",{
  665.         Var.dont_move_row[step][r], true},
  666.         "if and only if",
  667.         "ALL of",{
  668.         Var.move_row_down_by[step][r][1], false,
  669.         Var.move_row_down_by[step][r][2], false,
  670.         Var.move_row_down_by[step][r][3], false,
  671.         Var.move_row_down_by[step][r][4], false}
  672.     )
  673. end
  674.  
  675. for r = 1, vrow_offset do for c = 1, vcols do
  676.     AddIfAndOnlyIfClause(
  677.         "ALL of",{
  678.         Var.playingfield[step + 1][r][c], true},
  679.         "if and only if",
  680.         "ALL of",{
  681.         Var.playingfield[step][r][c], true}
  682.     )
  683. end end
  684. for r = rows + vrow_offset + 1, vrows do for c = 1, vcols do
  685.     AddIfAndOnlyIfClause(
  686.         "ALL of",{
  687.         Var.playingfield[step + 1][r][c], true},
  688.         "if and only if",
  689.         "ALL of",{
  690.         Var.playingfield[step][r][c], true}
  691.     )
  692. end end
  693. for r = vrow_offset + 1, rows + vrow_offset do for c = 1, vcols do
  694.     AddIfThenClause(
  695.         "if ALL", {
  696.         Var.intermediate_playingfield[step][r][c], true,
  697.         Var.dont_move_row[step][r], true},
  698.         "then ALL", {
  699.         Var.playingfield[step + 1][r][c], true}
  700.     )
  701.  
  702.     AddIfThenClause(
  703.         "if ALL", {
  704.         Var.intermediate_playingfield[step][r][c], false,
  705.         Var.dont_move_row[step][r], true},
  706.         "then ALL", {
  707.         Var.playingfield[step + 1][r][c], false}
  708.     )
  709.  
  710.     for downmovement = 1, 4 do
  711.         AddIfThenClause(
  712.             "if ALL", {
  713.             Var.intermediate_playingfield[step][r - downmovement][c], true,
  714.             Var.move_row_down_by[step][r][downmovement], true},
  715.             "then ALL", {
  716.             Var.playingfield[step + 1][r][c], true}
  717.         )
  718.  
  719.         AddIfThenClause(
  720.             "if ALL", {
  721.             Var.intermediate_playingfield[step][r - downmovement][c], false,
  722.             Var.move_row_down_by[step][r][downmovement], true},
  723.             "then ALL", {
  724.             Var.playingfield[step + 1][r][c], false}
  725.         )
  726.     end
  727. end end
  728.  
  729. --for testing: enforce a specific piece type
  730. AddSimpleClause{Var.piece_type[step][1], true}
  731.  
  732.  
  733. ------------------------------------------------------
  734. ------------------------------------------------------
  735. ------------------------------------------------------
  736. ----                                              ----
  737. ----                                              ----
  738. ----                                              ----
  739. ----                LARGE LOOP                    ----
  740. ----                    END                       ----
  741. ----                                              ----
  742. ----                                              ----
  743. ------------------------------------------------------
  744. ------------------------------------------------------
  745. ------------------------------------------------------
  746. end
  747.  
  748.  
  749. ---------------------------------------------------------------------
  750. ---------------------------------------------------------------------
  751. -- for testing...
  752. ---------------------------------------------------------------------
  753. ---------------------------------------------------------------------
  754.  
  755. -- enforce a specific type of block
  756.  
  757.  
  758.  
  759. -- force a specific destination field
  760. destination_field = {
  761. --row 1 to 5
  762. {0,0,0,0,0,0,0,0,0,0},
  763. {0,0,0,0,0,0,0,0,0,0},
  764. {0,0,0,0,0,0,0,0,0,0},
  765. {0,0,0,0,0,0,0,0,0,0},
  766. {0,0,0,0,0,0,0,0,0,0},
  767. --row 6 to 10
  768. {0,0,0,0,0,0,0,0,0,0},
  769. {0,0,0,0,0,0,0,0,0,0},
  770. {0,0,0,0,0,0,0,0,0,0},
  771. {0,0,0,0,0,0,0,0,0,0},
  772. {0,0,0,0,0,0,0,0,0,0},
  773. --row 11 to 15
  774. {0,0,0,0,0,0,0,0,0,0},
  775. {0,0,0,0,0,0,0,0,0,0},
  776. {0,0,0,0,0,0,0,0,0,0},
  777. {0,0,0,0,0,0,0,0,0,0},
  778. {0,0,0,0,0,0,0,0,0,0},
  779. --row 16 to 20
  780. {0,0,0,0,0,0,0,0,0,0},
  781. {0,0,0,0,0,0,0,0,0,0},
  782. {0,0,0,0,0,0,0,0,0,0},
  783. {0,0,0,0,0,0,0,0,0,0},
  784. {0,0,0,0,0,0,0,0,0,0}
  785. }
  786.  
  787. for r = 1, rows do for c = 1, cols do
  788.     local b
  789.     if destination_field[r][c] == 1 then b = true else b = false end
  790.     AddSimpleClause{Var.playingfield[steps+1][r + vrow_offset][c + vcol_offset], b}
  791. end end
  792. --]]
  793.  
  794. WriteSATfile()
  795. os.execute("minisat satfile.cnf solutionfile")
  796. ParseSolution()
  797. --PrintSolution()
  798.  
  799. if Sol.playingfield == nil then
  800.     print("no solution found!")
  801.     return
  802. end
  803.  
  804. for step = 1, steps do
  805.  
  806. for r = 1, vrows do
  807.     local s = ""
  808.     for c = 1, vcols do
  809.         if Sol.intermediate_playingfield[step][r][c] then
  810.             if Sol.playingfield[step][r][c] then
  811.                 s = s .. "[]"
  812.             elseif Sol.final_row[step][r] and Sol.final_col[step][c] then
  813.                 s = s .. "*!"
  814.             else
  815.                 s = s .. "@?"
  816.             end
  817.         elseif Sol.new_block_path[step][r][c] then
  818.             s = s .. "* "
  819.         else
  820.             s = s .. "  "
  821.         end
  822.     end
  823.    
  824.     s = s.."          "
  825.     for c = 1, vcols do
  826.         if Sol.playingfield[step+1][r][c] then
  827.             s = s .. "[]"
  828.         else
  829.             s = s .. "  "
  830.         end
  831.     end
  832.     print(s)
  833. end
  834. for r = 1, vrows do if Sol.final_row[step][r] then print("final row: "..r) end end
  835. for c = 1, vcols do if Sol.final_col[step][c] then print("final col: "..c) end end
  836. print()
  837. print()
  838.  
  839. end
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!