0
Я искал решение для поиска (минимального) первичного импликанта для формулы в логике QF_AUBV с использованием решателя z3. возможно ли получить такой частичный первичный импликант из z3-решателя?Prime Implicant in z3
Большое спасибо за ваш ответ. Если я прав, вы имеете в виду, что у меня должен быть алгоритм, чтобы найти основной импликант. Я читал о распространении релевантности в z3, что просто существенные назначения истинности для удовлетворения формулы, распространяются на решателя теории. могу ли я воспользоваться этими заданиями. Я прав, что это частичное назначение, которое может быть основным импликантом для формулы или, возможно, нет. если yse, могу ли я извлечь распространенные присваивания теоретическому решателю из формулы? – Mary
Если вы используете решатель теории, это может помочь (начните смотреть на релевантные_и (...) в других теориях), иначе это, вероятно, не стоит (довольно значительных) усилий. Обратите внимание, что релевантность распространяется также и на небулевые подтермы. Если вы ищете все (первичные или другие) импликанты, вам понадобятся несколько запросов SAT, а не только один, поэтому лучше всего реализовать все это во внешнем слое, а не внутри решателя SMT. –
Большое спасибо. ты прав. могу ли я угодить вам, чтобы больше объяснить, как использовать количественные выражения для аксиоматизации понятия импликантов. это расплывчато для меня. – Mary