Использование переписывания терминов в процедурах принятия решений для арифметики битовых векторов

Question

Я работаю над проектом, целью которого является использование термина перезаписи для решения / упрощения арифметических задач с бит-вектором фиксированного размера, что полезно сделать в качестве предварительного шага к некоторой процедуре принятия решения, такой как основанная на битах-blasting.Термин «перезапись» может решить проблему вообще или иным образом создать гораздо более простую эквивалентную проблему, поэтому сочетание обоих может привести к значительному ускорению.

Я знаю, что многие решатели SMT реализуют эту стратегию (например, Boolector, Beaver, Alt-Ergo или Z3), но трудно найти документы / технические отчеты / и т. д., в которых эти шаги переписывания описаны подробно.В общем, я нашел только статьи, в которых авторы описывают такие шаги упрощения в нескольких параграфах.Я хотел бы найти документ, в котором подробно объясняется использование термина «переписывание»: приводятся примеры правил, обсуждается удобство переписывания AC и / или других эквиациональных аксиом, используется стратегия переписывания и т. Д.

На данный момент,Я только что нашел технический отчет Процедура принятия решения для битовых векторов фиксированной ширины , в котором описываются этапы нормализации / упрощения, выполняемые CVC Lite, и я хотел бы найти больше таких технических отчетов, как этот!Я также нашел плакат о переписывании терминов в STP , но это всего лишь краткое резюме.

Я уже посещал веб-сайты этих SMT-решателей и искал в их Публикации страниц ...

Буду признателен за любую ссылку или любое объяснение того, как переписывание терминов используется в текущих версиях известных решателей SMT.Я особенно заинтересован в Z3, потому что он выглядит как один из самых умных этапов упрощения.Например, Z3 3. * ввел новую процедуру принятия решения о битовых векторах, но, к сожалению, я не смог найти ни одной статьи, описывающей это.

Answer 1

Я согласен с вами. Трудно найти статьи, описывающие этапы предварительной обработки, используемые в современных решателях SMT. Большинство разработчиков SMT-решателей сходятся во мнении, что эти этапы предварительной обработки очень важны для теории битовых векторов. Я считаю, что эти методы не публикуются по нескольким причинам: большинство из них представляют собой небольшие уловки, которые сами по себе не являются значительным научным вкладом; большинство методов работают только в контексте конкретной системы; Техника, которая может показаться очень хорошей для солвера A, не работает для солвера B. Я считаю, что использование SMT-решения с открытым исходным кодом - единственный способ решить эту проблему. Даже если мы опубликуем методы, используемые в конкретном решателе A, было бы очень трудно воспроизвести реальное поведение решателя А, не видя его исходного кода.

В любом случае, вот краткая информация о предварительной обработке, выполненной Z3, и важные детали.

• Несколько правил упрощения могут уменьшить этот размер локально, но увеличить его глобально. Упрощающий должен избегать разрушения памяти, вызванного таким упрощением. Вы можете найти примеры по адресу: http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf

• Первый шаг упрощения выполняет только локальные упрощения, которые сохраняют эквивалентность. Примеры:

2*x - x ->  x 
x and x -> x

• Затем Z3 выполняет постоянное распространение. При условии равенства t = v, где v является значением. Он заменяет t везде на v.

t = 0 and F[t]  -> t = 0 and F[0]

• Затем выполняется устранение Гаусса для битовых векторов. Однако исключаются только те переменные, которые встречаются в арифметических выражениях не более двух раз. Это ограничение используется для предотвращения увеличения количества сумматоров и множителей в вашей формуле. Например, предположим, что у нас x = y+z+w и x происходит в p(x+z), p(x+2*z), p(x+3*z) и p(x+4*z). Тогда, после исключения x, мы получим p(y+2*z+w), p(y+3*z+w), p(y+4*z+w) и p(y+5*z+w). Хотя мы исключили x, у нас больше сумматоров, чем в исходной формуле.

• Далее, это исключает неограниченные переменные. Этот подход описан в докторской диссертации Роберта Браммайера и Роберто Брутомессо.

• Затем выполняется еще один раунд упрощения. На этот раз выполняются локальные контекстуальные упрощения. Эти упрощения потенциально очень дороги. Таким образом, используется пороговое значение для максимального количества посещаемых узлов (значение по умолчанию составляет 10 миллионов). Упрощение локального контекста содержит такие правила, как

(x != 0 or  y = x+1) ->  (x != 0 or y = 1)

• Затем он пытается минимизировать количество множителей, используя дистрибутив. Пример:

a b + a c -> (b + c) * a

• Затем он пытается минимизировать количество сумматоров и множителей, применяя ассоциативность и коммутативность. Предположим, что формула содержит термины a + (b + c) и a + (b + d). Затем Z3 перепишет их так: (a+b)+c и (a+b)+d. Перед преобразованием Z3 придется кодировать 4 сумматора. После этого нужно кодировать только три сумматора, поскольку Z3 использует полностью разделяемые выражения.

• Если формула содержит только операторы равенства, конкатенации, извлечения и аналогичные. Затем Z3 использует специализированный решатель на основе объединения-поиска и конгруэнтного замыкания.

• В противном случае он обрабатывает все биты, использует AIG для минимизации логической формулы и запускает свой SAT-решатель.

Answer 2

Z3 использует переписывание для многих упрощений, выполняемых во время предварительной обработки. Многие из правил перезаписи, используемых для стратегии UFBV (с квантификаторами), подробно описаны в следующей статье:

Wintersteiger, Hamadi, de Moura: эффективное решение количественных формул битовых векторов, FMCAD, 2010