Witness of unsatisfiability for a random 3-satisfiability formula.
Phys Rev E Stat Nonlin Soft Matter Phys
; 87(5): 052807, 2013 May.
Article
em En
| MEDLINE
| ID: mdl-23767584
ABSTRACT
The random 3-satisfiability (3-SAT) problem is in the unsatisfiable (UNSAT) phase when the clause density α exceeds a critical value α(s)≈4.267. Rigorously proving the unsatisfiability of a given large 3-SAT instance is, however, extremely difficult. In this paper we apply the mean-field theory of statistical physics to the unsatisfiability problem, and show that a reduction to 3-XORSAT, which permits the construction of a specific type of UNSAT witnesses (Feige-Kim-Ofek witnesses), is possible when the clause density α>19. We then construct Feige-Kim-Ofek witnesses for single 3-SAT instances through a simple random sampling algorithm and a focused local search algorithm. The random sampling algorithm works only when α scales at least linearly with the variable number N, but the focused local search algorithm works for clause density α>cN(b) with b≈0.59 and prefactor c≈8. The exponent b can be further decreased by enlarging the single parameter S of the focused local search algorithm.
Buscar no Google
Base de dados:
MEDLINE
Assunto principal:
Interpretação Estatística de Dados
/
Modelos Estatísticos
/
Tamanho da Amostra
Tipo de estudo:
Clinical_trials
/
Prognostic_studies
/
Risk_factors_studies
Idioma:
En
Revista:
Phys Rev E Stat Nonlin Soft Matter Phys
Assunto da revista:
BIOFISICA
/
FISIOLOGIA
Ano de publicação:
2013
Tipo de documento:
Article
País de afiliação:
China