Вот подход, в котором не используются DFA.
Я рассмотрел проблему только проверки, существует ли строка заданной длины k
, удовлетворяющей каждому шаблону, и возврата одного, если он есть. Это немного более простая проблема, но мы можем найти самую короткую строку, удовлетворяющую каждому шаблону, проверяя увеличение k
, пока не найдем решение (или пока k
не превысит некоторую верхнюю границу длины кратчайшего решения).
Мое решение недостаточно быстрое, чтобы решить более крупные примеры в течение 10-20 секунд, но, возможно, идея будет полезна в любом случае. Я использовал доказательство теоремы Z3 в Python, но есть привязки для многих языков.
По сути, идея состоит в том, чтобы определить k
формальные переменные, представляющие буквы в затем создайте огромное логическое выражение, кодирующее шаблоны, и используйте решатель Z3 для поиска решения (или проверки того, что решение не существует).
Существует несколько дополнительных приемов для повышения эффективности. Мы можем начать с упрощения шаблонов; лучше иметь ?
с до *
с, чтобы уменьшить коэффициент ветвления, и любая последовательность из двух или более *
с является избыточной. Мы также можем определить минимально возможную длину решения на основе не *
символов в шаблонах.
В принципе ту же идею можно использовать для проверки строк длины <= k
, оптимизируя для самого короткого, введя символ $
в алфавит, добавив ограничение, которое $
не может появляться перед любым символом, кроме $
, и затем решив задачу оптимизации, чтобы максимизировать количество символов $
, Я не пробовал это; Есть также некоторые другие простые улучшения, которые могут быть сделаны, но я постарался сделать это простым, как подтверждение концепции.
Моя реализация ниже. Основная проблема, влияющая на производительность, заключается в том, что размер логического выражения экспоненциально равен числу *
с в данном шаблоне.
from z3 import *
def simplify_pattern(p):
q = ''
while p != q:
q = p
p = p.replace('*?', '?*').replace('**', '*')
return p
def min_length(p):
return len(p.replace('*', ''))
def solve(patterns, max_length):
patterns = [simplify_pattern(p) for p in patterns]
m = max(map(min_length, patterns))
for k in range(m, max_length+1):
s = solve_for_length(patterns, k)
if s is not None:
return s
return None
def solve_for_length(patterns, k):
alphabet = sorted(set(''.join(patterns)) - set('?*'))
vs = [Int('v' + str(i)) for i in range(k)]
constraints = [And(0 <= v, v < len(alphabet)) for v in vs]
for p in patterns:
cs = constraints_for_pattern(p, vs, alphabet)
constraints.extend(cs)
s = Solver()
s.add(constraints)
if s.check() == sat:
m = s.model()
idx = [m.eval(v).as_long() for v in vs]
return ''.join(alphabet[i] for i in idx)
else:
return None
def constraints_for_pattern(pattern, vs, alphabet):
while pattern and pattern[0] != '*':
if not vs:
# output string shorter than pattern
yield False
return
if pattern[0] != '?':
yield vs[0] == alphabet.index(pattern[0])
pattern = pattern[1:]
vs = vs[1:]
if pattern == '*':
pass
elif pattern:
# pattern starts with '*' but != '*'
p = pattern[1:]
yield Or(*[
And(*constraints_for_pattern(p, vs[i:], alphabet))
for i in range(len(vs) - min_length(p) + 1)
])
elif vs:
# output string longer than pattern
yield False
Примеры:
>>> solve(['a?', '?b'], 2)
'ab'
>>> solve(['a*', '*b'], 2)
'ab'
>>> solve(['a*', '?b*', '*c'], 3)
'abc'
>>> solve(['a*a*a*', '*b*b*b'], 5) is None
True
>>> solve(['a*a*a*', '*b*b*b'], 6)
'ababab'
>>> solve(['*a*b*', '*c*d*', '*e*?*'], 10)
'eabcd'
>>> solve(['?a*b', 'a*b*', '*a??a*'], 10)
'aaaab'
>>> mini_5 = [
... "*i*o*?*?*u?*??*e?o*e*a*a*i*ee*",
... "*e*?ue*o*i*?*e*u*i*?*oa?*??*",
... "*?oi*i??uu*a*iu*",
... "*o*e*ea?*eu*?e*",
... "*u*?oe*u*e?*e?*",
... ]
>>> solve(mini_5, 33) # ~20 seconds on my machine
'ioiiueuueaoeiueuiaoaiee'