gophersat
1.0.0
Este é o Gophersat, um solucionador SAT e pseudo-booleano escrito puramente em Go. Gophersat foi desenvolvido pelo CRIL (Centre de Recherche en Informatique de Lens) da Universidade Artois e CNRS. É lançado sob a licença do MIT. O Gophersat é bastante eficiente, ou seja, em benchmarks SAT típicos, ele funciona cerca de 2 a 5 vezes mais devagar do que os solucionadores de nível superior (ou seja, glicose ou minisat), nos quais é fortemente inspirado. Ele também pode resolver problemas MAXSAT e problemas pseudo-booleanos de decisão e otimização.
A última versão estável do Gophersat é a versão 1.4. Inclui a estratégia opcional de resolução de planos de corte.
Alguns problemas, como o famoso problema do pombo, levam muito tempo para serem resolvidos usando o raciocínio lógico puro.
O problema dos pombos pode ser expresso desta forma: é possível colocar n pombos em m pombos, onde m = n-1, sem colocar vários pombos na mesma cova e colocar todos os pombos em uma cova? A resposta é óbvia: se você tem 4 pombos em 3 buracos, não pode colocá-los todos em um buraco diferente. Mas como você prova isso? Um solucionador SAT ou PB provará isso tentando todas as combinações possíveis, e o número de combinações possíveis cresce exponencialmente. Portanto, tentar resolver o problema com n=20 não é viável na prática, apesar do problema ter uma resposta óbvia.
Alguns solucionadores de OP implementam uma estratégia alternativa: a estratégia de planos de corte. Não será descrito em detalhes neste documento, mas esta estratégia pode ser extremamente eficiente em alguns problemas, como o problema do pombo, que não pode ser resolvido eficientemente por raciocínio lógico puro, mas será mais lento na maioria dos problemas.
Agora é possível utilizar os planos de corte com o Gophersat. Basta usar a opção de linha de comando -cp . Então, em vez de ligar:
gophersat problem.opb
Basta ligar:
gophersat -cp problem.opb
A última versão estável do Gophersat é a versão 1.3. É uma pequena atualização que adiciona a capacidade de acessar o solucionador subjacente ao lidar com problemas de MAXSAT.
Gophersat versão 1.2 inclui uma maneira de entender instâncias UNSAT, fornecendo certificados RUP quando um problema é UNSAT e fornecendo a capacidade de extrair subconjuntos insatisfatórios da fórmula. Vários bugs também foram corrigidos e o suporte para resolução incremental de SAT foi melhorado.
Para saber mais sobre essas funcionalidades, você pode conferir o tutorial sobre certificados UNSAT e MUSes.
Para gerar um certificado com o executável gophersat, basta chamar:
gophersat -certified problem.cnf
O certificado será então impresso na saída padrão, utilizando a notação RUP. O certificado é gerado dinamicamente, portanto, esteja ciente de que um certificado parcial e inútil será gerado mesmo que o problema seja realmente solucionável. Esta é uma prática comum na comunidade e, embora as cláusulas geradas sejam ruídos inúteis, na prática isso não é um problema.
Para extrair um MUS de uma instância UNSAT, basta chamar:
gophersat -mus problem.cnf
O MUS será impresso na saída padrão. Se o problema não for UNSAT, uma mensagem de erro será exibida.
No momento, essas facilidades estão disponíveis apenas para problemas SAT puros (ou seja, não para problemas pseudo-booleanos).
Desde sua versão 1.1, Gophersat inclui um solucionador central novo e mais eficiente para problemas SAT puros e um pacote que trata de problemas MAXSAT. Também inclui uma nova API para otimização e contagem de modelos, onde novos modelos são gravados nos canais assim que são encontrados.
Desde a versão 1.0, a API do Gophersat é considerada estável, o que significa que a API tem garantia de compatibilidade com versões anteriores até uma grande mudança de versão. Em outras palavras, se o seu programa funcionar com a versão 1.0 do gophersat, ele ainda funcionará com a versão 1.1 ou superior, mas não necessariamente com versões superiores a 2.0.
Observe que, por "ainda funcionando", queremos dizer apenas "compilará e produzirá a mesma saída", e não "terá o mesmo desempenho em termos de memória ou tempo". Esta é uma distinção importante: durante atualizações de versões secundárias, novas heurísticas ou tipos de dados podem ser introduzidos, o que significa que alguns problemas podem ser resolvidos mais rapidamente ou mais lentamente do que antes.
go get github.com/crillab/gophersat && go install github.com/crillab/gophersat
Gophersat pode ser usado como um solucionador independente (leitura de arquivos DIMACS CNF) ou como uma biblioteca em qualquer programa Go.
Para resolver um arquivo DIMACS, você pode chamar gophersat com a seguinte sintaxe:
gophersat --verbose file.cnf
onde --verbose é um parâmetro opcional que faz com que o solucionador exiba informações durante o processo de resolução.
Gophersat também é capaz de ler e resolver fórmulas booleanas mais gerais, não apenas problemas representados no formato DIMACS hostil ao usuário. Também lida nativamente com restrições de cardinalidade, ou seja, cláusulas que devem ter pelo menos n literais verdadeiros, com n > 1.
Gophersat pode ser usado como um solucionador independente (leitura de arquivos OPB) ou como uma biblioteca em qualquer programa Go.
Para resolver um problema pseudo-booleano (seja de decisão ou de otimização), você pode chamar gophersat com a seguinte sintaxe:
gophersat --verbose file.opb
onde --verbose é um parâmetro opcional que faz com que o solucionador exiba informações durante o processo de resolução.
No momento, ele só pode resolver os chamados problemas DEC-SMALLINT-LIN e OPT-SMALLINT-LIN, ou seja, problemas de decisão (existe solução ou não), para restrições lineares (uma soma de literais ponderados) em inteiros pequenos (n < 2^30), ou problemas de otimização (qual é a melhor solução, minimizando uma determinada função de custo), para restrições lineares em inteiros pequenos.
Graças ao pacote maxsat , Gophersat agora pode resolver problemas de MAXSAT.
Para resolver um problema de MAXSAT ponderado, você pode chamar gophersat com a seguinte sintaxe:
gophersat --verbose file.wcnf
onde --verbose é um parâmetro opcional que faz com que o solucionador exiba informações durante o processo de resolução. O arquivo deve ser representado no (formato WCNF)[http://www.maxsat.udl.cat/08/index.php?disp=requirements].
SAT, que significa Problema de Satisfiabilidade Booleana , é o problema canônico NP-completo, ou seja, um problema para o qual não existe solução conhecida que não leve tempo exponencial no pior caso. Em poucas palavras, um solucionador SAT tenta encontrar, para uma dada fórmula proposicional, uma atribuição para todas as suas variáveis que a torne verdadeira, se tal atribuição existir.
Embora seja trivial implementar um solucionador SAT usando um algoritmo ingênuo, tal implementação seria muito ineficiente na prática. Gophersat implementa recursos de última geração e, portanto, é bastante eficiente, tornando-o utilizável na prática em programas Go que necessitam de um mecanismo de inferência eficiente.
Embora esta nem sempre seja a melhor decisão por razões práticas, qualquer problema NP-completo pode ser traduzido como um problema SAT e resolvido pelo Gophersat. Tais problemas incluem o problema do caixeiro viajante, programação de restrições, problema da mochila, planejamento, verificação de modelo, verificação de correção de software, etc.
Mais sobre o problema do SAT pode ser encontrado no artigo da Wikipedia sobre o SAT.
Você também pode encontrar informações sobre como representar suas próprias fórmulas booleanas para que possam ser usadas pelo gophersat no tutorial "SAT para novatos".
MAXSAT é o equivalente de otimização do problema de decisão SAT. Embora um solucionador SAT puro retorne um modelo que satisfaça todas as cláusulas ou UNSAT se tal modelo não existir, um solucionador MAXSAT retornará um modelo que satisfaça tantas cláusulas quanto possível.
Existem extensões para MAXSAT.
MAXSAT parcial significa que, embora queiramos satisfazer o maior número possível de cláusulas, algumas cláusulas (chamadas cláusulas rígidas ) devem ser satisfeitas, não importa o que aconteça. Um problema parcial de MAXSAT pode, portanto, ser declarado insatisfatório.
Por exemplo, gerar um horário para uma escola é um problema parcial do MAXSAT: há tanto o soft (queremos ter o menor número possível de aulas que comecem depois das 16h, por exemplo) quanto o hard (dois professores não podem estar em dois lugares diferentes ao mesmo tempo). ao mesmo tempo) restrições.
MAXSAT ponderado significa que as cláusulas estão associadas a um custo: embora opcionais, algumas cláusulas são consideradas mais importantes que outras. Por exemplo, se a cláusula C1 tiver um custo de 3 e as cláusulas C2 e C3 tiverem ambas um custo de 1, uma solução que satisfaça C1, mas nem C2 nem C3, será considerada melhor do que uma solução que satisfaça C2 e C3, mas não C1, todas as outras coisas sendo iguais.
MAXSAT parcialmente ponderado significa que existem cláusulas flexíveis e rígidas no problema, e as cláusulas flexíveis são ponderadas. A este respeito, MAXSAT "puro" é um caso particular do MAXSAT parcial ponderado mais genérico: um problema MAXSAT "puro" é um problema MAXSAT parcial ponderado onde todas as cláusulas são cláusulas suaves associadas a um peso de 1.
Problemas pseudo-booleanos são, de certa forma, uma generalização dos problemas SAT: qualquer cláusula proposicional pode ser escrita como uma única restrição pseudo-booleana, mas representar uma restrição pseudo-booleana pode exigir um número exponencial de cláusulas proposicionais.
Uma expressão pseudo-booleana (linear) é uma expressão como:
w1 l1 + w2 x2 + ... + wn xn ≥ y
onde y e todos wi são constantes inteiras e todos li são literais booleanos.
Por exemplo, para que a seguinte expressão seja verdadeira
2 ¬x1 + x2 + x3 ≥ 3
a variável booleana x1 deve ser falsa e pelo menos um de x2 e x3 deve ser verdadeiro. Isso é equivalente à fórmula proposicional
¬x1 ∧ (x2 ∨ x3)
Expressões pseudo-booleanas são uma generalização de cláusulas proposicionais: qualquer cláusula
x1 ∨ x2 ∨ ... ∨ xn
pode ser reescrito como
x1 + x2 + ... + xn ≥ 1
A descrição de um problema pseudo-booleano pode ser exponencialmente menor do que sua contraparte proposicional, mas a resolução de um problema psudo-booleano ainda é NP-completa.
Gophersat resolve problemas de decisão (existe alguma solução para o problema) e problemas de otimização. Um problema de otimização é um problema pseudo-booleano associado a uma função de custo, ou seja, uma soma de termos que devem ser minimizados. Em vez de apenas tentar encontrar um modelo que satisfaça as restrições dadas, o gophersat tentará então encontrar um modelo que garanta tanto a satisfação das restrições quanto a minimização da função de custo.
Durante a busca por essas soluções ótimas, o gophersat fornecerá soluções subótimas (ou seja, soluções que resolvem todas as restrições, mas ainda não são garantidas como ótimas) assim que as encontrar, para que o usuário possa obter uma solução subótima em um determinado tempo limite ou espere mais pela solução ótima garantida.
Sim e não. É muito mais rápido do que implementações ingênuas, rápido o suficiente para ser usado em problemas do mundo real, mas mais lento do que solucionadores de última geração, altamente otimizados e de nível superior.
Gophersat não pretende ser o solucionador SAT/PB mais rápido disponível. O objetivo é dar acesso às tecnologias SAT e PB aos gophers, sem recorrer a interfaces para solucionadores escritos em outras linguagens (normalmente C/C++).
Entretanto, em alguns casos, a interface com um solucionador escrito em outra linguagem é a melhor escolha para sua aplicação. Se você tiver muitos pequenos problemas para resolver, o Gophersat será a alternativa mais rápida. Para problemas maiores, se você quiser ter o mínimo de dependências possível em detrimento do tempo de resolução, o Gophersat também é bom. Se você precisa resolver problemas difíceis e não se importa em usar o cgo ou um programa externo, o Gophersat provavelmente não é a melhor opção.
Existem alguns outros solucionadores de SAT em Go, principalmente go-sat e gini. O desempenho do Gini está praticamente no mesmo nível do Gophersat, embora um pouco mais lento em média, de acordo com os testes que realizamos.
Gophersat também fornece recursos interessantes nem sempre disponíveis em outros solucionadores (um formato de entrada amigável, por exemplo), para que possa ser usado como uma ferramenta para descrever e resolver problemas NP-difíceis que podem ser facilmente reduzidos a um SAT/PB problema.
Não. O pacote bf (para "fórmula booleana") fornece facilidades para traduzir qualquer fórmula booleana para CNF.
Isso é conhecido como contagem de modelos e, sim, existe uma função para isso: solver.Solver.CountModels .
Você também pode contar modelos na linha de comando, com
gophersat --count filename
onde filename pode ser um arquivo .opb ou .cnf.
