Levantamento de transformações relacionadas ao uso de solucionadores SAT

13

Estou começando a investigar a possibilidade de contar com um solucionador SAT para resolver um problema de otimização que me interessa e atualmente estou procurando uma pesquisa que contenha exemplos de transformações "inteligentes" em variantes de SAT (ou seja, transformações resultantes em um problema de tamanho razoável, já que não estou interessado em provar resultados de dureza, mas em resolver o problema), aproximadamente no espírito do que pode ser encontrado na pesquisa de gráficos cúbicos de Greenlaw e Petreschi , se houver alguma comparação. feito entre os dois.

Essa pesquisa me escapou porque não existe, ou porque eu simplesmente perdi?

ds.algorithms reference-request sat optimization Anthony Labarre
fonte
O que você quer dizer exatamente com "variantes do SAT"?
Giorgio Camerani
k
4
Não se preocupe, é a palavra certa, eu deveria ter entendido isso. De um ponto de vista puramente prático, no entanto, não acho que isso importe (o que mais importa é quão parcimoniosa é a sua codificação). Você poderia fornecer mais detalhes sobre o problema de otimização que você está tentando resolver? Estou muito interessado em aplicações práticas do SAT e nos aspectos de engenharia da solução do SAT.
Giorgio Camerani
Parece um pouco confuso que você esteja falando sobre um problema de otimização, mas ao mesmo tempo sobre o SAT. Normalmente, para otimizar, você precisa de algo mais forte, por exemplo, MAX-SAT. Talvez você possa esclarecer isso.
Mikolas
esta questão pode ser algo relacionado: cstheory.stackexchange.com/q/4314/4506
Mikolas

Respostas:

9

Não tenho certeza se é isso que você está procurando, mas aqui está um: JM Silva, aplicações práticas de satisfação booleana .

Mikolas
fonte
2
Não consegui acessá-lo através do seu link, aqui está outro . À primeira vista, o artigo parece bastante interessante, mas mais focado em aplicativos do que o que estou procurando.
Anthony Labarre
@ Anthony bem, você disse que está interessado no aspecto prático :-) De qualquer forma, os solucionadores convencionais existentes não diferenciam realmente os diferentes tipos de SAT. No passado, houve algum trabalho na exploração de cláusulas binárias, por exemplo. Mas os solucionadores existentes apenas usam o aprendizado de cláusulas DPLL + unit prop + +. No entanto, alguns dos pré-processadores exploram a estrutura. Mas, novamente, não realmente do ponto de vista da complexidade. classificação.
Mikolas
8

O capítulo 2 do Manual de satisfação examina os aspectos a serem considerados ao projetar essas transformações, bem como uma lista de referências que respondem à minha pergunta. Isso me ajudou a encontrar alguns exemplos que podemos observar para se familiarizar com essas transformações:

Anthony Labarre
fonte