Разбиение формул
https://www.cs.cmu.edu/~mheule/publications/bcd.pdf
"We want to lift random simulation to the domain of Boolean formulas. Yet even computing a single solution is hard for most interesting Boolean formulas. Therefore we focus on computing solutions for a satisfiable subset of a Boolean formula. The main question that arises is: which subset? If the subset is too large, then solving the formula is still hard. Hence, computing many solutions to observe patterns is too costly. On the other hand, if the subset is too small, the patterns get obscured and therefore hard to detect."
И далее они там изобретают алгоритмы разбиения, и всё такое.
Если вы возьмёте программу наподобие yalsat, и запустите её на любой КНФ, то с удивлением обнаружите, что она довольно быстро доходит до процента неудовлетворённых ограничений, если не меньше. Буквально, за доли секунды.
Скорость перещёлкивания значений в yalsat в районе единиц миллионов в секунду. За секунду он пройдёт обычную сложную КНФ несколько раз. Вот сейчас запустил, для задачи в 455 тысяч ограничений yalsat добрался до 4500 неудовлетворённых ограничений за 1,02 секунды на моём медленном i7.
Далее можно выбросить неудовлетворённые решением ограничения и получить легко решаемую часть большой задачи (что и требуется), с перекосом (несбалансированностью) в 99%. А blocked clause decomposition даёт, большую часть времени, что-то в области 60-75%.
Внимание, вопрос.
Почему авторы статьи по ссылке под заголовком не сравнивали работу их алгоритмов с работой yalsat? Самое важное здесь то, что авторы yalsat пересекаются с авторами статьи.
Леность ума поразительная.
PS
По задаче можно пройти один раз (по каждому неудовлетворённому ограничению). Оставив это решение и отбросив все неудовлетворённые ограничения, мы получаем легко решаемую подзадачу.
"We want to lift random simulation to the domain of Boolean formulas. Yet even computing a single solution is hard for most interesting Boolean formulas. Therefore we focus on computing solutions for a satisfiable subset of a Boolean formula. The main question that arises is: which subset? If the subset is too large, then solving the formula is still hard. Hence, computing many solutions to observe patterns is too costly. On the other hand, if the subset is too small, the patterns get obscured and therefore hard to detect."
И далее они там изобретают алгоритмы разбиения, и всё такое.
Если вы возьмёте программу наподобие yalsat, и запустите её на любой КНФ, то с удивлением обнаружите, что она довольно быстро доходит до процента неудовлетворённых ограничений, если не меньше. Буквально, за доли секунды.
Скорость перещёлкивания значений в yalsat в районе единиц миллионов в секунду. За секунду он пройдёт обычную сложную КНФ несколько раз. Вот сейчас запустил, для задачи в 455 тысяч ограничений yalsat добрался до 4500 неудовлетворённых ограничений за 1,02 секунды на моём медленном i7.
Далее можно выбросить неудовлетворённые решением ограничения и получить легко решаемую часть большой задачи (что и требуется), с перекосом (несбалансированностью) в 99%. А blocked clause decomposition даёт, большую часть времени, что-то в области 60-75%.
Внимание, вопрос.
Почему авторы статьи по ссылке под заголовком не сравнивали работу их алгоритмов с работой yalsat? Самое важное здесь то, что авторы yalsat пересекаются с авторами статьи.
Леность ума поразительная.
PS
По задаче можно пройти один раз (по каждому неудовлетворённому ограничению). Оставив это решение и отбросив все неудовлетворённые ограничения, мы получаем легко решаемую подзадачу.