Блог

Я не изучаю информатику и не очень хорошо разбираюсь в алгоритмах или логике высказываний. Тем не менее, я использую SMT solver в проекте и хотел бы получить общее представление о том, как работает алгоритм?

По сути, у меня есть функция

f(x)=(p_0)x (p_1)x^2 (p_2)x^3 ...(p_n)^x^n

и набор уравнений, таких как

f(x)>0

f(x)<1

f(x) f'(x)f(x)<0.5

Решатель SMT z3 вычисляет коэффициенты p_0,p_1...,p_n путем проверки на выполнимость заданных ограничений по набору выборок данных.

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

Вы можете думать о SMT как об одном великолепном алгоритме поиска, но это было бы крайне вводящим в заблуждение: он намного умнее и изощреннее, чем этот. В частности, он определенно не выполняет поиск по всему пространству выборки, как вы выразились. (Представьте: решатели SMT могут иметь дело с неограниченными целыми числами и действительными числами: было бы невозможно выполнить их исчерпывающий поиск.)

К сожалению, это слишком широкий вопрос, чтобы отвечать на него в контексте переполнения стека, но вам повезло, что есть много отличных ссылок, которые стоят того, чтобы потратить ваше время и прочитать. Вот два моих любимых:

• Книга «Процедуры принятия решений»http://www.decision-procedures.org / это отличное чтение, и в нем есть много ссылок, которые могут помочь вам ориентироваться в литературе. Эта книга расскажет вам все об алгоритмах, используемых в SMT-решателях для различных логик, и даже поможет вам, если вы заинтересованы в их создании.

• http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.367.9961amp;rep=rep1amp;type=pdf — отличная статья Леонардо и Николая (главных разработчиков z3). Он предоставляет отличный обзор, и его гораздо легче читать, если вас интересуют только приложения.

Я бы рекомендовал начать с последнего и использовать ссылки в нем для дальнейшего изучения области в соответствии с вашими интересами. Есть много отличных статей, руководств и дружелюбное сообщество stack-overflow, которое поможет вам, если вы застряли!