Описание тега optimathsat
2
ответа
Тайм-аут для Z3 Optimize
Как установить тайм-аут для оптимизатора z3, чтобы он давал вам наиболее известное решение, когда время истекает? from z3 import * s = Optimize() # Hard Problem print(s.check()) print(s.model()) Последующий вопрос: можете ли вы настроить z3 на случа…
25 мар '20 в 03:59
1
ответ
Minizinc. Подсчитать количество смен в цикле
Продолжая другой пост ( Minizinc: сгенерируйте действительную смену). Я пытаюсь иметь максимум 2 im между двойными ls. Сделать это с обычным ограничением довольно сложно, так как таблица переходов будет довольно большой (слишком много путей). Есть л…
26 окт '19 в 21:03
1
ответ
синтаксическая ошибка при переносе кода с Mac на Linux-машину
У меня есть этот код, который я написал для выполнения на моей удаленной машине Linux для некоторых повторяющихся экспериментов с разными входными данными. #!/bin/bash #timeout 10m trap "exit 1" INT repeat() { executiontime=$( /usr/bin/time /home/me…
16 ноя '19 в 19:22
1
ответ
Контроль допуска зазора в оптимизации Z3
Я хотел бы использовать класс z3 optimize для получения неоптимальных результатов, но при этом иметь возможность контролировать, насколько я далек от оптимального результата. Я использую C++ API. Например, CPLEX имеет параметры epgap и epagap для от…
13 дек '19 в 03:51
1
ответ
Как решить проблему покрытия вершины с помощью SAT и оптимизации?
Итак, прямо сейчас я работаю над использованием SAT для решения проблемы минимального покрытия вершин, и вот моя кодировка для графа G = {V,E} имеет k покрытий вершин, и вот пункты: Let n = sizeof(V); Во-первых, хотя бы одна вершина находится в верш…
29 ноя '19 в 17:18
1
ответ
Какие операторы преобразования доступны в Z3 и CVC4 для битовых векторов?
Я пишу кодировку BV проблемы, которая требует преобразования некоторых Int к BitVec наоборот. В mathsat/optimathsat можно использовать: ((_ to_bv BITS) <int_term>) ; Int => BitVec (sbv_to_int <bv_term>) ; Signed BitVec => Int (ubv_…
07 май '20 в 22:39
1
ответ
Инкрементальное обучение с использованием MAXSMT
Можем ли мы использовать предыдущее решение решателя MaxSMT (оптимизировать) поэтапно в z3? Кроме того, есть ли способ распечатать мягкие утверждения в оптимизаторе?
11 дек '19 в 17:52
0
ответов
Математика для информатики [закрыто]
Пожалуйста, проверьте изображение ниже, чтобы попытаться задать вопрос. Какое минимальное количество процессоров необходимо для выполнения всех задач за минимальное параллельное время? https://stackru.com/images/950e6d11350b22dd5b73abc39896780089e2f…
16 дек '21 в 18:44
1
ответ
Линейное программирование, группировка двоичных переменных
Я новичок в линейном программировании, пробовал несколько примеров. Ищу помощь по решению/подходу для приведенной ниже проблемы. Я не уверен, что это линейное программирование, или мне следует поискать другие варианты. Здесь я пытаюсь определить диз…
29 мар '23 в 14:05