私はSATインスタンスを解決するためにminisatを使用しています。構文はですminisat inputfile outputfile。ただし、1つの解決策のみを返します。すべてのソリューションを見つけるには、最初のソリューションの否定を元のインスタンスに追加して解決できなくなるまで再解決する必要があります。出力ファイルは次のとおりです。
SAT
1 -2 3 -4 5 -6 -7 0
したがって、1のすべての自然数は否定または否定されず、その後にゼロが続きます。各数字に-1を掛け、対応する（最後の）行（0を含む）を最後に追加し、inputfile最初の行にoutputfileなるまで繰り返す必要がありますUNSAT。
ベストアンサー1
このスクリプトはあなたが要求したことを行います。
#!/bin/sh
while :; do
minisat inputfile outputfile
if [ `head -1 outputfile` = UNSAT ]; then
break
fi
tail -1 outputfile |
awk '{
for(i=1;i<NF;++i) { $i = -$i }
print
}' >> inputfile
done
$i = -$iiawkは、各数値を1から（フィールド数）に設定して、NF数値行を否定する操作を実行します。