☰

minisat을 사용하여 SAT의 모든 솔루션을 찾으세요

tag-icon • tag-icon shell-script
minisat을 사용하여 SAT의 모든 솔루션을 찾으세요

SAT 인스턴스를 해결하기 위해 minisat을 사용하고 있습니다. 구문은 입니다 minisat inputfile outputfile. 그러나 하나의 솔루션만 반환합니다. 모든 솔루션을 찾으려면 첫 번째 솔루션의 부정을 원래 인스턴스에 추가하고 해결할 수 없게 될 때까지 다시 해결해야 합니다. 출력 파일은 다음과 같습니다.

SAT
1 -2 3 -4 5 -6 -7 0

따라서 1의 모든 자연수는 부정되거나 부정되지 않으며 그 뒤에는 0이 옵니다. 각 숫자에 -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

관련 정보