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

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

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

Они выглядят так:

  1. A → B ∨ C ∨ D
  2. C → ¬F
  3. F ∧ G → D
  4. ...

где «∧» = «и» / «∨» = «или» / «¬» = «не» / «→» = «импликация».

Переменные A, B, C, ... связаны с компонентами в спецификации. Имеющиеся у меня данные состоят из пар компонентов со связанными переменными.

Пример:

  1. Компонент_1, Компонент_2: (А) ∧ (В)
  2. Компонент_1, Компонент_3: (А) ∧ (С ∨ F)
  3. Компонент_3, Компонент_5: (B ∨ G)
  4. ...

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

  1. Какой инструмент, программное обеспечение и алгоритм могут решить такие проблемы?
  2. Есть наглядный пример?
  3. Как я могу автоматизировать это, чтобы проверять каждую комбинацию в моем списке?
  4. Вообще, что мне поискать в гугле, чтобы углубить свои знания в этой теме?

Спасибо большое за помощь! Олаф


logic boolean-logic sat boolean-expression satisfiability
person Olaf_SQL    schedule 18.11.2017    source источник
comment
Вы можете просмотреть список прошедших конкурсов SAT, чтобы выбрать инструмент для решения вашей собственной проблемы. Имхо, Handbook of Satisfiability — наиболее полное введение в тему, с которого вы можете начать. После того, как вы закодируете все правила, вы можете использовать так называемый поиск all-sat, чтобы перечислить все возможные модели вашей формулы, каждая из которых соответствует определенной комбинации компонентов. . Чтобы автоматизировать это, используйте какой-нибудь скрипт для создания формулы SAT. Попробуйте использовать решатель поэтапно, если это возможно в вашем случае, для повышения производительности.   -  person Patrick Trentin    schedule 26.11.2017
comment
Хорошо, большое спасибо. Тем более поиск по всем сатам наверное мне поможет.   -  person Olaf_SQL    schedule 06.12.2017
comment
Что касается AllSAT, я бы порекомендовал sharpCDCL, у меня большой положительный опыт работы с ним. , решение некоторых реальных проблем. Если вы хотите большей выразительности, рассмотрите возможность использования застежки.   -  person CaptainTrunky    schedule 13.12.2017

Ответы (1)


arrow_upward
1
arrow_downward

Возможно, вы захотите попробовать систему Prolog с помощью SAT Solver, такого как SWI-Prolog, Jekejeke Minlog и т. д., вы можете легко поиграть с ним в REPL системы Prolog. Чтобы загрузить решатель SAT, просто введите (вам не нужно вводить сам ?-):

/* in SWI-Prolog */
?- use_module(library(clpb)).

/* in Jekejeke Minlog */
?- use_module(library(finite/clpb)).

Затем вы можете использовать верхний уровень для поиска решений логической формулы, как в этом примере здесь xor:

?- sat(X#Y), labeling([X,Y]).
X = 0,
Y = 1 ;
X = 1,
Y = 0.

Вот пример кода планировщика кухни. На кухне 3 места, и мы назначаем морозильник и плиту. Морозильная камера не должна находиться рядом с плитой.

Морозильная камера имеет код 0,1, а плита — код 1,0. Мы используем ограничение карты, чтобы разместить морозильник и плиту.

:- use_module(library(finite/clpb)).

freezer([X,Y|L],[(~X)*Y|R]) :-
   freezer(L, R).
freezer([], []).

stove([X,Y|L],[X*(~Y)|R]) :-
   stove(L, R).
stove([], []).

free([X,Y|L],[(~X)*(~Y)|R]) :-
    free(L, R).
free([], []).

allowed([X,Y,Z,T|L]) :-
   sat(~((~X)*Y*Z*(~T))),
   sat(~(X*(~Y)*(~Z)*T)),
   allowed([Z,T|L]).
allowed([_,_]).
allowed([]).

kitchen(L) :-
   freezer(L, F), card(1, F),
   stove(L, G), card(1, G),
   free(L, H), card(1, H),
   allowed(L).

Что я хочу продемонстрировать с помощью кода Пролога, так это то преимущество, что кодирование задачи для формулировки SAT может быть выполнено с помощью самого кода Пролога. Когда приведенный выше код запускается, я получаю следующий результат, как и ожидалось:

?- L=[_,_,_,_,_,_], kitchen(L), labeling(L).
L = [0,1,0,0,1,0] ;
L = [1,0,0,0,0,1] ;
No
person Mostowski Collapse    schedule 19.03.2018