Use minisat para encontrar todas as soluções para o SAT

Question

Estou resolvendo instâncias de SAT usando minisat. A sintaxe é minisat inputfile outputfile . No entanto, só retorna uma solução. Para encontrar todas as soluções, devo anexar a negação da primeira solução à instância original e resolvê-la novamente até que fique insolúvel. O arquivo de saída é assim:

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

Assim, cada número natural de um para qualquer um é negado ou não-seguido seguido de um 0. Preciso multiplicar cada número por -1 e acrescentar essa (última) linha (incluindo 0) ao final de inputfile e faça um loop até a primeira linha de outputfile é UNSAT .

    

Answer 1

Eu fiz algumas modificações no script do Wumpus Q. Wumbley para torná-lo útil. Mais importante, adicionei um contador para exibir o número de soluções e silenciei a saída detalhada do MINISAT, além de adicionar alguns canais importantes aos arquivos temporários para preservar os arquivos de entrada. Por fim, elimina o requisito de fornecer um arquivo de saída para que você possa chamá-lo de SCRIPTNAME FILENAME na linha de comando.

#!/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

    

Answer 2

Este script faz o que você pergunta:

#!/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

O awk faz o trabalho de negar a linha de números definindo $i = -$i para cada i de 1 para NF (Number of Fields).