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

Question

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

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

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

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

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

Переменные A, B, C, ... связаны с компонентами в ведомости материалов. У меня есть данные, состоящие из пар компонентов с их связанными переменными.

Пример:

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

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

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

Большое спасибо за Вашу помощь! Olaf

Answer 1

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

/* 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