Вопросы по теме 'sat'

Планирование классов для логической выполнимости [сокращение за полиномиальное время]
У меня есть теоретическая / практическая проблема, и я пока не знаю, как ею управлять. Вот она: Я создаю решатель SAT , способный найти существующую модель и доказать противоречие. когда это не относится к проблемам CNF в C с использованием...
4562 просмотров
c scheduling algorithm sat reduction
schedule 29.04.2023
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)...
168 просмотров
solver sat z3 smt
schedule 13.04.2022
Решение SAT с более чем 2 ^ 32 пунктами
Я пытаюсь решить большую формулу CNF , используя SAT solver . В формуле (в формате DIMACS ) есть предложения 4,697,898,048 = 2^32 + 402,930,752 , и все решатели SAT, которые я мог find испытывают проблемы с этим: (P) lingeling...
577 просмотров
c integer-overflow sat sat-solvers
schedule 12.12.2021
Решатель Prolog SAT методом грубой силы для логических формул
Я пытаюсь написать алгоритм, который наивно ищет модели булевой формулы (NNF, но не CNF). Код, который у меня есть, может проверить существующую модель, но он не завершится (или не завершится), когда его попросят найти модели, по-видимому, потому,...
671 просмотров
sat prolog clpb
schedule 28.09.2022
Вычислимость: формула SAT с ограниченным числом предложений
Определите SAT2016 = {\phi | \phi — формула CNF с не более чем 2016 пунктами}. Если предположить, что P\neq NP, является ли SAT2016 NP-полным? Поскольку количество литералов в каждом предложении не ограничено, не сразу ясно, существует ли...
244 просмотров
sat computability
schedule 28.10.2022
Почему WSAT лучше имитации отжига?
в каком-то журнале я прочитал, что алгоритм WSAT (Walking SAT) имеет лучшие характеристики, чем алгоритм имитации отжига, в решении проблемы SAT. Итак, мой вопрос: может ли кто-нибудь объяснить, почему мы получили такой результат? Может быть...
189 просмотров
artificial-intelligence algorithm sat simulated-annealing wsat
schedule 18.02.2023
время, затраченное на разбор и упрощение файла CNF
Я только начинаю использовать библиотеки Sat4j. Можете ли вы указать мне, как рассчитать время, необходимое для анализа и упрощения данного ввода CNF. я использовал ISolver solver = SolverFactory.newDefault(); Reader reader = new...
115 просмотров
java sat sat4j
schedule 29.07.2023
Добавление предложений непосредственно в решатель z3
У меня есть AIG (и граф инвертора), который я продолжаю модифицировать, и чью работоспособность мне нужно проверять поэтапно с помощью Z3. Я могу сгенерировать CNF-представление AIG и в идеале хотел бы передать эти предложения непосредственно в...
168 просмотров
c c++ sat z3
schedule 11.12.2022
Решатель SAT устанавливает результат по умолчанию (cryptominisat)
Я моделирую проблему с SAT и пытаюсь решить ее с помощью cryptominisat . Я хотел бы дать моей переменной значение по умолчанию, если для нее нет ограничений. Я просмотрел руководство, и set_default_polarity кажется ответом. Я попробовал это,...
127 просмотров
logic solver sat
schedule 12.12.2022
Процедура алгоритма DPLL
Я пытаюсь понять процедуру DPLL, прежде чем ее кодировать. Например, у меня есть такие пункты: C1 : {c, !d, !b} C2 : {d, a} C3: {b, !d, !a} C4: {d, c, b, a} C5: {c, !d, !b} C6: {d, c, b} C7: {c} Теперь я принимаю...
498 просмотров
authentication algorithm sat satisfiability dpll
schedule 21.03.2022
SMT/SAT Solver и средство проверки моделей
Недавно я начал изучать методы формальной проверки. В литературе модуль проверки и решатель используются как взаимозаменяемые. Но как связаны друг с другом средство проверки моделей и решатель? p.s. Я был бы признателен, если бы некоторые...
1207 просмотров
solver sat smt model-checking
schedule 26.03.2023
/usr/bin/ld: не удается найти -lcplex
Я пытаюсь настроить решатель MaxHS SAT из этого репозитория git - https://github.com/fbacchus/MaxHS . Я получаю сообщение об ошибке «/usr/bin/ld: не удается найти -lcplex». Может ли кто-нибудь рассказать мне, что такое библиотека lcplex и как...
1325 просмотров
c++ cplex sat sat-solvers
schedule 09.03.2023
Есть ли какой-либо инструмент, который реализует решатель SAT, отличный от CNF?
Мне нужен решатель SAT, способный принимать в качестве входных данных не только файлы CNF, но и обычные файлы txt, содержащие пропозициональные предложения (написанные только с и или и нет ). Я не мог найти ни одного. Не могли бы вы указать...
402 просмотров
sat sat-solvers cnf
schedule 10.11.2022
Снижение доступности графов до SAT (CNF)
Вот и я столкнулся с этой проблемой в своем учебнике. Мне было интересно, как свести проблему доступности графа к проблеме SAT (CNF). (т.е. формула выполнима, если существует путь в графе G от начала до конца узла) 1) Я не могу понять, как...
355 просмотров
graph algorithm sat
schedule 07.07.2023
Как использовать CNF для описания сложения
Во многих статьях используется SAT, но мало кто упоминает, как преобразовать дополнение в CNF. Поскольку CNF допускает только операцию AND OR NOT, описать операцию сложения сложно. Например, x1 + x2 + x3 + ... +x1599 < 30, xi is binary....
90 просмотров
addition sat conjunctive-normal-form
schedule 24.08.2022
нахождение максимального числа чисел в z3 с использованием SMTLIB2
У меня есть 7 чашек, в которых есть немного воды. Мне нужно запрограммировать эти чашки на разное количество воды. Как только это будет сделано, мне нужно измерить чашку, в которой больше всего воды, а затем удалить некоторое количество (скажем, 2...
254 просмотров
python sat z3 satisfiability
schedule 13.12.2023
Несовместимая выполнимость между ctx-solver-simplify и ctx-simplify Z3
Я пытаюсь сделать z3 (я использую z3py), чтобы проверить, выполнима ли формула или нет, и если она выполнима, то упростить ее. Сначала я использовал Z3 ctx-solver-simplify . Однако, поскольку я постоянно делаю много звонков, использование этой...
72 просмотров
sat z3 z3py simplification satisfiability
schedule 05.02.2023
Ядро Unsat в Minisat
Есть ли какой-либо вызов API в minisat для извлечения ядра unsat или любого другого метода для того же. Я хочу извлекать ядро ​​unsat для каждого вызова решателя, а затем работать с ядром unsat.
222 просмотров
constraint-programming sat sat-solvers
schedule 12.02.2023
Какова основная причина того, что при использовании алгоритма CDCL для SAT забывают предложения в булевой формуле?
Алгоритм Conflict Drive Learning Clause Learning использует компонент обратного отслеживания, который основан на «изучении» новых предложений (полученных при достижении конфликта в процессе поиска присваивания истинности, удовлетворяющего булевой...
26 просмотров
algorithm sat
schedule 18.08.2022
Округление Non-LinearExpr с помощью SAT-решателя google or-tools
Используя CP-SAT Google or-tools , я пытаюсь напишите это ограничение: q >= (50x + 100y + 150z + 200k + 250p + 300v) / (x + y + z + k + p + v) Где q - простое целое число. Дело в том, что мне нужно округлить правую часть уравнения...
235 просмотров
optimization or-tools nonlinear-optimization sat
schedule 24.02.2023