Основы алгоритма SMT - PullRequest
Новая
       9

Основы алгоритма SMT

0 голосов
/ 10 марта 2019

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

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

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, проверяя выполнимость данных ограничений для набора выборок данных.

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

1 Ответ

2 голосов
/ 10 марта 2019

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

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

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

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

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

...