Apa prinsip matematika / komputasi di balik game ini?

Anak-anak saya memiliki permainan menyenangkan ini yang disebut Spot It! Kendala permainan (seperti yang saya bisa jelaskan) adalah:

• Ini adalah setumpuk 55 kartu
• Pada masing-masing kartu terdapat 8 gambar unik (yaitu kartu tidak dapat memiliki 2 gambar yang sama)
• Diberikan 2 kartu yang dipilih dari geladak, ada 1 dan hanya 1 gambar yang cocok .
• Gambar yang cocok mungkin diskalakan secara berbeda pada kartu yang berbeda tetapi itu hanya untuk membuat permainan lebih sulit (yaitu pohon kecil masih cocok dengan pohon yang lebih besar)

Prinsip permainan ini adalah: membalikkan 2 kartu dan siapa pun yang pertama kali mengambil gambar yang cocok mendapat poin.

Berikut gambar untuk klarifikasi:

(Contoh: Anda dapat melihat dari 2 kartu terbawah di atas bahwa gambar yang cocok adalah dinosaurus hijau. Di antara gambar kanan bawah dan kanan tengah, itu adalah kepala badut.)

Saya mencoba memahami yang berikut:

1. Berapa jumlah minimum gambar berbeda yang diperlukan untuk memenuhi kriteria ini dan bagaimana Anda menentukan ini?

2. Menggunakan pseudocode (atau Ruby), bagaimana Anda menghasilkan 55 kartu permainan dari berbagai gambar N (di mana N adalah angka minimum dari pertanyaan 1)?

Memperbarui:

Gambar memang muncul lebih dari dua kali per dek (bertentangan dengan apa yang beberapa orang duga). Lihat gambar 3 kartu ini, masing-masing dengan petir:

Geometri Proyektif Hingga

The aksioma dari proyektif (pesawat) geometri yang sedikit berbeda dari geometri Euclidean:

• Setiap dua titik memiliki tepat satu garis yang melewati mereka (ini sama).
• Setiap dua baris bertemu tepat satu titik (ini sedikit berbeda dari Euclid).

Sekarang, tambahkan "terbatas" ke dalam sup dan Anda memiliki pertanyaan:

Bisakah kita memiliki geometri hanya dengan 2 poin? Dengan 3 poin? Dengan 4? Dengan 7?

Masih ada pertanyaan terbuka tentang masalah ini, tetapi kami tahu ini:

• Jika ada geometri dengan Qtitik, maka Q = n^2 + n + 1dan ndisebut ordergeometri.
• Ada n+1poin di setiap baris.
• Dari setiap titik, berikan n+1garis persis .

• Jumlah total garis juga Q.

• Dan akhirnya, jika nprima, maka memang ada geometri urutan n.

Apa hubungannya dengan teka-teki, orang mungkin bertanya.

Masukan cardbukannya pointdan picturebukan linedan aksioma menjadi:

• Setiap dua kartu memiliki tepat satu gambar yang sama.
• Untuk setiap dua gambar ada tepat satu kartu yang memiliki keduanya.

Sekarang, mari n=7kita ambil dan kita memiliki order-7geometri terbatas Q = 7^2 + 7 + 1. Itu membuat Q=57garis (gambar) dan Q=57poin (kartu). Saya kira pembuat puzzle memutuskan bahwa angka 55 lebih bulat dari 57 dan meninggalkan 2 kartu.

Kami juga mendapatkan n+1 = 8, jadi dari setiap titik (kartu), 8 baris berlalu (8 gambar muncul) dan setiap baris (gambar) memiliki 8 poin (muncul dalam 8 kartu).

Berikut ini adalah representasi dari bidang (geometri) proyektif terbatas hingga paling terkenal dengan 7 poin, yang dikenal sebagai Fano Plane , disalin dari Noelle Evans - Finite Geometry Problem Page

Saya sedang berpikir untuk membuat gambar yang menjelaskan bagaimana pesawat order-2 di atas dapat dibuat puzzle yang sama dengan 7 kartu dan 7 gambar, tetapi kemudian tautan dari pertanyaan kembar math.exchange memiliki diagram seperti itu: Dobble-et- la-geometrie-finie

Bagi mereka yang kesulitan menggambar geometri bidang proyektif dengan 57 poin, ada cara yang sangat bagus dan intuitif untuk membangun permainan dengan 57 kartu dan 57 simbol (berdasarkan jawaban oleh Yuval Filmus untuk pertanyaan ini ):

1. Untuk kartu dengan 8 simbol, buat 7x7 kisi simbol unik.
2. Tambahkan 8 simbol tambahan untuk "lereng" dari 0 hingga 6, ditambah satu untuk lereng tanpa batas.
3. Setiap kartu adalah garis pada grid (7 simbol) ditambah satu simbol dari kemiringan yang ditetapkan untuk kemiringan garis. Garis memiliki offset (yaitu titik awal di sebelah kiri), dan kemiringan (yaitu berapa banyak simbol untuk naik untuk setiap langkah ke kanan). Ketika garis meninggalkan grid di bagian atas, masukkan kembali di bagian bawah. Lihat contoh gambar ini (gambar dari boardgamegeek ) untuk dua kartu tersebut:

Dalam contoh, saya mengambil satu baris dengan kemiringan nol (merah), dan satu dengan kemiringan 1 (hijau). Mereka berpotongan tepat pada satu titik yang sama (burung hantu).

Metode ini memastikan bahwa dua kartu memiliki tepat satu simbol yang sama, karena

1. Jika kemiringannya berbeda, maka garis akan selalu bersilangan tepat pada satu titik.
2. Jika kemiringannya sama, maka garis tidak akan berpotongan dan tidak akan ada simbol umum dari kisi. Dalam hal ini, simbol kemiringan akan sama.

Dengan cara ini, kita dapat membuat kartu 7x7 (7 offset dan 7 lereng).

Kami juga dapat membuat tujuh kartu tambahan dari garis vertikal melalui kisi (yaitu mengambil setiap kolom). Untuk itu, ikon infinity slope digunakan.

Karena setiap kartu terdiri dari tujuh simbol dari grid dan tepat satu simbol "slope", kita dapat membuat satu kartu tambahan, yang hanya terdiri dari semua 8 simbol slope.

Ini membuat kita dengan 7x8 + 1 = 57 kartu yang mungkin, dan 7 x 7 + 8 = 57 simbol yang diperlukan.

(Secara alami, ini hanya bekerja dengan kisi berukuran bilangan prima (misalnya n = 7). Kalau tidak, garis-garis kemiringan yang berbeda dapat memiliki nol atau lebih dari satu persimpangan jika lereng merupakan pembagi ukuran kisi.)

Jadi ada k = 55 kartu yang berisi m = 8 gambar masing-masing dari kumpulan n gambar total. Kita bisa menyatakan kembali pertanyaan 'Berapa banyak gambar n kita perlu, sehingga kita dapat membangun satu set k kartu dengan hanya satu gambar dibagi antara setiap pasangan kartu?' ekuivalen dengan bertanya:

Diberikan ruang vektor n- dimensi dan himpunan semua vektor, yang berisi elemen m persis sama dengan satu dan semua nol lainnya, seberapa besar n harus, sehingga kita dapat menemukan satu set vektor k , yang produk titik berpasangannya adalah semua sama dengan 1 ?

Ada tepat ( n pilih m ) vektor yang memungkinkan untuk membangun pasangan. Jadi kita setidaknya membutuhkan n yang cukup besar sehingga ( n pilih m )> = k . Ini hanya batas bawah, jadi untuk memenuhi batasan kompatibilitas berpasangan kita mungkin membutuhkan n yang jauh lebih tinggi .

Hanya untuk bereksperimen sedikit, saya menulis sebuah program kecil Haskell untuk menghitung set kartu yang valid:

Sunting: Saya baru sadar setelah melihat solusi Neil dan Gajet, bahwa algoritma yang saya gunakan tidak selalu menemukan solusi terbaik, jadi semuanya di bawah ini belum tentu valid. Saya akan segera mencoba memperbarui kode saya.

module Main where

cardCandidates n m = cardCandidates' [] (n-m) m
cardCandidates' buildup  0  0 = [buildup]
cardCandidates' buildup zc oc
    | zc>0 && oc>0 = zerorec ++ onerec
    | zc>0         = zerorec
    | otherwise    = onerec
    where zerorec = cardCandidates' (0:buildup) (zc-1) oc
          onerec  = cardCandidates' (1:buildup) zc (oc-1)

dot x y = sum $ zipWith (*) x y
compatible x y = dot x y == 1

compatibleCards = compatibleCards' []
compatibleCards' valid     [] = valid
compatibleCards' valid (c:cs)
  | all (compatible c) valid = compatibleCards' (c:valid) cs
  |                otherwise = compatibleCards'    valid  cs

legalCardSet n m = compatibleCards $ cardCandidates n m

main = mapM_ print [(n, length $ legalCardSet n m) | n<-[m..]]
  where m = 8

Jumlah maksimum kartu yang kompatibel yang dihasilkan untuk m = 8 gambar per kartu untuk jumlah gambar yang berbeda untuk dipilih dari n untuk beberapa n pertama terlihat seperti ini:

Metode brute force ini tidak terlalu jauh karena ledakan kombinatorial. Tapi saya pikir itu mungkin masih menarik.

Menariknya, tampaknya untuk m yang diberikan , k meningkat dengan n hanya sampai n tertentu , setelah itu tetap konstan.

Ini berarti, bahwa untuk setiap jumlah gambar per kartu ada sejumlah gambar untuk dipilih, yang menghasilkan jumlah maksimum kartu legal. Menambahkan lebih banyak gambar untuk dipilih dari masa lalu bahwa jumlah optimal tidak menambah jumlah kartu legal lebih jauh.

Beberapa k optimal pertama adalah:

Yang lain telah menjelaskan kerangka kerja umum untuk desain (finive projective plane) dan menunjukkan bagaimana menghasilkan pesawat projektif terbatas orde utama. Saya hanya ingin mengisi beberapa celah.

Pesawat proyektif yang terbatas dapat dihasilkan untuk banyak pesanan yang berbeda, tetapi mereka paling mudah dalam hal pesanan utama p. Kemudian bilangan bulat modulo pmembentuk bidang terbatas yang dapat digunakan untuk menggambarkan koordinat untuk titik dan garis dalam pesawat. Ada 3 jenis koordinat untuk titik-titik: (1,x,y), (0,1,x), dan (0,0,1), di mana xdan ydapat mengambil nilai-nilai dari 0ke p-1. 3 jenis poin menjelaskan rumus p^2+p+1untuk jumlah poin dalam sistem. Kami juga bisa menggambarkan garis dengan 3 jenis yang sama dari koordinat: [1,x,y], [0,1,x], dan [0,0,1].

Kami menghitung apakah suatu titik dan garis adalah insiden dengan apakah produk titik dari koordinatnya sama dengan 0 mod p. Jadi misalnya titik (1,2,5)dan garis [0,1,1]adalah kejadian p=7sejak saat itu 1*0+2*1+5*1 = 7 == 0 mod 7, tetapi titik (1,3,3)dan garis [1,2,6]bukan kejadian sejak itu 1*1+3*2+3*6 = 25 != 0 mod 7.

Menerjemahkan ke dalam bahasa kartu dan gambar, itu berarti kartu dengan koordinat (1,2,5)berisi gambar dengan koordinat [0,1,1], tetapi kartu dengan koordinat (1,3,3)tidak berisi gambar dengan koordinat [1,2,6]. Kita dapat menggunakan prosedur ini untuk mengembangkan daftar kartu lengkap dan gambar-gambar yang dikandungnya.

Ngomong-ngomong, saya pikir lebih mudah untuk menganggap gambar sebagai titik dan kartu sebagai garis, tetapi ada dualitas dalam geometri projektif antara titik dan garis sehingga benar-benar tidak masalah. Namun, pada bagian selanjutnya saya akan menggunakan poin untuk gambar dan garis untuk kartu.

Konstruksi yang sama berfungsi untuk bidang terbatas apa pun. Kita tahu bahwa ada bidang keteraturan terbatas qjika dan hanya jika q=p^k, kekuatan utama. Bidang ini disebut GF(p^k)yang merupakan singkatan dari "bidang Galois". Ladang tidak mudah dibangun dalam wadah listrik utama seperti pada wadah listrik utama.

Untungnya, kerja keras telah dilakukan dan diimplementasikan dalam perangkat lunak bebas, yaitu Sage . Untuk mendapatkan desain bidang proyektif pesanan 4, misalnya, ketikkan saja

print designs.ProjectiveGeometryDesign(2,1,GF(4,'z'))

dan Anda akan mendapatkan output yang mirip

ProjectiveGeometryDesign<points=[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19, 20], blocks=[[0, 1, 2, 3, 20], [0,
4, 8, 12, 16], [0, 5, 10, 15, 19], [0, 6, 11, 13, 17], [0, 7, 9, 14,
18], [1, 4, 11, 14, 19], [1, 5, 9, 13, 16], [1, 6, 8, 15, 18], [1, 7,
10, 12, 17], [2, 4, 9, 15, 17], [2, 5, 11, 12, 18], [2, 6, 10, 14, 16],
[2, 7, 8, 13, 19], [3, 4, 10, 13, 18], [3, 5, 8, 14, 17], [3, 6, 9, 12,
19], [3, 7, 11, 15, 16], [4, 5, 6, 7, 20], [8, 9, 10, 11, 20], [12, 13,
14, 15, 20], [16, 17, 18, 19, 20]]>

Saya menafsirkan di atas sebagai berikut: ada 21 gambar berlabel 0 hingga 20. Setiap blok (garis dalam geometri projektif) memberi tahu saya gambar mana yang muncul pada kartu. Misalnya, kartu pertama memiliki gambar 0, 1, 2, 3, dan 20; kartu kedua akan memiliki gambar 0, 4, 8, 12, dan 16; dan seterusnya.

Sistem pesanan 7 dapat dihasilkan oleh

print designs.ProjectiveGeometryDesign(2,1,GF(7)) 

yang menghasilkan output

ProjectiveGeometryDesign<points=[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28,
29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46,
47, 48, 49, 50, 51, 52, 53, 54, 55, 56], blocks=[[0, 1, 2, 3, 4, 5, 6,
56], [0, 7, 14, 21, 28, 35, 42, 49], [0, 8, 16, 24, 32, 40, 48, 50], [0,
9, 18, 27, 29, 38, 47, 51], [0, 10, 20, 23, 33, 36, 46, 52], [0, 11, 15,
26, 30, 41, 45, 53], [0, 12, 17, 22, 34, 39, 44, 54], [0, 13, 19, 25,
31, 37, 43, 55], [1, 7, 20, 26, 32, 38, 44, 55], [1, 8, 15, 22, 29, 36,
43, 49], [1, 9, 17, 25, 33, 41, 42, 50], [1, 10, 19, 21, 30, 39, 48,
51], [1, 11, 14, 24, 34, 37, 47, 52], [1, 12, 16, 27, 31, 35, 46, 53],
[1, 13, 18, 23, 28, 40, 45, 54], [2, 7, 19, 24, 29, 41, 46, 54], [2, 8,
14, 27, 33, 39, 45, 55], [2, 9, 16, 23, 30, 37, 44, 49], [2, 10, 18, 26,
34, 35, 43, 50], [2, 11, 20, 22, 31, 40, 42, 51], [2, 12, 15, 25, 28,
38, 48, 52], [2, 13, 17, 21, 32, 36, 47, 53], [3, 7, 18, 22, 33, 37, 48,
53], [3, 8, 20, 25, 30, 35, 47, 54], [3, 9, 15, 21, 34, 40, 46, 55], [3,
10, 17, 24, 31, 38, 45, 49], [3, 11, 19, 27, 28, 36, 44, 50], [3, 12,
14, 23, 32, 41, 43, 51], [3, 13, 16, 26, 29, 39, 42, 52], [4, 7, 17, 27,
30, 40, 43, 52], [4, 8, 19, 23, 34, 38, 42, 53], [4, 9, 14, 26, 31, 36,
48, 54], [4, 10, 16, 22, 28, 41, 47, 55], [4, 11, 18, 25, 32, 39, 46,
49], [4, 12, 20, 21, 29, 37, 45, 50], [4, 13, 15, 24, 33, 35, 44, 51],
[5, 7, 16, 25, 34, 36, 45, 51], [5, 8, 18, 21, 31, 41, 44, 52], [5, 9,
20, 24, 28, 39, 43, 53], [5, 10, 15, 27, 32, 37, 42, 54], [5, 11, 17,
23, 29, 35, 48, 55], [5, 12, 19, 26, 33, 40, 47, 49], [5, 13, 14, 22,
30, 38, 46, 50], [6, 7, 15, 23, 31, 39, 47, 50], [6, 8, 17, 26, 28, 37,
46, 51], [6, 9, 19, 22, 32, 35, 45, 52], [6, 10, 14, 25, 29, 40, 44,
53], [6, 11, 16, 21, 33, 38, 43, 54], [6, 12, 18, 24, 30, 36, 42, 55],
[6, 13, 20, 27, 34, 41, 48, 49], [7, 8, 9, 10, 11, 12, 13, 56], [14, 15,
16, 17, 18, 19, 20, 56], [21, 22, 23, 24, 25, 26, 27, 56], [28, 29, 30,
31, 32, 33, 34, 56], [35, 36, 37, 38, 39, 40, 41, 56], [42, 43, 44, 45,
46, 47, 48, 56], [49, 50, 51, 52, 53, 54, 55, 56]]>

Saya baru saja menemukan cara untuk melakukannya dengan 57 atau 58 gambar tetapi sekarang saya memiliki sakit kepala yang sangat buruk, saya akan memposting kode ruby ​​dalam 8-10 jam setelah saya tidur nyenyak! hanya petunjuk solusi saya saya setiap 7 kartu berbagi tanda yang sama dan total 56 kartu dapat dibangun menggunakan solusi saya.

di sini adalah kode yang menghasilkan 57 kartu yang dibicarakan oleh ypercube. tepatnya menggunakan 57 gambar, dan maaf saya telah menulis kode C ++ yang sebenarnya tetapi mengetahui bahwa itu vector <something>adalah array yang berisi nilai-nilai tipe somethingmudah untuk memahami apa yang dilakukan kode ini. dan kode ini menghasilkan P^2+P+1kartu menggunakan P^2+P+1gambar yang masing-masing berisi P+1gambar dan hanya berbagi 1 gambar yang sama, untuk setiap nilai P utama. yang berarti kita dapat memiliki 7 kartu menggunakan 7 gambar masing-masing memiliki 3 gambar (untuk p = 2), 13 kartu menggunakan 13 gambar (untuk p = 3), 31 kartu menggunakan 31 gambar (untuk p = 5), 57 kartu untuk 57 gambar (untuk p = 7) dan seterusnya ...

#include <iostream>
#include <vector>

using namespace std;

vector <vector<int> > cards;

void createcards(int p)
{
    cards.resize(0);
    for (int i=0;i<p;i++)
    {
        cards.resize(cards.size()+1);
        for(int j=0;j<p;j++)
        {
            cards.back().push_back(i*p+j);
        }
        cards.back().push_back(p*p+1);
    }

    for (int i=0;i<p;i++)
    {
        for(int j=0;j<p;j++)
        {
            cards.resize(cards.size()+1);
            for(int k=0;k<p;k++)
            {
                cards.back().push_back(k*p+(j+i*k)%p);
            }
            cards.back().push_back(p*p+2+i);
        }
    }

    cards.resize(cards.size()+1);

    for (int i=0;i<p+1;i++)
        cards.back().push_back(p*p+1+i);
}

void checkCards()
{
    cout << "---------------------\n";
    for(unsigned i=0;i<cards.size();i++)
    {
        for(unsigned j=0;j<cards[i].size();j++)
        {
            printf("%3d",cards[i][j]);
        }
        cout << "\n";
    }
    cout << "---------------------\n";
    for(unsigned i=0;i<cards.size();i++)
    {
        for(unsigned j=i+1;j<cards.size();j++)
        {
            int sim = 0;
            for(unsigned k=0;k<cards[i].size();k++)
                for(unsigned l=0;l<cards[j].size();l++)
                    if (cards[i][k] == cards[j][l])
                        sim ++;
            if (sim != 1)
                cout << "there is a problem between cards : " << i << " " << j << "\n";

        }
    }
}

int main()
{
    int p;
    for(cin >> p; p!=0;cin>> p)
    {
        createcards(p);
        checkCards();
    }
}

lagi maaf untuk kode yang tertunda.

Inilah solusi Gajet dalam Python, karena saya menemukan Python lebih mudah dibaca. Saya telah memodifikasinya sehingga berfungsi dengan angka non-prima juga. Saya telah menggunakan wawasan Thies untuk menghasilkan beberapa kode tampilan yang lebih mudah dipahami.

from __future__ import print_function
from itertools import *

def create_cards(p):
    for min_factor in range(2, 1 + int(p ** 0.5)):
        if p % min_factor == 0:
            break
    else:
        min_factor = p
    cards = []
    for i in range(p):
        cards.append(set([i * p + j for j in range(p)] + [p * p]))
    for i in range(min_factor):
        for j in range(p):
            cards.append(set([k * p + (j + i * k) % p
                              for k in range(p)] + [p * p + 1 + i]))

    cards.append(set([p * p + i for i in range(min_factor + 1)]))
    return cards, p * p + p + 1

def display_using_stars(cards, num_pictures):
    for pictures_for_card in cards:
        print("".join('*' if picture in pictures_for_card else ' '
                      for picture in range(num_pictures)))

def check_cards(cards):
    for card, other_card in combinations(cards, 2):
        if len(card & other_card) != 1:
            print("Cards", sorted(card), "and", sorted(other_card),
                  "have intersection", sorted(card & other_card))

cards, num_pictures = create_cards(7)
display_using_stars(cards, num_pictures)
check_cards(cards)

Dengan output:

***      *   
   ***   *   
      ****   
*  *  *   *  
 *  *  *  *  
  *  *  * *  
*   *   *  * 
 *   **    * 
  **   *   * 
*    * *    *
 * *    *   *
  * * *     *
         ****

Menggunakan z3teorema teorema

Membiarkan Pmenjadi jumlah simbol per kartu. Menurut artikel ini dan ypercubeᵀᴹjawabannya N = P**2 - P + 1masing-masing ada kartu dan simbol. Setumpuk kartu dapat diwakili dengan matriks insiden yang memiliki baris untuk setiap kartu dan kolom untuk setiap simbol yang mungkin. Its (i,j)elemen 1jika kartu imemiliki simbol jdi atasnya. Kita hanya perlu mengisi matriks ini dengan batasan berikut:

• setiap elemen adalah nol atau satu
• jumlah setiap baris persis P
• jumlah setiap kolom persis P
• setiap dua baris harus memiliki tepat satu simbol yang sama

Itu berarti N**2variabel dan N**2 + 2*N + (N choose 2)kendala. Tampaknya dapat dikelola dalam waktu yang tidak terlalu lama dengan z3input kecil.

sunting : Sayangnya P = 8 tampaknya terlalu besar untuk metode ini. Saya membunuh proses setelah 14 jam waktu perhitungan.

from z3 import *
from itertools import combinations

def is_prime_exponent(K):
    return K > 1 and K not in 6  # next non-prime exponent is 10, 
                                 # but that is too big anyway

def transposed(rows):
    return zip(*rows)

def spotit_z3(symbols_per_card):
    K = symbols_per_card - 1
    N = symbols_per_card ** 2 - symbols_per_card + 1
    if not is_prime_exponent(K):
        raise TypeError("Symbols per card must be a prime exponent plus one.")

    constraints = []

    # the rows of the incidence matrix
    s = N.bit_length()
    rows = [[BitVec("r%dc%d" % (r, c), s) for c in range(N)] for r in range(N)]

    # every element must be either 1 or 0
    constraints += [Or([elem == 1, elem == 0]) for row in rows for elem in row]

    # sum of rows and cols must be exactly symbols_per_card
    constraints += [Sum(row) == symbols_per_card for row in rows]
    constraints += [Sum(col) == symbols_per_card for col in transposed(rows)]

    # Any two rows must have exactly one symbol in common, in other words they
    # differ in (symbols_per_card - 1) symbols, so their element-wise XOR will
    # have 2 * (symbols_per_card - 1) ones.
    D = 2 * (symbols_per_card - 1)
    for row_a, row_b in combinations(rows, 2):
        constraints += [Sum([a ^ b for a, b in zip(row_a, row_b)]) == D]

    solver = Solver()
    solver.add(constraints)

    if solver.check() == unsat:
        raise RuntimeError("Could not solve it :(")

    # create the incidence matrix
    model = solver.model()
    return [[model[elem].as_long() for elem in row] for row in rows]


if __name__ == "__main__":
    import sys
    symbols_per_card = int(sys.argv[1])
    incidence_matrix = spotit_z3(symbols_per_card)
    for row in incidence_matrix:
        print(row)

Hasil

$python spotit_z3.py 3
[0, 0, 1, 1, 0, 1, 0]
[0, 0, 0, 0, 1, 1, 1]
[0, 1, 0, 1, 0, 0, 1]
[1, 1, 0, 0, 0, 1, 0]
[0, 1, 1, 0, 1, 0, 0]
[1, 0, 0, 1, 1, 0, 0]
[1, 0, 1, 0, 0, 0, 1]
python spotit_z3.py 3  1.12s user 0.06s system 96% cpu 1.225 total

$ time python3 spotit_z3.py 4
[0, 0, 0, 0, 0, 0, 1, 0, 1, 1, 0, 1, 0]
[0, 0, 0, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0]
[0, 0, 0, 1, 0, 1, 1, 0, 0, 0, 0, 0, 1]
[0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 1, 1, 0]        
[0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1]
[0, 0, 1, 0, 1, 1, 0, 0, 0, 1, 0, 0, 0]
[0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 1]
[0, 1, 0, 0, 1, 0, 1, 1, 0, 0, 0, 0, 0]
[0, 1, 1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0]
[1, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1]
[1, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0]
[1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0]
[1, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0]
python spotit_z3.py 4  664.62s user 0.15s system 99% cpu 11:04.88 total

$ time python3 spotit_z3.py 5
[1, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0]
[0, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0]
[0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0]
[0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1, 0, 0]
[0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0]
[0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0]
[0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 1, 0, 1]
[0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, 0]
[0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
[0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0]
[0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0]
[0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1]
[1, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0]
[0, 1, 0, 1, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0]
[0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, 1, 0]
[0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 1]
[1, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]
[1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1, 0]
[0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0]
[0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 1]
[1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0]
python spotit_z3.py 5  1162.72s user 20.34s system 99% cpu 19:43.39 total

$ time python3 spotit_z3.py 8
<I killed it after 14 hours of run time.>

Saya sangat menyukai utas ini. Saya membangun proyek python github ini dengan bagian-bagian dari kode ini di sini untuk menggambar kartu khusus sebagai png (jadi orang dapat memesan permainan kartu khusus di internet).

https://github.com/plagtag/ProjectiveGeometry-Game

Saya menulis sebuah artikel tentang cara membuat deck semacam ini, dengan kode di Perl. Kode tidak dioptimalkan tetapi setidaknya mampu menghasilkan setumpuk pesanan "masuk akal" ... dan beberapa lainnya.

Berikut adalah contoh dengan urutan 8, yang harus mempertimbangkan matematika dasar yang sedikit lebih rumit, karena 8 tidak prima meskipun urutan yang valid untuk menghasilkan deck semacam ini. Lihat di atas atau artikel untuk penjelasan yang lebih rinci, di bawah ini jika Anda hanya ingin menghasilkan Spot-It yang sedikit lebih sulit :-)

$ time pg2 8
elements in field: 8
  0. (1, 9, 17, 25, 33, 41, 49, 57, 65)
  1. (0, 9, 10, 11, 12, 13, 14, 15, 16)
  2. (2, 9, 18, 27, 36, 45, 54, 63, 72)
  3. (6, 9, 22, 26, 37, 43, 56, 60, 71)
  4. (7, 9, 23, 32, 34, 46, 52, 59, 69)
  5. (8, 9, 24, 30, 35, 42, 55, 61, 68)
  6. (3, 9, 19, 29, 39, 44, 50, 64, 70)
  7. (4, 9, 20, 31, 38, 48, 53, 58, 67)
  8. (5, 9, 21, 28, 40, 47, 51, 62, 66)
  9. (0, 1, 2, 3, 4, 5, 6, 7, 8)
 10. (1, 10, 18, 26, 34, 42, 50, 58, 66)
 11. (1, 14, 22, 30, 38, 46, 54, 62, 70)
 12. (1, 15, 23, 31, 39, 47, 55, 63, 71)
 13. (1, 16, 24, 32, 40, 48, 56, 64, 72)
 14. (1, 11, 19, 27, 35, 43, 51, 59, 67)
 15. (1, 12, 20, 28, 36, 44, 52, 60, 68)
 16. (1, 13, 21, 29, 37, 45, 53, 61, 69)
 17. (0, 17, 18, 19, 20, 21, 22, 23, 24)
 18. (2, 10, 17, 28, 35, 46, 53, 64, 71)
 19. (6, 14, 17, 29, 34, 48, 51, 63, 68)
 20. (7, 15, 17, 26, 40, 44, 54, 61, 67)
 21. (8, 16, 17, 27, 38, 47, 50, 60, 69)
 22. (3, 11, 17, 31, 37, 42, 52, 62, 72)
 23. (4, 12, 17, 30, 39, 45, 56, 59, 66)
 24. (5, 13, 17, 32, 36, 43, 55, 58, 70)
 25. (0, 49, 50, 51, 52, 53, 54, 55, 56)
 26. (3, 10, 20, 30, 40, 43, 49, 63, 69)
 27. (2, 14, 21, 32, 39, 42, 49, 60, 67)
 28. (8, 15, 18, 28, 37, 48, 49, 59, 70)
 29. (6, 16, 19, 31, 36, 46, 49, 61, 66)
 30. (5, 11, 23, 26, 38, 45, 49, 64, 68)
 31. (7, 12, 22, 29, 35, 47, 49, 58, 72)
 32. (4, 13, 24, 27, 34, 44, 49, 62, 71)
 33. (0, 57, 58, 59, 60, 61, 62, 63, 64)
 34. (4, 10, 19, 32, 37, 47, 54, 57, 68)
 35. (5, 14, 18, 31, 35, 44, 56, 57, 69)
 36. (2, 15, 24, 29, 38, 43, 52, 57, 66)
 37. (3, 16, 22, 28, 34, 45, 55, 57, 67)
 38. (7, 11, 21, 30, 36, 48, 50, 57, 71)
 39. (6, 12, 23, 27, 40, 42, 53, 57, 70)
 40. (8, 13, 20, 26, 39, 46, 51, 57, 72)
 41. (0, 65, 66, 67, 68, 69, 70, 71, 72)
 42. (5, 10, 22, 27, 39, 48, 52, 61, 65)
 43. (3, 14, 24, 26, 36, 47, 53, 59, 65)
 44. (6, 15, 20, 32, 35, 45, 50, 62, 65)
 45. (2, 16, 23, 30, 37, 44, 51, 58, 65)
 46. (4, 11, 18, 29, 40, 46, 55, 60, 65)
 47. (8, 12, 21, 31, 34, 43, 54, 64, 65)
 48. (7, 13, 19, 28, 38, 42, 56, 63, 65)
 49. (0, 25, 26, 27, 28, 29, 30, 31, 32)
 50. (6, 10, 21, 25, 38, 44, 55, 59, 72)
 51. (8, 14, 19, 25, 40, 45, 52, 58, 71)
 52. (4, 15, 22, 25, 36, 42, 51, 64, 69)
 53. (7, 16, 18, 25, 39, 43, 53, 62, 68)
 54. (2, 11, 20, 25, 34, 47, 56, 61, 70)
 55. (5, 12, 24, 25, 37, 46, 50, 63, 67)
 56. (3, 13, 23, 25, 35, 48, 54, 60, 66)
 57. (0, 33, 34, 35, 36, 37, 38, 39, 40)
 58. (7, 10, 24, 31, 33, 45, 51, 60, 70)
 59. (4, 14, 23, 28, 33, 43, 50, 61, 72)
 60. (3, 15, 21, 27, 33, 46, 56, 58, 68)
 61. (5, 16, 20, 29, 33, 42, 54, 59, 71)
 62. (8, 11, 22, 32, 33, 44, 53, 63, 66)
 63. (2, 12, 19, 26, 33, 48, 55, 62, 69)
 64. (6, 13, 18, 30, 33, 47, 52, 64, 67)
 65. (0, 41, 42, 43, 44, 45, 46, 47, 48)
 66. (8, 10, 23, 29, 36, 41, 56, 62, 67)
 67. (7, 14, 20, 27, 37, 41, 55, 64, 66)
 68. (5, 15, 19, 30, 34, 41, 53, 60, 72)
 69. (4, 16, 21, 26, 35, 41, 52, 63, 70)
 70. (6, 11, 24, 28, 39, 41, 54, 58, 69)
 71. (3, 12, 18, 32, 38, 41, 51, 61, 71)
 72. (2, 13, 22, 31, 40, 41, 50, 59, 68)
errors in check: 0

real    0m0.303s
user    0m0.200s
sys 0m0.016s

Setiap pengenal dari 0ke 72dapat dibaca sebagai pengenal kartu dan pengenal gambar. Misalnya, baris terakhir berarti:

• kartu 72berisi gambar 2,13 , 22, ..., 59, 68, DAN
• gambar 72muncul di kartu 2, 13, 22, ..., 59, dan 68.