Устранение переменных в решателях SAT/SMT

Question

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

Answer 1

Для случая пропозициональной выполнимости, где формула является соединением предложений, каждое из которых является дизъюнкцией литералов. например (A | B) & (!B | A) & (!A | B | A)

Если переменная отображается либо только как положительный литерал, либо только как отрицательный литерал во всей формуле, ее можно безопасно удалить, а любые предложения, в которых она появляется, можно удалить и считать удовлетворенными. Однако в строгом смысле значение такой переменной не имеет значения, поскольку она может быть единственной переменной, которая может удовлетворять этим предложениям в удовлетворительном присваивании для определенных формул. Такие переменные называются чистыми, и эта фаза называется чистым буквальным исключением.

Перед чистым буквальным исключением формула должна быть очищена так, что любое предложение, содержащее переменную, которая выглядит как неотрицательная и отрицательная, удаляется. Это может привести к тому, что некоторые переменные станут чистыми. Более того, на протяжении всей процедуры решения, когда переменная идентифицируется как чистая, она должна быть исключена.

например, пункт (!A | B | A) тривиально удовлетворено: независимо от того, какое значение принимает А, оно выполняется.

затем (A | B) & (!B | A) & (!A | B | A) -> (A | B) & (!B | A)

Теперь A является чистым и может быть установлен в True, что приводит к удовлетворительному назначению. Обратите внимание, что решение было найдено без принятия каких-либо решений, мы просто применили два правила.