كما كتبت لغز الكلمات المتقاطعة اليابانية في 4 ساعات

SAT- () (1, 2, 3),(-1, 2 ..), (True/False).

, , .

( , ); , , 8x8 = 64 , .

(1 2 3… 8) — 1 . — [1,2,3...8]
— (9… 16) ..

— 1 !
[ 1 2] ( — ). [-1,-2],[-1,-3] .

, , . , .

( ) — (1 2… 8) ( 1 2) (...). , — .

for cnter in range(4):
  sol = pycosat.solve(clauses)
  if isinstance(sol, list):
    print(sol)
    clauses.append([-x for x in sol]) #   -      
  else: #    - 
    return
#     ,    ,   .

, «-» ?

/ /, — . , .

[1] 3 , :
[X__],[_X_],[__X]
, ,
[1,-2,-3],[-1,2,-3],[-1,-2,3]

, …
:
[1 -2 -3] [-1, 2...] [...]

, . , . — , !

نقدم إدخال اختبار DNF: lstall = [[1،2،3]]. أي أننا نتوقع أن يكون [1،2،3] فقط (يتوافق مع السطر الكامل [XXX]) حلاً صالحًا. تقدم

المكتبة KNF: cnf = [[-1، -2، -3، 4]، [1 ، -4]، [2، -4]، [3، -4]]
هذا ليس واضحًا ولكنه مثير للاهتمام. حسنًا ، لنفترض أنني أصدقك ...

نطلب من pycosat إيجاد جميع حلول cnf:
[1، 2، 3، 4]
[1، 2، -3، -4]
[1، -2، -3، -4]
[1 ، -2، 3، -4]
[-1، -2، -3، -4]
[-1، -2، 3، -4]
[-1، 2، -3، -4]
[-1، 2 ، 3 ، -4]

بدلاً من المتوقع ، هناك ثمانية منهم! ماذا أفعل؟

, , 4 True. ?

: cnf2 = [[-1, -2, -3, 4], [1, -4], [2, -4], [3, -4], [4]]
pycosat cnf2:
1: [1, 2, 3, 4]

, , ! , , .
— !