Я пытаюсь найти практический способ (например, с точки зрения инженерных усилий) решения проблемы, где у меня есть куча неизвестных значений: val a: Int32 = ??? val c: Int32 = ??? val d: Bool = ??? и двоичное дерево выражения (в памяти),...

Доказательство того, что SAT является NP-полным, является конструктивным доказательством, поэтому его можно реализовать в виде программы. Кто-нибудь сделал это? Я ищу программу (компилятор), которая принимает на вход программу (которая возвращает...

Из API: /* As alternative to a decision limit you can use the number of propagations * as limit. This is more linearly related to execution time. This has to * be called after 'picosat_init' and before 'picosat_sat'. */ void...

Я новичок в решении SMT, и я пишу, чтобы получить несколько советов и указателей, чтобы понять, что на самом деле является difficult constraint для решения SMT, например Z3. Я попытался настроить длину битовых векторов, например, следующим...

Я новичок в теме пропозициональной логики и логических выражений. Вот почему мне нужна помощь. Вот моя проблема: В автомобильной промышленности у вас есть тысячи различных вариантов компонентов, доступных на выбор при покупке автомобиля. Не все...

У меня такая проблема: У меня есть две пропозициональные формулы, которые должны стать логически эквивалентными. Только один из них содержит «переменную» в том смысле, что переменную можно заменить любой пропозициональной формулой. Теперь...

Вот вопрос: Рассмотрим следующие правила и определения для задачи планирования спортивной лиги: N (четных) команд, и каждые две команды играют друг с другом ровно один раз за сезон. Сезон длится (N-1) недель. Каждая команда играет одну...

В мой последний вопрос Я спросил, как я могу разобрать пропозициональное выражение, а затем найти все модели формулы с помощью библиотеки SBV. Я использовал библиотеку hatt для анализа логического выражения. К сожалению, SBV кажется, что он либо...

Как я могу получить случайную пропозициональную формулу в haskell? Предпочтительно мне нужна формула в CNF, но я бы Я хочу использовать формулы для тестирования производительности, которые также включают решатели SAT. Обратите внимание, что моей...

Учитывая массив, последовательные элементы выходного массива, где общая сумма равна 0. Например: Для ввода [2, 3, -3, 4, -4, 5, 6, -6, -5, 10], Вывод [3, -3, 4, -4, 5, 6, -6, -5] Я просто не могу найти оптимальное решение. Пояснение...

есть ли способ выразить предположения в Z3 (я использую библиотеку Z3Py), чтобы движок не проверял их достоверность, а воспринимал их как основополагающие теории, как при доказательстве теорем? Например, допустим, у меня есть две унарные функции с...

У меня есть анализатор выражений ANTLR, который может оценивать выражения формы ( A & ( B | C )) с использованием сгенерированного посетителя. A , B и C могут принимать любое из двух значений true или false . Однако я столкнулся с проблемой...

В ASP (программирование набора ответов) программы пишутся на декларативном языке более высокого уровня, а затем обосновываются детерминистическим способом для создания экземпляра ASP с использованием такого средства заземления, как lparse или гринго....