Mam problem z kombinatoryką, który chciałbym postawić na OEIS - problem polega na tym, że nie mam wystarczającej liczby terminów. To wyzwanie kodowe ma pomóc mi w obliczeniu większej liczby terminów, a zwycięzcą zostanie użytkownik, który prześle największą liczbę terminów.

Problem

Załóżmy, że dam ci trójkątny zestaw żarówek o długości boku $n$ :

     o
    o o
   o o o
  o o o o
 o o o o o
o o o o o o
1 2  ...  n

Zamierzam włączyć trzy żarówki, które tworzą „pionowy” trójkąt równoboczny, jak w poniższym przykładzie:

     o
    o x
   o o o
  o o o o
 o x o o x
o o o o o o

Zanim zapalę światła, Twoim zadaniem jest usunięcie jak największej liczby żarówek z tablicy - bez utraty możliwości wywnioskowania trójkąta włączonych żarówek. Dla jasności, jeśli żarówka została usunięta, nie świeci się, gdy jej położenie jest włączone.

Na przykład, jeśli usuniesz następujące żarówki (oznaczone przez .), zobaczysz tylko następujące dwa światła włączające się (oznaczone przez x), co wystarczy jednoznacznie wydedukować trzecią (nieoświetloną) pozycję:

     .              .
    . o            . x
   . . o          . . o
  o o o .   =>   o o o .
 o o o o .      o x o o . <- the third unlit position
o . . . o o    o . . . o o

Niech a(n)będzie maksymalną liczbą żarówek, które można usunąć bez wprowadzania dwuznaczności.

Przykład

Za pomocą naiwnego algorytmu sprawdziłem wartości do trójkąta o długości boku 7, jak pokazano poniżej:

                                                                      .
                                                      .              . o
                                        .            . o            o . o
                           .           . .          . . o          . o o .
              .           . .         . o o        o o o .        o o . o .
 .           . .         . o o       o o . o      o o o o .      o . o . o o
. .         . o o       . o o o     o . . o o    o . . . o o    o . o . o o o

a(2) = 3    a(3) = 4    a(4) = 5    a(5) = 7     a(6) = 9       a(7) = 11

Punktacja

Zgłoszenie obliczające sekwencję [a(2), a(3), ..., a(n)]dla największej liczby n wygrywa. Jeśli dwa zgłoszenia mają identyczne sekwencje, wygrywa ten, który został wcześniej opublikowany.

Chociaż nie jest to konieczne do przesłania, byłoby pouczające, jeśli opublikujesz konstrukcję wynikowych tablic triangluarowych, jak w powyższym przykładzie.

Python 3 ,n=8

import itertools
from ortools.sat.python import cp_model


def solve(n):
    model = cp_model.CpModel()
    solver = cp_model.CpSolver()
    cells = {
        (y, x): model.NewBoolVar(str((y, x)))
        for y in range(n) for x in range(y + 1)}
    triangles = [
            {cells[v] for v in ((y1, x1), (y2, x1), (y2, x1 + y2 - y1))}
            for (y1, x1) in cells.keys() for y2 in range(y1 + 1, n)]
    for t1, t2 in itertools.combinations(triangles, 2):
        model.AddBoolOr(t1.symmetric_difference(t2))
    model.Minimize(sum(cells.values()))
    solver.Solve(model)
    return len(cells) - round(solver.ObjectiveValue())


for n in itertools.count(2):
    print('a(%d) = %d' % (n, solve(n)))

Wykorzystuje solver CP-SAT Google OR-Tools .

Po uruchomieniu przez ~ 30 sekund wyświetla następujące informacje:

a(2) = 3
a(3) = 4
a(4) = 5
a(5) = 7
a(6) = 9
a(7) = 11
a(8) = 13

Nie zdarzyło mi się nawet próbować czekać, n=9bo prawdopodobnie zajmie to wiele godzin (liczba ograniczeń rośnie$n^6$a(9)=15n=8

Jak to działa

$T_1$$T_2$$T_1$$T_2$

Tak więc pytanie może zostać przeformułowane jako problem SAT, z jednym ograniczeniem dla każdej pary trójkątów.

PS: Chciałbym bardzo podać przykład n=8, ale mam problemy z solverem SAT, który najwyraźniej chce zachować rozwiązania dla siebie.

Uzyskiwanie rozwiązań z programu @ Delfad0r

Rozszerzyłem program @ Delfad0r o rozwiązania wyjściowe. Daje również wyniki pośrednie, więc otrzymujesz dane wyjściowe w następujący sposób:

Solving n = 8:
a(8) >= 9
a(8) >= 10
a(8) >= 11
a(8) >= 12
a(8) >= 13
       o
      . o
     . o o
    . o o .
   o o . o o
  o o o o . .
 o . . o o o .
o . . o . o o o
a(8) = 13

Solving n = 9:
a(9) >= 10
a(9) >= 13
a(9) >= 14
a(9) >= 15
        o
       o o
      o . .
     o . o o
    . o . o o
   . o o o o o
  o o o . o . .
 o o o . . . o o
. o o o o o o . .
a(9) = 15

Obliczenia trwały kilka godzin.

Jeśli niecierpliwisz się i naciskasz Ctrl-Cpo znalezieniu prawdopodobnie nieoptymalnego rozwiązania, program wyświetli to rozwiązanie. Nie trzeba więc długo czekać na to:

                   .
                  o o
                 . o o
                . o o o
               o o . o o
              o . o o o .
             o . o . o o o
            . o o o o o . o
           o . . o o o o o o
          o o o o o o o o o .
         o o . o o o o . o o o
        o o o o o o . o . o o o
       o . o o . o o o o o o o o
      o o o . o o o o o . o o o o
     o o o . o o o o o o o o . . o
    o o o o o o o o o o o . o . . o
   o o o o . o o o o . o o o o o . o
  o o o o o o o o . o o . . o o o o .
 o o o o . o o . o . o o o o o o . o o
o o . o o . o o o o . o o o . o o o o o
a(20) >= 42

Oto rozszerzony program:

import itertools
from ortools.sat.python import cp_model

class ReportPrinter(cp_model.CpSolverSolutionCallback):

    def __init__(self, n, total):
        cp_model.CpSolverSolutionCallback.__init__(self)
        self.__n = n
        self.__total = total

    def on_solution_callback(self):
        print('a(%d) >= %d' %
              (self.__n, self.__total-self.ObjectiveValue()) )

def solve(n):
    model = cp_model.CpModel()
    solver = cp_model.CpSolver()
    cells = {
        (y, x): model.NewBoolVar(str((y, x)))
        for y in range(n) for x in range(y + 1)}
    triangles = [
            {cells[v] for v in ((y1, x1), (y2, x1), (y2, x1 + y2 - y1))}
            for (y1, x1) in cells.keys() for y2 in range(y1 + 1, n)]
    for t1, t2 in itertools.combinations(triangles, 2):
        model.AddBoolOr(t1.symmetric_difference(t2))
    model.Minimize(sum(cells.values()))
    print('Solving n = %d:' % n)
    status = solver.SolveWithSolutionCallback(model, ReportPrinter(n,len(cells)))
    if status == cp_model.OPTIMAL:
        rel = '='
    elif status == cp_model.FEASIBLE:
        rel = '>='
    else:
        print('No result for a(%d)\n' % n)
        return
    for y in range(n):
        print(' '*(n-y-1), end='')
        for x in range(y+1):
            print('.o'[solver.Value(cells[(y,x)])],end=' ')
        print()
    print('a(%d) %s %d' % (n, rel, len(cells) - solver.ObjectiveValue()))
    print()

for n in itertools.count(2):
    solve(n)

Python 3

Opierając się silnie na odpowiedzi Delfad0r , przeważnie podąża tą samą progresją logiczną, sprawdzając pary trójkątów i sprawdzając poprawność konfiguracji, jeśli nie zawiera ona żadnych par trójkątów, które nie sprawdzą tej weryfikacji. Ponieważ nie korzystałem z żadnych bibliotek oprócz itertools i kopiowania, mam pełną kontrolę nad zapisywaniem przykładów napotkanych w całym programie.

examples = dict() # stores examples by key pair of n to a tuple with the triangle and number of lights turned off

for n in range(3, 8):
    tri = [] # model of the triangle, to be filled with booleans representing lights
    tri_points = [] # list of tuples representing points of the triangle
    for i in range(n):
        tri.append([True]*(i + 1))
        for j in range(i+1):
            tri_points.append((i, j))

    t_set = [] # list of all possible triangles from tri, represented by lists of points
    for i in range(n):
        for j in range(len(tri[i])):
            for k in range(1, n - i):
                t_set.append([(i, j), (i + k, j), (i + k, j + k)])

    from itertools import combinations
    import copy

    # validates whether or not a triangle of n lights can have i lights turned off, and saves an example to examples if validated
    def tri_validate(x):
        candidate_list = list(combinations(tri_points, x))
        tri_pairs = list(combinations(t_set, 2))
        for candidate in candidate_list:
            temp_tri = copy.deepcopy(tri)
            valid = False
            for point in candidate:
                (row, col) = point
                temp_tri[row][col] = False
            for pair in tri_pairs:
                valid = False
                (tri1, tri2) = pair
                for point in tri1:
                    if not valid:
                        if point not in tri2:
                            (row, col) = point
                            if temp_tri[row][col]:
                                valid = True
                for point in tri2:
                    if not valid:
                        if point not in tri1:
                            (row, col) = point
                            if temp_tri[row][col]:
                                valid = True
                if not valid:
                    break
            if valid:
                examples[n] = (temp_tri, x)
                return True
        return False

    # iterates up to the point that validation fails, then moves on to the next n
    for i in range(len(tri_points)):
        if tri_validate(i + 1):
            continue
        break

Problem w tym, że nie jest zbyt wydajny. Działa naprawdę szybko n=5, ale zaczyna znacznie zwalniać po tym punkcie. W n=6biegu zajmuje około minuty i jest znacznie wolniejszy n=7. Wyobrażam sobie, że istnieje wiele poprawek wydajności, które można wprowadzić za pomocą tego programu, ale jest to szybko opracowany wstępny szkic dobrego rozwiązania o wiele większej elastyczności, aby sprawdzić wewnętrzne funkcjonowanie tej metody. Z czasem będę stopniowo nad tym pracował.