Багрепорт

[TonitaN]

Багрепорт

[Postlog]

Вот и проблема обнаружилась, я на отдельные элементы ограничения не накладывал, обидно(

[TonitaN]

Случай

X≠bX and Y≠ε and X≠ε and Y≠bY
PairComp(a, b) -> a₁
XYcYX=a₁ca₁

Нужно усилить эвристику, чтобы учитывалось, что длина X и Y больше 0, раз они непусты, и в целых числах тогда уравнение на совокупные длины левой и правой части не решится.

[Postlog]

Баг исправил, над усилением эвристики поработаю

[TonitaN]

Эвристику нужно доделать, иначе разбор взрывается в конце, когда строка уже очень короткая.

[TonitaN]

X=cX and (X≠Xa₁ or Y≠cY)
PairComp(a₁, c) -> a₂
Za₂XYa₂X=a₂a₁

Почему разбор этого узла продолжился? Должна была сработать эвристика по a2.

[TonitaN]

И по каждой константе делать свою модель не нужно, объедините их в одну с разными переменными для учета разных констант. Должно получиться быстрее (если нашлась неудача хотя бы по одной букве, то сразу будет unsat).

[TonitaN]

+нужно заменить полный перебор пустых-непустых значений на перебор по критерию, указанному в ТЗ и в отчете @affeeal

Этот полный перебор добавляет дополнительный этаж в башню экспонент.

[Postlog]

@TonitaN скиньте пожалуйста сопоставление на котором что-то пошло не так

[TonitaN]

[TonitaN]

Проблема с моделями видна с первого же запуска to_smt2()

(set-info :status unknown)
(declare-fun |Zc₂| () Int)
(declare-fun |Za₁| () Int)
(declare-fun Zb () Int)
(assert
 (let ((?x100 (+ (+ Zb |Za₁|) |Zc₂|)))
 (>= ?x100 0)))
(assert
 (= 0 (+ 1 Zb)))
(assert
 (= 1 (+ 1 |Za₁|)))
(assert
 (let ((?x19 (+ 0 |Zc₂|)))
 (= 1 ?x19)))
(check-sat)

Здесь противоречие не определяется, а потому что нигде не сказано, что значения всех переменных должны быть больше либо равны нулю. Нужно вернуть эту рестрикцию + добавить рестрикции, проверяющие, что части уравнения не начинаются с разных констант и не кончаются разными константами.

[Postlog]

Я правильно понял, что в модель нужно добавлять помимо Ya+Yb+... > 0 еще и ограничения по каждой отдельный переменной, т.е. Ya > 0, Yb > 0 итд?

[TonitaN]

Не >, а только >=, иначе будет та же проблема, которую вы обнаружили.

[Postlog]

Но ведь в вашем примере >

[TonitaN]

> у суммы, а у каждого из элементов суммы именно >=
Т.к. y=ya+yb+yc

[TonitaN]

Чуть аккуратнее бы смотрели в z3, были бы аттестованы сегодня...
Теперь проявляйте чудеса убедительности с Захаровым и заодно доделывайте прочие фиксы.

[Postlog]

На ветке empty_substs лежит реалзиация, в рамках которой пустые подстановки не полностью перебираются, а выбираются исходя из правил

[TonitaN]

Вполне закономерный фейл на XXYX=abcab. В принципе, должна дойти до ситуации, где только отрицательные условия и уравнение вида XXYX=c_1000 (одна буква справа), после чего применить эвристику насчёт переменной кратности 1. Но что-то пошло не так.

[TonitaN]

Следующий пример

зачем-то ветвится по вариантам сжатых пар. Сжатие одно, и в принципе здесь по эвристикам всего один вариант распределения значений на втором шаге.

[TonitaN]

Вот две эвристики Z!=Zc и Z!=Xc OR Y=a_4Y должны попасть в одно и то же состояние, т.к. каждая из них порождает лишнюю букву c_16. И если уж сжатие по паре ca_4, то оно по всем ветвям должно делаться, а по первой ветви делается обратное.

[Postlog]

Я не очень понял что не так в XXYX=abcab. В результате все ветви приходят к Y=c_... Мой алгоритм не останавливается на первом найденном решении. По случаю ZbXYbX=abcab тоже не совсем понял, у нас две ветви сжатия ca_4 поскольку там разные ограничения. Единственное - да, сжатие одной и той же пары порождает разные константы - мой косяк, но на решение он не влияет  среда, 13 марта 2024г. в 15:42 +03:00 от ***@***.*** < ***@***.*** >:

…

Вот две эвристики Z!=Zc и Z!=Xc OR Y=a_4Y должны попасть в одно и то же состояние, т.к. каждая из них порождает лишнюю букву c_16. И если уж сжатие по паре ca_4, то оно по всем ветвям должно делаться, а по первой ветви делается обратное. — Reply to this email directly, view it on GitHub , or unsubscribe . You are receiving this because you were assigned. Message ID: <Postlog/recompression/issues/1/1994308497 @ github . com>

[TonitaN]

Не должно быть двух разных ограничений по разным ветвям, должна быть их конъюнкция.

[TonitaN]

И по первой ветви вообще другое сжатие.

[TonitaN]

XXYX=abcab считается очень долго по ветви empty_substs (по main намного быстрее). Хотя там всего 3 сжатия до буквы и почти все варианты, кроме отрицательного, должны отваливаться по эвристикам. И то, что по допветви такой огромный перебор, что я ни разу не смогла дождаться результата, означает, что там что-то пошло не так.

[Postlog]

Не должно быть двух разных ограничений по разным ветвям, должна быть их конъюнкция.

Видимо я не до конца понял главу 6 "Извлечение пар в Pair
Comp" из тз Ильи. После построения прямых произведений, одинаковые подстановки нужно объединять в единую опцию (объединяя при этом рестрикции)?

Я разобрал данный пример:

Получились отдельные опции:

1. Y = Yc & Z != Zc
2. Y = Yc & (X != Xc || Y != aY)

Необходимо все опции такого вида объединять между собой (отбрасывая противоречивые)?

[Postlog]

И по первой ветви вообще другое сжатие.

А в чем тут проблема? Нам выгодно сжать как ac так и ca, поэтому рассматриваются оба сжатия

[TonitaN]

Необходимо все опции такого вида объединять между собой (отбрасывая противоречивые)?

Если смотреть пример в ТЗ, то там рассматривался похожий разбор случаев, за одним важным различием: там два случая были уже композициями подстановок. Т.е. на самом деле у вас должны были быть последовательно два разбора:
1-1. Z=Zc
1-2. Z!=Zc
2-1. Y=Yc
2-2. Y!=Yc
3-1. X=Xc & Y=aY
3-2. X!=Xc V Y!=aY
Все подстановки независимые, поэтому получаются произведения:
(1-1)(2-1)(3-1)
(1-1)(2-1)(3-2)
...
(1-2)(2-2)(3-2)

По-умному, следовало бы ограничить выбор подстановок, порождающих новую букву, сверху сразу же числом таких букв в константной части, чтобы не мучить z3. То есть тут выбирается строго одна из 1-1, 2-1, 3-1, и потом уже 3-1 отваливается по эвристике подсчёта других букв.

По-глупому, рассматривать вообще все комбинации.

[TonitaN]

И по первой ветви вообще другое сжатие.

А в чем тут проблема? Нам выгодно сжать как ac так и ca, поэтому рассматриваются оба сжатия

А в том, что сжатия делаются последовательно, одно за другим. Если сжимаете ac, то вы уже укорачиваете константную часть, и решение будет лишь в том случае, если после сжатия оно есть. Зачем же ещё и избыточно рассматривать другой путь решения, который даст ту же самую информацию?

[Postlog]

Зачем же ещё и избыточно рассматривать другой путь решения, который даст ту же самую информацию?

Вот тут я совсем потерялся. Получается если нам на очередной итерации выгодно сжать несколько пар, то мы можем спокойно рассматривать лишь одну из них? Не может ли быть такого, что сжатие по другой паре даст другой ответ?

[Postlog]

По-глупому, рассматривать вообще все комбинации

Значит нужно рассматривать все возможные комбинации не ПАР опций, а комбинации из n опций, где n = исходное число существенных элементарных и композиционных подстановок?

[TonitaN]

Зачем же ещё и избыточно рассматривать другой путь решения, который даст ту же самую информацию?

Вот тут я совсем потерялся. Получается если нам на очередной итерации выгодно сжать несколько пар, то мы можем спокойно рассматривать лишь одну из них? Не может ли быть такого, что сжатие по другой паре даст другой ответ?

Такого быть не может, потому что сжатия не теряют решения. Так что да, спокойно рассматриваем только одну пару для сжатия за один шаг.

[TonitaN]

По-глупому, рассматривать вообще все комбинации

Значит нужно рассматривать все возможные комбинации не ПАР опций, а комбинации из n опций, где n = исходное число существенных элементарных и композиционных подстановок?

Да, слово "прямое произведение" в ТЗ можно было действительно понять как "прямое произведение пар", однако подразумевается прямое произведение в n-ки, что, кстати, и сделано в реализации Ильи (если посмотрите, как вызывается прямое произведение опций - там цикл по произведению пар).

[Postlog]

Вроде исправил...

[TonitaN]

Стало адекватнее. Но теперь расщепляет на слишком много случаев. Пример:

XYX = abcab
compress(a,b)->c
X=Xa & Y=bY (1-1)
X!=Xa v Y!=bY (1-2)
Y=Ya & X=Xb (2-1)
Y!=Ya v X!=Xb (2-2)

По факту остаётся с учётом эвристик префиксов-суффиксов только (1-2)*(2-2): (X!=Xa v Y!= bY) & (Y!=Ya v X!=Xb). И дальше он зачем-то преобразуется в ДНФ и превращается в 4 ветви только с конъюнкциями, а можно же было оставить всю указанную КНФ целиком, и разбора бы не было.

[Postlog]

Такое поведение я заложил изначально исходя из утверждения что более одной дизъюнкции в рестрикциях быть не может. Получается может, и рестрикции вида (... v ...) & (... v ...) - норма?

[Postlog]

Имеет ли в таком случае смысл их преобразовывать к виду (... & ...) v (... & ... ) v ... для более простой обработки рестрикций?

[TonitaN]

КНФ (а это именно она) ничем не хуже, чем ДНФ. Примерно одинаково просто обрабатываюьтся.

[Postlog]

Есть ли еще какие-либо проблемы, которые мне стоит поправить?

[TonitaN]

Нужно сделать ключ запуска с эвристикой z3 и без неё, для более удобного сбора статистики.

[TonitaN]

В целом реализация ок даже с такой обработкой рестрикций.

[Postlog]

Со вчерашнего вечера пытаюсь избавиться от преобразования КНФ в ДНФ и разбиения на ветви, но я код писал с сильным упором на то, что среди рестрикций может быть лишь одна дизъюнкция, поэтому задача оказалась не столь тривиальной и я скорее всего не успею сделать это до 17:30.

Добавил флаги для запуска, обновил ридми

[TonitaN]

Как уже писала, в принципе и так работает. Аккуратно проверьте последние изменения перед вливанием на максимуме тестов.