Контроль допуска зазора в оптимизации Z3

Question

Я хотел бы использовать класс z3 optimize для получения неоптимальных результатов, но при этом иметь возможность контролировать, насколько я далек от оптимального результата. Я использую C++ API.

Например, CPLEX имеет параметры epgap и epagap для относительного и абсолютного допуска соответственно. Он использует текущие нижние или верхние границы (в зависимости от того, является ли это минимизацией или максимизацией), чтобы оценить, насколько далеко (не более) текущее решение от оптимального.

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

Возможно ли это с использованием класса optimize, или мне нужно будет реализовать это с помощью экземпляра решателя и самому контролировать границы?

Answer 1

Я не совсем уверен в этом, но я сомневаюсь, что z3 имеет такие параметры.

Конечно, ничего подобного в интерфейсе командной строки не видно:

~$ z3 -p
...
[module] opt, description: optimization parameters
    dump_benchmarks (bool) (default: false)
    dump_models (bool) (default: false)
    elim_01 (bool) (default: true)
    enable_sat (bool) (default: true)
    enable_sls (bool) (default: false)
    maxlex.enable (bool) (default: true)
    maxres.add_upper_bound_block (bool) (default: false)
    maxres.hill_climb (bool) (default: true)
    maxres.max_core_size (unsigned int) (default: 3)
    maxres.max_correction_set_size (unsigned int) (default: 3)
    maxres.max_num_cores (unsigned int) (default: 4294967295)
    maxres.maximize_assignment (bool) (default: false)
    maxres.pivot_on_correction_set (bool) (default: true)
    maxres.wmax (bool) (default: false)
    maxsat_engine (symbol) (default: maxres)
    optsmt_engine (symbol) (default: basic)
    pb.compile_equality (bool) (default: false)
    pp.neat (bool) (default: true)
    priority (symbol) (default: lex)
    rlimit (unsigned int) (default: 0)
    solution_prefix (symbol) (default: )
    timeout (unsigned int) (default: 4294967295)
 ...

---

Альтернатива № 01:

Как вариант - реализовать это самостоятельно поверх z3.

Я бы предложил использовать схему двоичного поиска (см. Оптимизация в SMT с функциями затрат LA(Q)), в противном случае решающая программа OMT будет уточнять только один конец интервала поиска оптимизации, и это может нарушить намеченную цель вашего завершения поиска. критерии.

Обратите внимание, что для того, чтобы этот подход был эффективным, важно, чтобы внутренний T-optimizerвызывается по логическому назначению каждой промежуточной модели, обнаруженной во время поиска. (Я не уверен, доступна ли эта функция на уровне API с помощьюz3).

Вы также можете взглянуть на подход, основанный на линейной регрессии, используемый в Puli - A Problem-Specific OMT Solver. Если возможно, это может ускорить поиск оптимизации и улучшить оценку относительного расстояния от оптимального решения.

---

Альтернатива #02:

OptiMathSAT может предоставлять функции, которые вы ищете, как на уровне API, так и на уровне командной строки:

~$ optimathsat -help
Optimization search options:
 -opt.abort_interval=FLOAT
          If greater than zero, an objective is no longer actively optimized as 
          soon as the current search interval size is smaller than the given 
          value. Applies to all objective functions. (default: 0) 
 -opt.abort_tolerance=FLOAT
          If greater than zero, an objective is no longer actively optimized as 
          soon as the ratio among the current search interval size wrt. its 
          initial size is smaller than the given value. Applies to all 
          objective functions. (default: 0) 

Интервал прерывания является критерием завершения на основе абсолютного размера текущего интервала поиска оптимизации, в то время как допуск прерывания является критерием завершения на основе относительного размера текущего интервала поиска оптимизации относительно начального интервала поиска.

Обратите внимание, что для использования этих критериев завершения пользователь должен:

• предоставить (по крайней мере) начальную нижнюю границу для любой цели минимизации:

  (minimize ... :lower ...)
  

• предоставить (по крайней мере) начальную верхнюю границу для любой цели максимизации:

  (maximize ... :upper ...)
  

Кроме того, инструмент должен быть настроен для использования либо двоичного, либо адаптивного поиска:

 -opt.strategy=STR
          Sets the optimization search strategy: 
           - lin : linear search (default)
           - bin : binary search
           - ada : adaptive search
          A lower bound is required to minimize an objective with bin/ada 
          search strategy. Dual for maximization. 

Если ни один из этих критериев завершения вас не устраивает, вы также можете реализовать свой собственный алгоритм поверх OptiMathSAT. Это относительно легко сделать благодаря следующей опции, которую можно установить как через API, так и через командную строку:

 -opt.no_optimization=BOOL
          If true, the optimization search stops at the first (not optimal) 
          satisfiable solution. (default: false) 

Когда он включен, он заставляет OptiMathSAT вести себя как обычный решатель SMT, за исключением того, что, когда он находит полное логическое присвоение, для которого существует Модель входной формулы, он гарантирует, что Модель оптимальна по отношению к. целевая функция и заданное логическое присвоение (другими словами, он вызывает внутреннююT-optimizerпроцедура для вас).

---

Некоторые мысли.

Решатели OMT работают иначе, чем большинство решателей CP. Они используют арифметику бесконечной точности, а поиск по оптимизации управляется системой SAT. Повышение значения целевой функции становится все труднее, потому что решающая программа OMT вынуждена перечислять все большее количество (возможно, общее) логических присваиваний, разрешая конфликты и выполняя обратный переход на этом пути.

На мой взгляд, размер текущего интервала поиска не всегда является хорошим индикатором относительной сложности достижения прогресса в поиске оптимизации. Необходимо принимать во внимание слишком много факторов, например, возможность отсечения конфликтных положений, связанных с целевой функцией, кодирование входной формулы и т. Д. Это также одна из причин, почему, насколько я видел, большинство людей в сообществе OMT просто используют фиксированный тайм-аут, вместо того, чтобы беспокоиться об использовании каких-либо других критериев завершения. Единственная ситуация, в которой я считаю ее особенно полезной, - это нелинейная оптимизация (которая, однако, еще не является общедоступной с OptiMathSAT).