Описание тега sat
В информатике проблема логической выполнимости (или SAT) - это проблема определения того, существует ли интерпретация, удовлетворяющая заданной булевой формуле.
2
ответа
Инкрементное SAT-решение: сохранить экземпляр решения - изменить модель между прогонами
Насколько я понимаю, инкрементальное SAT-решение помогает оценить различные модели, которые достаточно близки друг к другу. Я хочу использовать это, чтобы оценить модель, и если я изменю ее позже, повторно оцените ее снова, используя предыдущее реше…
24 май '16 в 07:27
1
ответ
Найти, какие значения удовлетворяют булевой формуле
У меня есть следующее логическое выражение x > 5 И y > 10 C:\>python Python 3.6.1 (v3.6.1:69c0db5, Mar 21 2017, 18:41:36)Type "help", "copyright", "credits" or "license" for more information. >>> x = 3 >>> y = 11 >>> ev…
13 июн '18 в 15:21
2
ответа
Редактировать конкретное слово в конкретной строке
Я знаю, что об этом спрашивали несколько раз, но мне нужен быстрый способ сделать это в файлах с различным размером (маленькие и большие файлы). Мне нужно отредактировать масштабный коэффициент в файле Sat(TXT). Это первое число в третьей строке: 70…
16 авг '16 в 10:17
0
ответов
Как реализовать логику AND в Z3Py
Я хочу реализовать ограничение, которое требует логики AND в Z3Py. Предположим, у нас есть две переменные a а также bЯ просто хочу добавить одно ограничение, которое требует a == 0 а также b == 1, Там должно быть несколько способов, которые могут сд…
31 июл '18 в 19:45
0
ответов
Столкновения в САТ работают только в двух направлениях
Я пытаюсь разрешить коллизии через SAT в XNA, но это работает только в двух направлениях внизу и справа). Я полагаю, что эта проблема вызвана тем, что перекрытие не проходит проверку длины, если ось имеет отрицательные компоненты. Метод разрешения с…
14 янв '15 в 03:34
2
ответа
Разница между C-SAT и SAT?
В чем именно разница между этими двумя NP-полными задачами? Мне кажется, что они оба спрашивают, может ли быть выполнена булева формула (т.е. вывод 1), но один находится в контексте схемы, а другой - просто формула. Однако нельзя ли написать булеву …
21 май '17 в 23:54
1
ответ
Как прочитать файл.cnf (конъюнктивная нормальная форма) в C?
Файл показан ниже. Мне нужно прочитать их и сохранить их в структуре данных (может быть список смежности). Но я не знаю, как проигнорировать бесполезную аннотацию и начать читать после 'p cnf'. c This Formula is generated by mcnf c c horn? no c forc…
11 фев '19 в 13:00
0
ответов
Какие структуры данных / алгоритмы для эффективной замены выражений DNF друг на друга?
Я пытаюсь работать с системой, которая имеет несколько сотен логических литералов с отношениями между ними в дизъюнктивной нормальной форме (например, x1 = (x2 & x3) | x4; x2 = x5 | x6; так далее). Я хочу упростить систему, подставляя некоторые …
15 фев '19 в 03:17
1
ответ
Как мы можем вызвать Alloy из Java, не открывая интерфейс?
Я пишу программу, которая должна вызывать Alloy для модели и что-то делать в возвращаемом экземпляре. Проблема в том, что интерфейс Alloy открыт при каждом вызове команды Alloy. Мне интересно, можно ли в любом случае вызвать Alloy из кода Java без о…
06 апр '16 в 22:13
1
ответ
Z3: странное поведение с нелинейной арифметикой
Я только начинаю использовать Z3 (v4.4.0), и я хотел бы попробовать один из примеров учебника: (declare-const a Int) (assert (> (* a a) 3)) (check-sat) (get-model) (echo "Z3 will fail in the next example...") (declare-const b Real) (declare-const…
08 сен '15 в 14:35
1
ответ
Почему уже всплывающие области влияют на время проверки в последующих областях?
Общая проблема Я заметил несколько раз, что push-pop области, которые уже были вытолкнуты, влияют на время check-sat в последующем объеме необходимо. То есть, предположим, что программа имеет несколько (потенциально произвольно вложенных) областей …
20 янв '15 в 14:07
0
ответов
Инструкция Yosys "sat -dump_cnf "
У меня есть пример комбинаторного цирка в Verilog, где я могу следовать инструкции, чтобы сделать логический синтез и сгенерировать файл blif. Однако мне нужно создать формулу CNF из схемы. Инструменты, такие как ABC, позволяют генерировать только и…
13 сен '17 в 12:40
1
ответ
Нахождение пути: SAT решение
Нам дают n*m сетку, в которой есть препятствия в разных точках, в начальной и конечной локациях бота. Задача - найти путь без столкновений от начала до конца. Эта проблема должна быть смоделирована как проблема SAT. Пожалуйста, объясните мне, что ну…
01 июн '17 в 17:02
1
ответ
Как позволить командной строке z3 выводить режим (или несинусное ядро), а не сат / несат?
z3 -smt2 <filename> выводит только "sat" или "unsat". Я хотел бы, чтобы Z3 выводил модель, если ограничение выполнено, или несогласованное ядро, если не выполнено. Какие варианты Z3 я должен использовать?
18 дек '15 в 16:39
1
ответ
Есть ли веб-страница для тестирования моей программы 3-SAT?
Я написал программу для задачи 3-SAT. Есть ли веб-страница, где я могу получить несколько тестов или загрузить программу, чтобы проверить, работает ли она?
11 окт '18 в 14:23
2
ответа
SAT с двумя пунктами является полиномиальным
Какова сложность экземпляра SAT с k унарными предложениями и только двумя предложениями? Я хотел бы найти статью с таким результатом... Я нашел одну статью, в которой проблема немного отличается. Все переменные появляются не более двух раз...
27 июл '15 в 13:56
2
ответа
Скрипт для манипулирования файлами.SAT (ACIS)
Мне нужно сделать скрипт для манипулирования файлами ACIS, например: У меня есть 1 файл SAT, экспортированный из программного обеспечения CAD с 3D-моделью, и я хочу создать скрипт на каком-то языке (php, python и т. Д., Даже.BAT, если он работает), …
21 сен '15 в 15:44
1
ответ
Арифметическая операция над переменной bo3 Z3
У меня есть куча логических переменных в Z3, скажем ai, bj, а также ck, чтобы сформулировать мою проблему SAT. Однако в моей задаче есть три арифметических ограничения: a1 + a2 + a3 + ... + an = 1 b1 + b2 + b3 + ... + bn = 0 c1 + c2 + c3 + ... + cn …
28 окт '15 в 22:24
3
ответа
Упрощение формулы CNF при сохранении всех решений с определенными переменными
Связанный: упрощение CNF (фактически, я думаю, что автор этого вопроса мог быть после того, что я хочу здесь) Существует ряд инструментов для упрощения (или "предварительной обработки" перед решением) формул CNF в формате DIMACS, и большинство решат…
29 янв '17 в 22:15
3
ответа
Рандомизированные параметры с помощью System()?
Я пытаюсь попробовать некоторые рандомизированные параметры для minisat при вызове программы с помощью system(), Я никогда не делал ничего подобного раньше и должен признать, что я довольно потерян. Например, я могу сделать как: system("minisat -lub…
03 сен '16 в 01:13