DNF SAT имеет полиномиальное время, тогда как CNF SAT является NP-полным. Если у меня есть формула первого порядка, логический скелет которой уже находится в ДНФ, будет ли z3 знать об этом, или он будет слепо преобразовывать формулу в КНФ для решения с помощью CDCL?
Моя формула находится в DNF, преобразует ли z3 ее в CNF?
Ответы (1)
Может, особенно в интерактивном контексте с push/pull и/или тактикой, используемой в API. Однако когда это происходит, результирующие ограничения должно быть относительно легко решить. Однако возникает вопрос, почему все кубы переданы Z3, когда каждый из них может быть проверен независимо, оставляя меньше места для путаницы эвристики.
person
Christoph Wintersteiger
schedule
17.06.2014
Спасибо. Это означает, что итеративная проверка каждой чашки по одной более эффективна, чем проверка дизъюнкции всех чашек. Я прав?
- person qsp; 19.06.2014
Возможно - да. Это действительно зависит от того, что именно находится в каждом из литералов. Например, когда все дизъюнкции имеют общее теоретическое выражение, которое может упростить упрощение и которое делает все дизъюнкции ложными, будет быстрее запустить Z3 на всех дизъюнктах одновременно, чтобы избежать повторных вызовов упрощающего. И наоборот, если каждый из дискъюнктов полностью описывает другую модель, то было бы ненужным кодировать их все, чтобы выбрать в качестве результата первый.
- person Christoph Wintersteiger; 19.06.2014
