MiniSat - довольно старая программа на данный момент. По крайней мере, вы должны взглянуть на одного из решателей, участвовавших в недавнем конкурсе SAT , например, Глюкоза . Соревнования требовали, чтобы решатели SAT выдавали DRAT-доказательства неудовлетворенности с 2013 года. Запустите любой решатель, который вы выберете, и пусть он сбросит свое DRAT-доказательство в proof.out. Ввести proof.out в утилиту drat-trim с опцией - c, которая создаст ядро UNSAT в формате DIMACS. Т.е.
drat-trim originalproblem.cnf proof.out -c core.cnf
Обратите внимание, что вам не нужно использовать клон MiniSat; Любой современный решатель, который испускает доказательства DRAT, может получать свои доказательства в drat-trim, чтобы получить ядро UNSAT.