Benchmarks exclusivos do

Essa pergunta provavelmente está na linha de fronteira entre o tópico e o tópico, mas eu já vi perguntas semelhantes aqui, portanto, eu vou perguntar.

Estou implementando um solucionador Unique $k$ -SAT, cuja entrada é uma fórmula $k$ -CNF com no máximo $1$ atribuição satisfatória. Para testar seu comportamento prático, preciso de um conjunto dessas fórmulas. Eu procurei por eles na web e não encontrei nada (por outro lado, é muito fácil encontrar conjuntos de fórmulas $k$ CNF comuns ).

Onde posso encontrar instâncias exclusivas do $k$ -SAT?

Como alternativa, eu também ficaria satisfeito em conhecer qualquer procedimento para gerar instâncias exclusivamente satisfatórias. A única abordagem da qual estou ciente está sob o nome de geração de instância SAT plantada : você gera aleatoriamente uma atribuição de $n$ variáveis, depois gera apenas as cláusulas que concordam com essa atribuição. Essa abordagem é insatisfatória para meus propósitos, pelos seguintes motivos:

• A fórmula obtida pode ter outras atribuições satisfatórias indesejadas.
• Para ter certeza de que a fórmula é satisfeita exclusivamente pela atribuição desejada, você deve apresentar todas as possíveis cláusulas que concordam com ela. Isso produziria fórmulas com muitas cláusulas, que provavelmente serão fáceis de resolver e, portanto, não representativas do pior comportamento do solucionador. Não é óbvio para mim como podemos forçar eficientemente a exclusividade, mantendo o número de cláusulas razoável.

Como podemos gerar fórmulas exclusivamente satisfatórias com um número razoável de cláusulas? Por razoável, quero dizer longe do máximo .$2^k \cdot {n \choose k}$

Aqui está uma maneira de gerar um único exemplo -SAT, dado um exemplo SAT φ que você sabe é satisfeita. Considere a fórmula ψ ( x ) dada por$k$$\varphi$$\psi(x)$

onde é uma função de hash que mapeia uma atribuição x para um valor de k bits (para algum valor pequeno de k ) e y é um valor aleatório de k bits. Se φ tiver cerca de 2 k tarefas satisfatórias, (heuristicamente) assumimos que ψ terá exatamente uma tarefa satisfatória (com probabilidade constante). Podemos testar se esse é o caso usando um solucionador SAT (ou seja, testar se ψ é satisfatório; se for, e x 0 é uma tarefa satisfatória, testar se ψ ( x ) ∧ $h$$x$$k$$k$$y$$k$$\varphi$$2^k$$\psi$$\psi$$x_0$ é satisfatório). Se k não for conhecido, você poderá encontrar k usando pesquisa binária ou apenas iterando sobre cada valor candidato k = 1 , 2 , … , n (onde n é o número de variáveis ​​booleanas em x ).$\psi(x) \land x \ne x_0$$k$$k$$k=1,2,\dots,n$$n$$x$

Você pode escolher a função hash livremente. Você provavelmente desejará torná-lo o mais simples possível. Uma construção extremamente simples é ter escolher um subconjunto aleatório de k bits de x . Uma construção um pouco mais sofisticada é fazer com que o i- bit de h ( x ) seja o x ou os dois bits escolhidos aleatoriamente a partir de x (escolhendo um par separado de posições de bits para cada i , independentemente). Manter h simples manterá ψ relativamente simples.$h$$k$$x$$i$$h(x)$$x$$i$$h$$\psi$

Às vezes, esse tipo de transformação é usado / sugerido como parte de um esquema para estimar o número de atribuições satisfatórias para uma fórmula ; Eu o adaptei para sua necessidade específica.$\varphi$

Você pode encontrar muitos bancos de testes de instâncias SAT na Internet e aplicar essa transformação a todas elas, para obter uma coleção de instâncias Unique -SAT.$k$

Outra possibilidade seria gerar instâncias Unique -SAT a partir de criptografia. Por exemplo, suponha que f : { 0 , 1 } n → { 0 , 1 } n seja uma permutação criptográfica unidirecional. Seja x um elemento escolhido aleatoriamente de { 0 , 1 } n , e seja y = f ( x ) . Então a fórmula φ ( x ) dada por f ( x ) $k$$f:\{0,1\}^n \to \{0,1\}^n$$x$$\{0,1\}^n$$y=f(x)$$\varphi(x)$ é umainstânciaexclusiva k -SAT. Como outro exemplo, escolha dois números primos grandes p , q aleatoriamente e deixe n = p q . Então, a fórmula φ ( x , y ) dada por x ⋅ y = n ∧ x > 1 ∧ y > 1 ∧ x ≤ y (com a correspondência óbvia entre cadeias de bits e números inteiros) é um k exclusivo$f(x)=y$$k$$p,q$$n=pq$$\varphi(x,y)$$x \cdot y = n \land x>1 \land y>1 \land x \le y$$k$Instância -SAT. No entanto, essas construções não parecem uma maneira útil de avaliar ou otimizar seu solucionador. Todos eles têm uma estrutura especial e não há razão para acreditar que essa estrutura seja representativa dos problemas do mundo real. Em particular, sabe-se que as instâncias SAT extraídas de problemas criptográficos são extremamente difíceis, muito mais difíceis do que as instâncias SAT extraídas de muitas outras aplicações do mundo real de solucionadores SAT, portanto, elas não são uma base muito boa para comparar seu solucionador.

Em geral, todas as técnicas mencionadas nesta resposta têm a desvantagem de gerar instâncias -SAT únicas com uma estrutura específica, portanto, elas podem não ser o que você está procurando - ou, pelo menos, talvez não queira confiar somente nas fórmulas geradas dessa maneira. Uma abordagem melhor seria identificar os aplicativos do Unique k -SAT (quem você acha que vai usar o seu solucionador e com qual finalidade?) E, em seguida, tentar obter alguns exemplos realistas desses domínios de aplicativo.$k$$k$

Para um tópico relacionado, consulte também Gerando problemas interessantes de otimização combinatória

Você pode considerar os algoritmos usados ​​para gerar quebra-cabeças do Sudoku - presumivelmente generalizados para - já que (geralmente) os quebra-cabeças do Sudoku devem ter uma solução única. Por outro lado, também é garantido que os quebra-cabeças de Sudoku tenham pelo menos uma solução ... Mas encontrar essa solução ainda pode ser uma boa referência para o seu solucionador.$n \times n$

Você pode usar um gerador Sudoku junto com uma redução ao SAT ou pode pensar em como aplicar as técnicas usadas na geração Sudoku para gerar mais diretamente instâncias SAT exclusivas. Para o primeiro, obviamente suas instâncias SAT terão alguma estrutura, mas não está claro para mim se é mais ou menos estrutura do que, por exemplo, plantar uma solução ou usar a técnica de isolamento de testemunha. Provavelmente depende das suas necessidades e do seu solucionador.

A única referência que eu conheço aqui é: Sudoku Puzzles Generating: from Easy to Evil .

Acho que um bom caso de teste seria gerar instâncias 3XOR aleatórias e exclusivamente satisfatórias (instâncias plantadas) com restrições e depois convertê-las em instâncias 3SAT.$\Theta(n)$

Uma das melhores maneiras de criar instâncias SAT "presumivelmente difíceis" ao controlar o número de soluções é de instâncias / circuitos de fatoração inteiros codificados em binário. o código não é muito complexo, usa principalmente circuitos de adição EE e não leva a instâncias "grandes" de SAT. o número de soluções é igual ao número de fatores (incluindo "permutações" dos fatores). portanto, números primos geram exatamente duas soluções, . uma única solução pode ser garantida com uma restrição adicional de "comparação" que restringe os fatores a um $(1,p),(p,1)$$a<b$$a \neq 1$ .$b \neq p$

também com essa abordagem, é relativamente fácil encontrar números com praticamente todos os fatores / soluções desejados. quanto mais suave o número, mais fatores.

vários pesquisadores, ao longo dos anos, criaram esse código SAT de fatoração (por exemplo, para a competição / arquivo DIMACS que armazenou algumas instâncias de fatoração no passado), mas infelizmente não parece haver uma versão disponível ao público. veja também o primeiro link abaixo para uma referência onde o código foi escrito / implementado aparentemente para um curso de pós-graduação.

• Reduzindo o problema da fatoração inteira para um problema NP-Complete
• Gerando circuito 3SAT para exemplo de fatoração de número inteiro

Outra abordagem empírica / iterativo que pode ser útil para algumas, para criar casos mais "não estruturados": criar ocorrências aleatórias SAT perto do ponto de transição (a região onde a equação tem uma probabilidade de 50% entre "solúvel e insolúvel"), e então resolva a equação. se for insolúvel, jogue fora e reinicie. se for solucionável, adicione cláusulas que restrinjam a solução "não" à solução encontrada, obtendo e n + 1 e resolvendo novamente. repita se necessário. quando a equação e n + 1 não é mais solucionável, o e n deve ter uma solução única / única.$e_n$$e_{n+1}$$e_{n+1}$$e_n$

Você pode facilmente gerar diretamente fórmulas SAT exclusivas com tamanho razoável $(|F|<n+2^k)$

Seja o modelo único - digamos que m contenha apenas "0" s (renomeie as variáveis ​​posteriormente, se necessário). Seja F uma fórmula k- SAT satisfeita apenas por m - o tamanho máximo de F é o número total de cláusulas satisfeitas por m ie ( 2 k - 1 ) ($m$$m$
$F$$k$$m$$F$$m$ .$(2^k-1) \binom{n}{k}$

Pegue a cláusulas que eliminam todos os modelos atribuir exatamente um "1" entrex1,x2...xk:(¬x1,x2...xk)(x1,¬x2...xk)...(x1,x2...¬xk$\binom{k}{1}$$x_1,x_2 \ldots x_k$
$(\lnot x_1, x_2 \ldots x_k)(x_1, \lnot x_2 \ldots x_k)\ldots (x_1,x_2 \ldots \lnot x_k)$

Pegue a cláusulas que eliminam todos os modelos de atribuição de exatamente dois "1" entrex1,x2...xk:(¬x1,¬x2,x3...xk)(¬x1,x2,¬x3...xk)…(x1,x2…¬xk-1$\binom{k}{2}$$x_1,x_2 \ldots x_k$
$(\lnot x_1, \lnot x_2, x_3 \ldots x_k)(\lnot x_1,x_2, \lnot x_3 \ldots x_k)\ldots (x_1,x_2 \ldots \lnot x_{k-1} \lnot x_k)$

$\binom{k}{k}$$x_1,x_2 \ldots x_k$

$x_1,x_2 \ldots x_k$$m$$n-k$$x_i (k<i\leq n)$$0$$k-1$$x_1,x_2 \ldots x_k$
$(\lnot x_{k+1}, x_1 \ldots, x_{k-1}) \ldots (\lnot x_n, x_1 \ldots x_{k-1})$.

Then $|F|=\sum_{i=1}^k \binom{k}{i} +n-k = 2^k-1+n-k$

Para obter mais cláusulas, adicione qualquer cláusula que contenha pelo menos uma variável negada. Para obter uma fórmula insatisfatória, basta adicionar uma cláusula com$k$ variáveis ​​não-negativas.