☰

minisatを使用してSATのすべてのソリューションを見つけます

tag-icon • tag-icon shell-script
minisatを使用してSATのすべてのソリューションを見つけます

私は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数値行を否定する操作を実行します。

答え2

Wumpus Q. Wumbleyのスクリプトを便利にするためにいくつか修正しました。また、ソリューションの数を表示するカウンタを追加し、冗長なMINISAT出力をミュートし、入力ファイルを保存するために一時ファイルにいくつかの重要ではないパイプを追加しました。最後に、出力ファイルを提供する必要があるという要件が排除されるため、コマンドラインからSCRIPTNAME FILENAMEと呼ぶことができます。

#!/bin/sh
SOLUTIONS=0
cp $1 /tmp/tmpsat
while :; do

  minisat -verb=0 /tmp/tmpsat /tmp/tmpout > /tmp/tmpmsg 2> /tmp/tmpmsg

  if [ `head -1 /tmp/tmpout` = UNSAT ]; then
    break
  fi
 SOLUTIONS=$((SOLUTIONS + 1))
  tail -1 /tmp/tmpout |
    awk '{
      for(i=1;i<NF;++i) { $i = -$i }
      print
    }' >> /tmp/tmpsat

done

echo There are $SOLUTIONS solutions.
rm -f /tmp/tmpsat
rm -f /tmp/tmpout
rm -f /tmp/tmpmsg

関連情報