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

Планирование классов для логической выполнимости [сокращение за полиномиальное время], часть 2
Несколько дней назад я задал вопрос о том, как преобразовать проблему планирования занятий в университете в проблему логической выполнимости. ( Планирование классов до логической выполнимости [сокращение за полиномиальное время] ) Я получил...
815 просмотров
scheduling algorithm np sat np-complete
schedule 29.09.2021
Как мне скомпилировать программу расчета глюкозы SAT на Mac?
Когда я компилирую решатель глюкозы SAT на Mac, я получаю следующие ошибки времени компиляции при компиляции глюкозы 3.0. Как мне избежать этих ошибок? ~/acl2/glucose-3.0/simp$ make Making dependencies Compiling:...
517 просмотров
sat
schedule 03.10.2021
Решатель SMT с пользовательскими теориями?
Я собираюсь провести некоторую работу по проверке, в которой у меня есть регулярные древовидные грамматики в качестве базовой теории. Z3 позволяет вам определять свои собственные вещи с помощью неинтерпретируемых функций, но это не всегда хорошо...
637 просмотров
verification sat z3 smt formal-verification
schedule 17.09.2021
Как вы определяете ограничение SAT At-Most-K в OrTools
Ограничение не более k для заданного количества задач и пользователей, где заданное количество задач должно быть выполнено не более чем k количеством пользователей, каждая задача назначается только одному пользователю, у пользователя может быть...
152 просмотров
python constraints workflow or-tools sat
schedule 30.09.2021
Создание неудовлетворительных тестовых задач
Я пытаюсь создать несколько тестовых задач для пропозициональной выполнимости, в частности, чтобы сгенерировать некоторые, которые являются неудовлетворительными, но в соответствии с фиксированным шаблоном, так что для любого N может быть...
96 просмотров
language-agnostic boolean-logic sat propositional-calculus
schedule 12.03.2022
Как позволить командной строке z3 выводить режим (или ядро ​​unsat), а не sat / unsat?
z3 -smt2 <filename> выводит только "sat" или "unsat". Я хотел бы, чтобы Z3 выводил модель, если ограничение выполнено, или ненадежное ядро, если не выполнено. Какие варианты Z3 мне следует использовать?
289 просмотров
sat z3
schedule 18.03.2022
Тесты SAT на SATLIB оказались ошибочными?
Я обнаружил, что многие удовлетворительные проблемы, согласно экземплярам SATLIB SAT, фактически являются неудовлетворительными, поскольку все они содержат одно или несколько пунктов, которые имеют точную антиклазу против них. Например, приведенная...
207 просмотров
sat
schedule 30.04.2022
Удовлетворение комбинаторных ограничений и оптимизация
Проблема Я создал набор полигонов на основе мешка пересечения плоскостей. Теперь я пытаюсь создать следующее многообразие с помощью комбинаторной оптимизации. Ограничение многообразия каждое ребро в окончательной модели должно быть...
464 просмотров
python mathematical-optimization mixed-integer-programming nonlinear-optimization sat
schedule 30.04.2022
Изменить определенное слово в определенной строке
Я знаю, что об этом спрашивали несколько раз, но мне нужен быстрый способ сделать это в файлах разного размера (маленьких и больших файлах). Мне нужно отредактировать коэффициент масштабирования в файле sat(txt). Это первое число в третьей строке:...
102 просмотров
c# sat
schedule 27.06.2022
Добавление ограничений на целые биты в Z3
У меня есть целочисленная константа, скажем: expr x = ctx.int_const("x"); Я пытаюсь применить случайные ограничения к отдельным битам x. Однако оказывается, что вы не можете использовать побитовые операции с целочисленными сортировками,...
228 просмотров
c++ sat z3 smt z3py
schedule 07.08.2022
Инструмент для решения пропозициональной логики / логических выражений (SAT Solver?)
Я новичок в теме пропозициональной логики и логических выражений. Вот почему мне нужна помощь. Вот моя проблема: В автомобильной промышленности у вас есть тысячи различных вариантов компонентов, доступных на выбор при покупке автомобиля. Не все...
434 просмотров
logic boolean-logic sat boolean-expression satisfiability
schedule 26.09.2022
Как получить все удовлетворяющие задания в SMTLIB2?
Есть ли способ получить все удовлетворяющие задания, используя синтаксис SMTLIB2? Я использую решатели Z3 и CVC4.
85 просмотров
sat smt
schedule 18.08.2023
Решение уравнений с использованием логики высказываний
Я ищу идеи о том, как кодировать математические уравнения в форму cnf-sat, чтобы их можно было решить с помощью SAT-решателя с открытым исходным кодом, такого как MiniSat. Итак, как мне преобразовать что-то вроде: 3x + 4y - z = 14 -2x - 4z...
350 просмотров
logic sat smt sat-solvers bitvector
schedule 13.02.2023
Как строить литералы в решателях SAT
Я изучаю источники minisat, и здесь есть следующая встроенная функция typedef int Var; inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } который принимает на входе целое число var (целое число из...
41 просмотров
solver sat
schedule 06.06.2023
Предположения в Z3 или Z3Py
есть ли способ выразить предположения в Z3 (я использую библиотеку Z3Py), чтобы движок не проверял их достоверность, а воспринимал их как основополагающие теории, как при доказательстве теорем? Например, допустим, у меня есть две унарные функции с...
662 просмотров
sat z3 z3py satisfiability
schedule 02.11.2022
Компиляция SAT-решателя BumbleBEE
Я пытаюсь скомпилировать спутниковый решатель шмеля из http://amit.metodi.me/research/bee/ . Я уже установил SWI-Prolog и MinGW, но после ввода «make-minisat» в cmd я получаю: A subdirectory or file ..\satsolver already exists. In file...
268 просмотров
artificial-intelligence sat prolog swi-prolog sat-solvers
schedule 20.11.2022
Есть ли способ ввести Z3 Solver как обычное выражение?
Формат ввода Z3 является расширением формата, определенного стандартом SMT-LIB 2.0 . Входные выражения необходимо записывать в префиксной форме. Например, rise4fun , x + (y * 2) = 20 необходимо ввести в виде " (= (+ x (* 2 y)) 20)) ". Z3...
229 просмотров
sat z3 smt sat-solvers pysmt
schedule 20.09.2023
Как отлаживать решатель conda SAT, обрезая параметры Python до нуля?
Я наблюдаю ошибку conda install ... , в которой решатель SAT conda обрезает мои параметры для python до нуля: {snip} DEBUG conda.resolve:filter_group(400): scipy: pruned from 391 -> 127 DEBUG conda.resolve:filter_group(400): python: pruned...
456 просмотров
python dependencies conda anaconda sat
schedule 09.02.2023
Определение эквивалентности двух логических функций?
Задача Имея две логические функции f1(a,b) и f2(a,b,c) с логическими значениями a, b и c, я хотел бы знать, существует ли значение c такое, что для любых комбинаций a и b f1(a,b)=f2(a,b,c) . Например, если f1(a,b)=a AND b и f2(a,b,c)=a...
332 просмотров
sat model-checking ctl nuxmv
schedule 17.10.2022
Округление LinearExpr с помощью SAT-решателя google or-tools
Я создаю ограничение (на Java), используя or-tools SAT solver : IntVar x, y, z; IntVar[] variables = new IntVar{x, y, z}; int[] multiplier = new int{2, 3, 3}; LinearExpr expression = LinearExpr.scalProd(variables, multiplier); //2x + 3y + 3z...
246 просмотров
java or-tools nonlinear-optimization sat
schedule 24.06.2023