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

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

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

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

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


z3 sat-solvers
person liyistc    schedule 24.01.2012    source источник
comment
Этот документ отвечает именно на этот вопрос: cs.utoronto.ca/~aws/papers /popl14.pdf Границы систематически обнаруживаются с помощью итеративного подхода к выборке. В процессе также обнаруживаются неограниченные переменные.   -  person liyistc    schedule 15.02.2014
comment
Этот вопрос кажется не по теме, потому что речь идет об определении границ формулы.   -  person Flexo    schedule 01.07.2014

Ответы (2)


arrow_upward
3
arrow_downward

Это предполагает, что домен 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, то у переменной нет верхней границы.

person Kyle Jones    schedule 26.01.2012

arrow_upward
2
arrow_downward

На практике для большинства таких задач оптимизации требуется своего рода внешний драйвер повторения до максимума/минимума поверх решателя 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#g:34 для подробностей.)

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

person alias    schedule 30.01.2012