#data-structures #sat #bitflags
Вопрос:
Глядя на общие кодовые базы для 3SAT, такие как Z3, кажется, что предложения обычно представляются в виде троек переменных, возможно, отрицаемых. Однако другое возможное представление состоит в том, чтобы упаковать каждое предложение в байт, где каждый бит байта представляет одну из восьми возможных комбинаций отрицаний. Когда два предложения имеют одинаковые переменные, они используют один и тот же байт. Это похоже на умную и экономичную кодировку; используют ли ее какие-либо решатели SAT?
Комментарии:
1. Предложения обычно представлены в виде массива
u32/unsigned, выделенного как часть предложения с элементом гибкой длины. См. Строку 56 в вашей ссылке Z3. Большинство решателей SAT не работают в (строгом) 3-SAT, только в общем SAT.2. Я думаю, что большинство решателей SAT имеют специальные структуры данных для двоичных, троичных и n-арных предложений. Ваш байт, похоже, хранит только знак 3 переменных, а не сами переменные ? Вам все еще нужно хранить сами переменные, верно ? Кроме того, важна компактность, но необходимо учитывать и другие вещи, такие как расположение памяти, пропуски кэша и, конечно, схема 2-х букв. Я не знаю, можно ли решить эти проблемы с помощью вашего подхода, поскольку я не совсем понимаю ваш подход. Не могли бы вы подробнее рассказать ?
3. @Corbin, Но не означает ли это, что ваш ключ/индекс в этой структуре данных имеет размер 3*(переменная). Я не уверен в хэш-картах, но разве это не означает, что вы храните тот же объем памяти, что и раньше?
4. @Корбин, будучи новым, не избавляет от необходимости в доработке. 🙂 На первый взгляд все еще неясно, как вы можете перейти от байта (1 из 256 возможных значений) к любому количеству значений (8 * (n выбирает 3) для 3-SAT). В этом пункте требуется больше информации, чем это, верно? Что еще более важно, горячая точка для распространения единиц находится в пропусках кэша для извлеченных предложений — наличие двойного косвенного обращения будет иметь значительное влияние на производительность, и можно склониться к тому, чтобы встроить литералы в предложение/как можно ближе к часам. Вот почему двоичные предложения обычно хранятся непосредственно в списках наблюдения.
5. @Корбин Понял Тебя. Проблема, с которой вы столкнетесь, заключается в том, что «Обучающие предложения выполняются путем установки битов внутри структуры, но не выделения нового пространства». Изученные предложения не обязательно являются 3SAT. На самом деле они обычно немного длиннее этого — поэтому, чтобы преобразовать их в 3SAT, вам нужно добавить больше вспомогательных переменных, что, в свою очередь, требует увеличения количества переменных в три раза.