Kleine Büning, Hans; Zhao, Xishun Extension and equivalence problems for clause minimal formulae. (English) Zbl 1099.68041 Ann. Math. Artif. Intell. 43, No. 1-4, 295-306 (2005). MSC: 68Q25 68T20 PDFBibTeX XMLCite \textit{H. Kleine Büning} and \textit{X. Zhao}, Ann. Math. Artif. Intell. 43, No. 1--4, 295--306 (2005; Zbl 1099.68041) Full Text: DOI
Egly, Uwe; Pichler, Reinhard; Woltran, Stefan On deciding subsumption problems. (English) Zbl 1099.68095 Ann. Math. Artif. Intell. 43, No. 1-4, 255-294 (2005). MSC: 68T15 68T20 PDFBibTeX XMLCite \textit{U. Egly} et al., Ann. Math. Artif. Intell. 43, No. 1--4, 255--294 (2005; Zbl 1099.68095) Full Text: DOI
Van Gelder, Allen Toward leaner binary-clause reasoning in a satisfiability solver. (English) Zbl 1099.68097 Ann. Math. Artif. Intell. 43, No. 1-4, 239-253 (2005). MSC: 68T15 68T20 PDFBibTeX XMLCite \textit{A. Van Gelder}, Ann. Math. Artif. Intell. 43, No. 1--4, 239--253 (2005; Zbl 1099.68097) Full Text: DOI
Szeider, Stefan Generalizations of matched CNF formulas. (English) Zbl 1099.68044 Ann. Math. Artif. Intell. 43, No. 1-4, 223-238 (2005). MSC: 68Q25 68R10 68T20 PDFBibTeX XMLCite \textit{S. Szeider}, Ann. Math. Artif. Intell. 43, No. 1--4, 223--238 (2005; Zbl 1099.68044) Full Text: DOI
Pretolani, Daniele Probability logic and optimization SAT: The PSAT and CPA models. (English) Zbl 1075.68086 Ann. Math. Artif. Intell. 43, No. 1-4, 211-221 (2005). MSC: 68T20 03B48 68Q25 PDFBibTeX XMLCite \textit{D. Pretolani}, Ann. Math. Artif. Intell. 43, No. 1--4, 211--221 (2005; Zbl 1075.68086) Full Text: DOI
Prestwich, Steven; Bressan, Stéphane A SAT approach to query optimization in mediator systems. (English) Zbl 1099.68103 Ann. Math. Artif. Intell. 43, No. 1-4, 195-210 (2005). MSC: 68T20 68P15 PDFBibTeX XMLCite \textit{S. Prestwich} and \textit{S. Bressan}, Ann. Math. Artif. Intell. 43, No. 1--4, 195--210 (2005; Zbl 1099.68103) Full Text: DOI
Porschen, Stefan; Randerath, Bert; Speckenmeyer, Ewald Exact 3-satisfiability is decidable in time \(O(2^{0.16254 n})\). (English) Zbl 1099.68042 Ann. Math. Artif. Intell. 43, No. 1-4, 173-193 (2005). MSC: 68Q25 03B05 68T20 PDFBibTeX XMLCite \textit{S. Porschen} et al., Ann. Math. Artif. Intell. 43, No. 1--4, 173--193 (2005; Zbl 1099.68042) Full Text: DOI
Cocco, Simona; Monasson, Rémi Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT. (English) Zbl 1100.68576 Ann. Math. Artif. Intell. 43, No. 1-4, 153-172 (2005). MSC: 68Q25 68T20 PDFBibTeX XMLCite \textit{S. Cocco} and \textit{R. Monasson}, Ann. Math. Artif. Intell. 43, No. 1--4, 153--172 (2005; Zbl 1100.68576) Full Text: DOI arXiv
Lynce, Inês; Marques-Silva, João Efficient data structures for backtrack search SAT solvers. (English) Zbl 1099.68025 Ann. Math. Artif. Intell. 43, No. 1-4, 137-152 (2005). MSC: 68P05 68T20 PDFBibTeX XMLCite \textit{I. Lynce} and \textit{J. Marques-Silva}, Ann. Math. Artif. Intell. 43, No. 1--4, 137--152 (2005; Zbl 1099.68025) Full Text: DOI Link
Kusper, Gábor Solving the resolution-free SAT problem by submodel propagation in linear time. (English) Zbl 1099.68101 Ann. Math. Artif. Intell. 43, No. 1-4, 129-136 (2005). MSC: 68T20 68T27 PDFBibTeX XMLCite \textit{G. Kusper}, Ann. Math. Artif. Intell. 43, No. 1--4, 129--136 (2005; Zbl 1099.68101) Full Text: DOI
Kleine Büning, Hans; Xu, Daoyun The complexity of homomorphisms and renamings for minimal unsatisfiable formulas. (English) Zbl 1099.68040 Ann. Math. Artif. Intell. 43, No. 1-4, 113-127 (2005). MSC: 68Q25 68T20 PDFBibTeX XMLCite \textit{H. Kleine Büning} and \textit{D. Xu}, Ann. Math. Artif. Intell. 43, No. 1--4, 113--127 (2005; Zbl 1099.68040) Full Text: DOI
Hirsch, Edward A.; Kojevnikov, Arist UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. (English) Zbl 1100.68621 Ann. Math. Artif. Intell. 43, No. 1-4, 91-111 (2005). MSC: 68T20 03B05 68W20 PDFBibTeX XMLCite \textit{E. A. Hirsch} and \textit{A. Kojevnikov}, Ann. Math. Artif. Intell. 43, No. 1--4, 91--111 (2005; Zbl 1100.68621) Full Text: DOI
Goldberg, Eugene Testing satisfiability of CNF formulas by computing a stable set of points. (English) Zbl 1099.68099 Ann. Math. Artif. Intell. 43, No. 1-4, 65-89 (2005). MSC: 68T20 68T27 PDFBibTeX XMLCite \textit{E. Goldberg}, Ann. Math. Artif. Intell. 43, No. 1--4, 65--89 (2005; Zbl 1099.68099) Full Text: DOI
Chapdelaine, Philippe; Creignou, Nadia The complexity of Boolean constraint satisfaction local search problems. (English) Zbl 1099.68033 Ann. Math. Artif. Intell. 43, No. 1-4, 51-63 (2005). MSC: 68Q15 68Q17 68T20 PDFBibTeX XMLCite \textit{P. Chapdelaine} and \textit{N. Creignou}, Ann. Math. Artif. Intell. 43, No. 1--4, 51--63 (2005; Zbl 1099.68033) Full Text: DOI
Bruni, Renato On exact selection of minimally unsatisfiable subformulae. (English) Zbl 1099.68105 Ann. Math. Artif. Intell. 43, No. 1-4, 35-50 (2005). MSC: 68T27 68Q25 68T15 68T20 PDFBibTeX XMLCite \textit{R. Bruni}, Ann. Math. Artif. Intell. 43, No. 1--4, 35--50 (2005; Zbl 1099.68105) Full Text: DOI
Brglez, Franc; Li, Xiao Yu; Stallmann, Matthias F. On SAT instance classes and a method for reliable performance experiments with SAT solvers. (English) Zbl 1100.68575 Ann. Math. Artif. Intell. 43, No. 1-4, 1-34 (2005). MSC: 68Q25 68T20 62N05 PDFBibTeX XMLCite \textit{F. Brglez} et al., Ann. Math. Artif. Intell. 43, No. 1--4, 1--34 (2005; Zbl 1100.68575) Full Text: DOI