☰

使用 minisat 求 SAT 的所有解

tag-icon • tag-icon shell-script
使用 minisat 求 SAT 的所有解

我正在使用 minisat 解决 SAT 实例。语法是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 = -$iawk 通过将每个数字设置为i从 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

相关内容