どうでもいいが>>896とかはクソな問題で有名な
3−SATの亜種じゃね?