Perguntas com a marcação «sat»

24
Iniciando os papéis do SAT Solver

Eu quero fazer um primeiro solucionador de SAT. Conheço a competição do SAT e a conferência do SAT, e há tantos artigos sobre esse assunto. Eu sou um iniciante, um iniciante oprimido. Por onde devo começar? Eventualmente, eu quero empurrar o estado da arte. Quero alguns conselhos de especialistas...

22
Por que o CNF é usado para SAT e não DNF?

Não entendo muito bem por que quase todos os solucionadores de SAT usam CNF em vez de DNF. Parece-me que resolver o SAT é mais fácil usando DNF. Afinal, você só precisa verificar o conjunto de implicantes e verificar se um deles não contém uma variável e sua negação. Para a CNF, não existe um...

21
Download do #SAT Solver

Alguém poderia apontar para um ou mais sites onde é possível fazer o download de uma implementação de trabalho de um solucionador #SAT? Estou interessado em retornar a contagem exata da solução, não em uma

19
Fórmulas mínimas insatisfatórias de 3-CNF

Atualmente, estou interessado em obter (ou construir) e estudar fórmulas de 3-CNF insatisfatórias e de tamanho mínimo. Ou seja, eles devem consistir no menor número possível de cláusulas (m = 8) e no menor número possível de variáveis ​​distintas (n = 4 ou mais), de modo que a remoção de pelo menos...

18
Redução direta de SAT para 3-SAT

Aqui, o objetivo é reduzir um problema arbitrário de SAT para 3-SAT em tempo polinomial usando o menor número de cláusulas e variáveis. Minha pergunta é motivada pela curiosidade. Menos formalmente, eu gostaria de saber: "Qual é a redução 'mais natural' de SAT para 3-SAT?" Agora, a redução que eu...

18
Fórmula CNF equivalente mais curta

Seja uma fórmula CNF satisfatória com variáveis ​​e cláusulas . Seja o espaço de solução de .F1F1F_1m S F 1 F 1nnnmmmSF1SF1S_{F_1}F1F1F_1 Considere o problema de determinar, dada a , outra Fórmula CNF com o mesmo conjunto de variáveis ​​que , com (o mesmo espaço de solução que ), mas com o mínimo...

17
Satisfação de restrição aberta ou interativa

No passado, implementei modelos de coordenação usando SAT e satisfação regular de restrições como o cavalo de batalha principal em seus motores. Continuando nesta linha de trabalho, gostaria de tornar os modelos mais interativos, e a melhor maneira de fazer isso é abrir o solucionador de restrições...

16
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 kkk -SAT, cuja entrada é uma fórmula kkk -CNF com no máximo 111 atribuição satisfatória. Para testar...