Geodesic
On the complexity of unique Circuit SAT
Zapiski Nauchnykh Seminarov POMI, Combinatorics and graph theory. Part X, Tome 475 (2018), pp. 122-136 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

We consider the Circuit SAT problem for a circuit with at most one satisfying assignment. We present an algorithm running in time $O(2^{.374589m})$, where $m$ is the number of internal gates of the circuit. In order to make the exposition self-contained, we also describe the algorithm for the general case of Circuit SAT with running time $O(2^{.389667m})$ obtained by Savinov in [10]. 
@article{ZNSL_2018_475_a5,
     author = {A. A. Lialina},
     title = {On the complexity of unique {Circuit} {SAT}},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {122--136},
     year = {2018},
     volume = {475},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2018_475_a5/}
}
TY  - JOUR
AU  - A. A. Lialina
TI  - On the complexity of unique Circuit SAT
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2018
SP  - 122
EP  - 136
VL  - 475
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2018_475_a5/
LA  - en
ID  - ZNSL_2018_475_a5
ER  - 
%0 Journal Article
%A A. A. Lialina
%T On the complexity of unique Circuit SAT
%J Zapiski Nauchnykh Seminarov POMI
%D 2018
%P 122-136
%V 475
%U http://geodesic.mathdoc.fr/item/ZNSL_2018_475_a5/
%G en
%F ZNSL_2018_475_a5
A. A. Lialina. On the complexity of unique Circuit SAT. Zapiski Nauchnykh Seminarov POMI, Combinatorics and graph theory. Part X, Tome 475 (2018), pp. 122-136. http://geodesic.mathdoc.fr/item/ZNSL_2018_475_a5/

[1] E. Ya. Dantsin, “Two tautologihood proof systems based on the split method”, Zap. Nauchn. Sem. LOMI, 105, 1981, 24–44 | MR | Zbl

[2] A. Golovnev, A. S. Kulikov, A. V. Smal, S. Tamaki, “Circuit Size Lower Bounds and #SAT Upper Bounds Through a General Framework”, Proceedings of 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016), LIPIcs, 58, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016, 45:1–45:16 | MR

[3] E. A. Hirsch, “New worst-case upper bounds for SAT”, J. Automated Reasoning, 24:4 (2000), 397–420 | DOI | MR | Zbl

[4] O. Kullmann, “New methods for 3-SAT decision and worst-case analysis”, Theor. Computer Sci., 223:1–2 (1999), 1–72 | DOI | MR | Zbl

[5] O. Kullmann, H. Luckhardt, Deciding propositional tautologies: Algorithms and their complexity, Technical report, Fachbereich Mathematik, Johann Wolfgang Goethe Universität, 1997

[6] B. Monien, E. Speckenmeyer, $3$-satisfability is testable in $O(1.62^r)$ steps, Bericht Nr. 3/1979, Reihe Theoretische Informatik, Universität-Gesamthochschule-Paderborn, 1979

[7] S. Nurk, An ${O}(2^{.4058m})$ upper bound for Circuit SAT, PDMI Preprint, 2009

[8] R. Paturi, P. Pudlák, M. E. Saks, F. Zane, “An improved exponential-time algorithm for k-SAT”, J. ACM, 52:3 (2005), 337–364 | DOI | MR | Zbl

[9] R. Santhanam, “Fighting perebor: New and improved algorithms for formula and QBF satisfiability”, Proceedings of the 51th Annual IEEE Symposium on Foundations of Computer Science (FOCS), 2010, 183–192 | MR

[10] S. V. Savinov, Upper bound for Circuit SAT, MSc Thesis, St. Petersburg Academic University RAS, 2014

[11] K. Seto, S. Tamaki, “A satisfiability algorithm and average-case hardness for formulas over the full binary basis”, Comput. Complexity, 22:2 (2013), 245–274 | DOI | MR | Zbl

[12] L. G. Valiant, V. V. Vazirani, “NP is as easy as detecting unique solutions”, Theor. Computer Sci., 47 (1986), 85–93 | DOI | MR

[13] M. Wahlström, “An algorithm for the SAT problem for formulae of linear length”, Proceedings of the 13th Annual European Symposium on Algorithms, ESA 2005, Lecture Notes in Computer Science, 3669, 2005, 107–118 | DOI | MR | Zbl