![使用 minisat 求 SAT 的所有解](https://linux22.com/image/39831/%E4%BD%BF%E7%94%A8%20minisat%20%E6%B1%82%20SAT%20%E7%9A%84%E6%89%80%E6%9C%89%E8%A7%A3.png)
我正在使用 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 = -$i
awk 通过将每个数字设置为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