Описание тега sat-solvers
Решатели SAT - это класс алгоритмов для решения проблемы выполнимости булевых формул.
1
ответ
Как установить минизинк решатель
В MiniZinc (Windows IDE) Как я могу решить: flatzinc: error: переменные типа `var float'не поддерживаются бэкэндом решателя FD. Я понимаю, что мне нужен другой решатель, но я не смог найти процедуру установки, и dlg Preferences, кажется, не работает…
31 янв '15 в 15:36
1
ответ
SAT-решение системы одноразовых ограничений
Я пытаюсь решить проблему SAT, которая состоит только из горячих ограничений. Прямо сейчас я использую горячую кодировку, предложенную Клессеном в гл. 4.2 из [1] и MiniSAT. Интересно, есть ли лучший способ решения такой проблемы, например, класс реш…
28 май '13 в 05:29
1
ответ
Ячеистая сеть программирования ограничений
У меня есть ячеистая сеть, как показано на рисунке. Теперь я распределяю значения по всем ребрам в этой спутниковой сети. Я хочу предложить в моей программе, что в моем распределении нет замкнутых циклов. Например, ограничение для верхнего левого кв…
15 фев '13 в 22:17
1
ответ
z3 игнорирует некоторые из моих ограничений?
Stackru-ERS (?), Я играю с z3 и пытаюсь решить следующие ограничения: (declare-const A (_ BitVec 32)) (declare-const B (_ BitVec 32)) (declare-const C (_ BitVec 32)) (declare-const D (_ BitVec 32)) (declare-const E (_ BitVec 32)) (declare-const F (_…
11 дек '15 в 17:40
0
ответов
Обработка строк в Z3
Я пытаюсь решить это с помощью z3py def a(b): if b == 20: return "X" else: return "Y" b = Int("b") solve(a(b) == "X") решение, которое я хочу, это num = 20 но z3 печатает no solution
28 мар '18 в 08:19
1
ответ
Разделение и / или разбиение большого файла CNF / Matrix
Простой вопрос У меня есть очень большой файл CNF с представляет матрицу MXN. допустим,>10000 переменных с соответствующими терминами. Итак, в качестве первого шага я хочу разделить файл CNF или, что еще лучше, разбить матрицу на переменные 100 для …
07 апр '14 в 09:05
1
ответ
Есть ли простой в использовании 0-1 IP решатель для Java?
Я хотел бы использовать решатель целочисленного программирования 0-1 в качестве инструмента в Java-программе. Я не могу найти ничего простого в использовании в Интернете. Я попробовал псевдо-булеву библиотеку из sat4j, но это плохо документировано, …
07 фев '15 в 13:36
3
ответа
Как мне преобразовать ряд математических ограничений в задачи SAT или SMT и получить ответ?
У меня есть произвольный набор ограничений. Например: A, B, C and D are 8-bit integers. A + B + C + D = 50 (A + B) = 25 (C + D) = 30 A < 10 Я могу преобразовать это в проблему SAT, которую можно решить с помощью picosat (я не могу заставить minis…
20 май '17 в 02:18
2
ответа
Определить верхнюю / нижнюю границу для переменных в произвольной формуле высказываний
Учитывая произвольную пропозициональную формулу PHI (линейные ограничения на некоторые переменные), каков наилучший способ определения (приблизительной) верхней и нижней границы для каждой переменной? Некоторые переменные могут быть неограниченными.…
24 янв '12 в 22:17
1
ответ
Z3py: преобразовать формулу Z3 в предложения, используемые picosat
ССЫЛКИ: Z3 доказатель теоремы пикосат с привязками pyhton Я использовал Z3 в качестве SAT-решателя. Для больших формул, похоже, есть проблемы с производительностью, поэтому я хотел проверить picosat, чтобы увидеть, является ли это более быстрой альт…
23 окт '13 в 20:02
3
ответа
Вход CNF для решателя SAT4J
Я совершенно новый для Sat4j Solver.. он говорит, что некоторый файл cnf должен быть передан в качестве ввода Есть ли какой-нибудь возможный способ дать правило в качестве входных данных и получить, является ли оно выполнимым или нет? мое правило бу…
15 окт '10 в 15:23
1
ответ
(get-unsat-core) возвращает пустой в Z3
Я использую Z3, чтобы извлечь ядро из неудовлетворительной формулы. Я использую интерфейс Z3@Rise (веб-интерфейс), чтобы написать следующий код, (set-logic QF_LIA) (set-option :produce-unsat-cores true) (declare-fun ph1 () Int) (declare-fun ph1p (…
08 авг '13 в 17:25
2
ответа
Ищете практические примеры использования SMT Z3 (например, DbC) и альтернативы Z3 с открытым исходным кодом?
Я заинтересовался и ищу практические примеры использования SMT Z3 (например, DbC) с кодом и альтернативами с открытым исходным кодом для этого инструмента. Так что, на самом деле, меня интересуют аналогичные инструменты формального решения Z3, но: э…
06 янв '11 в 13:52
2
ответа
Есть ли инструмент, который реализует не-CNF SAT решатель?
Мне нужен SAT-решатель, способный принимать в качестве входных данных не только файлы CNF, но и обычные текстовые файлы, содержащие предложения с предложениями (пишутся только с и или без). Я не мог найти ни одного. Не могли бы вы указать один?
01 июн '18 в 10:15
2
ответа
Использовать разные решатели в Z3
Я использую интерфейс Z3 Python для создания формул для моих экспериментов. Затем я отправляю эту формулу решателю Z3. Если я прав, Z3 использует свой собственный решатель! Как использовать другой SAT/SMT решатель с Z3py? Способ, который я использую…
19 июн '17 в 04:11
1
ответ
Решение уравнений с использованием логики высказываний
Я ищу идеи о том, как кодировать математические уравнения в форму cnf-sat, чтобы их можно было решить с помощью SAT-решения с открытым исходным кодом, такого как MiniSat. Итак, как мне конвертировать что-то вроде: 3x + 4y - z = 14 -2x - 4z <= -6 x -…
08 дек '15 в 19:28
1
ответ
Предложение SAT Solver, написанного на C++ или haskell. Плюсы и минусы
Мне нужна библиотека или программа для решения SAT, написанная на C++ или haskell. Я хотел бы знать, почему вы выбрали бы это и каковы плюсы и минусы этой библиотеки / программы. Мне нужно, чтобы он был максимально быстрым и простым в использовании.…
12 ноя '12 в 18:30
2
ответа
Как преобразовать логическое выражение в файл cnf?
Мне нужно использовать Sat Solver для проверки выполнимости логических выражений.. У меня сложное логическое выражение, как это Есть ли автоматический конвертер файлов CNF, так что я могу дать его прямо в Sat Solver? Я прочитал файл формата cnf.. но…
16 окт '10 в 07:39
1
ответ
Z3py: вывести большую формулу с 144 переменными
Я использую доказательство теоремы Z3, и у меня есть большая формула (114 переменных). Можно ли напечатать большую формулу со всеми предложениями? Нормальный print str(f) обрезает вывод, и в конце выводится только "...", а не все пункты. Я проверял …
24 окт '13 в 14:57
1
ответ
Что является лучшей практикой в SMT: добавить несколько утверждений или одно и?
Допустим, у меня есть два предложения, которые я хочу смоделировать в SMT, лучше добавить их как отдельные утверждения типа (assert (> x y)) (assert (< y 2)) или добавить одно утверждение с помощью оператора и, как это (assert (and (> x y) …
12 июл '14 в 08:57