Определить верхнюю / нижнюю границу для переменных в произвольной формуле высказываний

Question

Учитывая произвольную пропозициональную формулу PHI (линейные ограничения на некоторые переменные), каков наилучший способ определения (приблизительной) верхней и нижней границы для каждой переменной?

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

например, PHI = (x=3 и y>=1). Верхняя и нижняя границы для x равны 3. Нижняя граница для y равна 1, а у верхней границы нет.

Это очень простой пример, но есть ли вообще решение (возможно, с использованием SMT-решателя)?

Answer 1

Это предполагает, что домен SAT/UNSAT каждой переменной является непрерывным.

1. Используйте решатель SMT, чтобы найти решение для формулы. Если нет решения, то это означает отсутствие верхних / нижних границ, поэтому остановитесь.
2. Для каждой переменной в формуле выполните два двоичных поиска по области переменной, один для поиска нижней границы, другой для верхней границы. Начальным значением в поиске для каждой переменной является значение для переменной в решении, найденном на шаге 1. Используйте SMT-решатель, чтобы проверить каждое поисковое значение на соответствие и методически заключить в скобки границы для каждой переменной.

Псевдокод для функций поиска, предполагающий переменные целочисленной области:

lower_bound(variable, start, formula)
{
    lo = -inf;
    hi = start;
    last_sat = start;
    incr = 1;
    do {
        variable = (lo + hi) / 2;
        if (SMT(formula) == UNSAT) {
            lo = variable + incr;
        } else {
            last_sat = variable;
            hi = variable - incr;
        }
    } while (lo <= hi);
    return last_sat;
}

а также

upper_bound(variable, start, formula)
{
    lo = start;
    hi = +inf;
    last_sat = start;
    do {
        variable = (lo + hi) / 2;
        if (SMT(formula) == SAT) {
            last_sat = variable;
            lo = variable + incr;
        } else {
            hi = variable - incr;
        }
    } while (lo <= hi);
    return last_sat;
}

-inf/+inf - наименьшее / наибольшее значение, представляемое в области каждой переменной. Если lower_bound возвращает -inf, то переменная не имеет нижней границы. Если upper_bound возвращает + inf, то переменная не имеет верхней границы.

Answer 2

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

Тем не менее, большинство языковых привязок высокого уровня включают в себя необходимый механизм, чтобы упростить вашу жизнь. Например, если вы используете библиотеку Haskell SBV для сценария z3, вы можете иметь:

Prelude> import Data.SBV
Prelude Data.SBV> maximize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]
Prelude Data.SBV> maximize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Nothing
Prelude Data.SBV> minimize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]
Prelude Data.SBV> minimize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1]

Первый результат утверждает, что x=3, y=1 максимизирует x по отношению к предикату x==3 && y>=1. Второй результат говорит, что нет значения, которое максимизирует y по отношению к тому же предикату. Третий вызов говорит, что x=3, y=1 минимизирует предикат относительно x. Четвертый вызов говорит, что x=3, y=1 минимизирует предикат по отношению к y. (Подробнее см. http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html.)

Вы также можете использовать опцию "Итеративный" (вместо Quanified), чтобы библиотека выполняла оптимизацию итеративно вместо использования квантификаторов. Эти два метода не эквивалентны, так как последние могут застрять в локальных минимумах / максимумах, но итеративные подходы могут решить проблемы, когда количественная версия слишком сложна для решения SMT.