Вы можете заглянуть в проект Tough SAT .Это создаст экземпляры CNF SAT, которые не обязательно будут 3-SAT, но вы можете довольно легко конвертировать в 3-SAT, используя следующее сокращение из Wikipedia :
(l1 or ... or ln) -> (l1 or l2 or x2) and (not x2 or l3 or x3) and ... and (not x(n-3) or l(n-2) or x(n-2)) and (not x(n-2) or l(n-1) or ln)
Я действительнохотелось бы, чтобы они также поддерживали встроенный математический синтаксис в stackoverflow.Это обычно не противоречит другим вещам, и лучше для таких вопросов.По существу, приведенное выше сокращение добавляет новые переменные x2 - x(n-2), так что новый экземпляр 3-SAT является равносильным исходному предложению CNF SAT (т. Е. При любом назначении этих переменных условия из исходного предложения все равно будутисполняться).l1 - ln являются литералами.