Аннотация:
Пропозициональные формулы представляются вещественными матрицами так, что невыполнимость оказывается эквивалентной устойчивой неотрицательной разрешимости линейных алгебраических систем.
Как следствие, предлагается полное исчисление для порождения всех неотрицательно разрешимых линейных однородных систем.
Разрешимость системы линейных неравенств с булевыми переменными и вещественными коэффициентами сводится к выполнимости некоторой формулы и доказывается теорема об альтернативах для разрешимости таких систем.
Описывается техника неявного перебора для поиска решений не только в этих
системах, но и в широком круге дискретных оптимизационных задач. Библ. – 21 назв.