Описание тега satisfiability

Описание тега Вопросы с тегом
Выполнимость (часто пишется заглавными буквами или сокращенно SAT) - это проблема определения, можно ли присвоить переменным данной булевой формулы таким образом, чтобы формула оценивалась как ИСТИНА.
1 ответ

Как выполнять SAT-вызовы параллельно, используя привязки haskell picosat?

import Picosat import Control.Applicative main :: IO () main = do dimacsList1 <- (read <$> getLine) :: IO [[Integer]] dimacsList2 <- (read <$> getLine) :: IO [[Integer]] res1 <- solve dimacsList1 res2 <- solve dimacsList2 put…
25 май '14 в 15:55
2 ответа

Решение SAT с библиотекой haskell SBV: как создать предикат из проанализированной строки?

Я хочу разобрать String это изображает формулу высказывания, а затем найти все модели формулы высказывания с помощью решателя SAT. Теперь я могу разобрать пропозициональную формулу с пакетом hatt; увидеть testParse функция ниже. Я также могу запусти…
23 апр '14 в 02:55
2 ответа

Поддерживает ли стандарт SMT-Lib сочетание теорий?

Я знаю, что несколько работ пытаются справиться с сочетанием теорий в SMT. Однако язык SMT-Lib 2.0 ( http://smtlib.cs.uiowa.edu/docs.html) ничего не говорит об этом. У меня вопрос, поддерживает ли он это, и что Солверс предлагает способность работат…
31 май '13 в 19:19
1 ответ

Минисат, как найти все решения SAT эффективно

Я нашел способ найти все решения, используя способ, описанный в этой ссылке. Это работает нормально, но медленно. Поскольку он пересчитывает ограничения с самого начала, i_e не использует преимущества предыдущих вычислений. Теперь, по этой ссылке, я…
14 окт '14 в 13:20
2 ответа

Разобрать строку с формулой высказываний в CNF для вложенного списка DIMACS int в haskell

Я хотел бы проанализировать строку с формулой высказываний в CNF для DIMACS, таким образом, вложенный список int в haskell. Формат подходит для привязок пикосата haskell, которые кажутся более производительными, чем другие варианты решения SAT. Проб…
18 май '14 в 05:58
1 ответ

SAT-решение системы одноразовых ограничений

Я пытаюсь решить проблему SAT, которая состоит только из горячих ограничений. Прямо сейчас я использую горячую кодировку, предложенную Клессеном в гл. 4.2 из [1] и MiniSAT. Интересно, есть ли лучший способ решения такой проблемы, например, класс реш…
28 май '13 в 05:29
2 ответа

Разница между C-SAT и SAT?

В чем именно разница между этими двумя NP-полными задачами? Мне кажется, что они оба спрашивают, может ли быть выполнена булева формула (т.е. вывод 1), но один находится в контексте схемы, а другой - просто формула. Однако нельзя ли написать булеву …
21 май '17 в 23:54
1 ответ

Является ли минимизация логических выражений NP-Complete?

Я знаю, что логическая выполнимость является NP-Complete, но является ли минимизация / упрощение логического выражения, что я имею в виду, принимая данное выражение в символической форме и производя эквивалентное, но упрощенное выражение в символиче…
01 мар '09 в 16:42
1 ответ

Доза SMTLIB 1.2 имеет (get-value) функцию, подобную SMTLIB 2

Интересно, если SMTLIB1.2 имеет эквивалент SMTLIB2s (get-value). Я бегаю по другому SMT тесты кодирования с использованием Z3 SMT solver а также SMTLIB1.2проблема в выводе, я продолжаю получать все значения, модели смешанные с сотнями значений вспом…
04 авг '14 в 12:22
2 ответа

Сделать ограничение труднее решить для решателя ограничений?

Я новичок в решении SMT, и я пишу, чтобы узнать некоторые советы и указатели, чтобы понять, что на самом деле difficult constraint для решения SMT, например Z3. Я попытался настроить длину битовых векторов, например, следующим образом: >>> …
28 янв '19 в 17:23
1 ответ

SAT для формулы LTL

SAT-решатель доказывает выполнимость пропозициональной формулы F. Однако возможно ли использовать SAT для проверки выполнимости формулы LTL? Например, можем ли мы доказать, что следующая формула LTL неудовлетворительна? G (A => B) и (A = True) и (B …
20 авг '14 в 13:05
0 ответов

Удовлетворенность булевой формулы - решение с минимальным количеством переменных, установленным в True

У меня возникли проблемы с созданием псевдокода для решения проблемы булевой выполнимости с использованием минимального количества переменных, установленного в значение true. У меня есть метод выполнимого числа (H), который я могу вызвать, чтобы пол…
10 ноя '16 в 07:04
4 ответа

Разделите людей на команды для наибольшего удовлетворения

Просто вопрос любопытства. Помните, когда в групповой работе профессор делил людей на группы определенного числа (n)? Некоторые из моих профессоров возьмут список n люди, с которыми хочется работать и n людей, с которыми не хочется работать, от кажд…
16 май '10 в 20:24
1 ответ

Picosat SAT solver: установить предел распространения - но какое значение?

Из 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 picosat_set_propagation_…
09 ноя '13 в 00:33
1 ответ

Теорема Кука (простым языком)

Я прочитал книгу Garey and Johnson " Компьютеры и непроницаемость - руководство по теории NP- полноты" для курса по алгоритмам; однако, просмотрев материал год спустя, я понял, что никогда не понимал теорему Кука. Что касается доказательства, я пони…
02 окт '14 в 18:30
1 ответ

Конвертировать Булевы плоские цинковые в CNF DIMACS

Чтобы решить систему булевых уравнений, я экспериментирую с Constraint-Programming Solver MiniZinc использует следующий вход: % Solve system of Brent's equations modulo 2 % Matrix dimensions int: aRows = 3; int: aCols = 3; int: bCols = 3; int: noOfP…
13 мар '14 в 22:20
0 ответов

CVC4: использование квантификаторов в интерфейсе C++

Я пытаюсь понять, как кодировать квантификаторы в CVC4, используя интерфейс C++. Вот пример, который я пытаюсь запустить, но не могу. int main() { SmtEngine smt(&em); smt.setLogic("AUFLIRA"); // Set the logic Expr three = em.mkConst(Rational(3))…
29 ноя '14 в 02:15
2 ответа

Пример неполноты GSAT

Алгоритм GSAT (Greedy Satisfiability) может быть использован для поиска решения проблемы поиска, закодированной в CNF. Я знаю, что, поскольку GSAT является жадным, он неполон (что означает, что могут быть случаи, когда решение может существовать, но…
27 фев '14 в 05:15
1 ответ

Инструмент для решения логики высказываний / логических выражений (SAT Solver?)

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

Как представить отрицательное число в битвекторе?

Название говорит само за себя. Я пытаюсь представить -1 как следующее: (_ bv-1 32)и z3 жалуется. Как мне представить такое ограничение, как 3x - 5y <= 10 в битовом векторе? По какой-то причине я не хочу использовать линейное целое число.
05 май '16 в 06:57