Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19--23, 2005. Proceedings. (Q2574654)

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1075.68002). Indexed articles: \textit{Argelich, Josep; Manyà, Felip}, Solving over-constrained problems with SAT technology, 1-15 [Zbl 1124.68430] \textit{Audemard, Gilles; Saïs, Lakhdar}, A symbolic search based approach for quantified Boolean formulas, 16-30 [Zbl 1128.68451] \textit{Belov, Anton; Stachniak, Zbigniew}, Substitutional definition of satisfiability in classical propositional logic, 31-45 [Zbl 1128.03303] \textit{Dershowitz, Nachum; Hanna, Ziyad; Nadel, Alexander}, A clause-based heuristic for SAT solvers, 46-60 [Zbl 1128.68461] \textit{Eén, Niklas; Biere, Armin}, Effective preprocessing in SAT through variable and clause elimination, 61-75 [Zbl 1128.68463] \textit{Galesi, Nicola; Thapen, Neil}, Resolution and pebbling games, 76-90 [Zbl 1128.03304] \textit{Gent, Ian P.; Rowley, Andrew G. D.}, Local and global complete solution learning methods for QBF, 91-106 [Zbl 1128.68464] \textit{Goldberg, Eugene}, Equivalence checking of circuits with parameterized specifications, 107-121 [Zbl 1128.68367] \textit{Heule, Marijn; van Maaren, Hans}, Observed lower bounds for random 3-SAT phase transition density using linear programming, 122-134 [Zbl 1128.68466] \textit{Hirsch, Edward A.; Nikolenko, Sergey I.}, Simulating cutting plane proofs with restricted degree of falsity by resolution, 135-142 [Zbl 1128.03314] \textit{Kouril, Michal; Franco, John}, Resolution tunnels for improved SAT solver performance, 143-157 [Zbl 1128.68468] \textit{Li, Chu Min; Huang, Wen Qi}, Diversification and determinism in local search for satisfiability, 158-172 [Zbl 1128.68472] \textit{Liffiton, Mark H.; Sakallah, Karem A.}, On finding all minimally unsatisfiable subformulas, 173-186 [Zbl 1128.68473] \textit{Marinov, Darko; Khurshid, Sarfraz; Bugrara, Suhabe; Zhang, Lintao; Rinard, Martin}, Optimizations for compiling declarative models into Boolean formulas, 187-202 [Zbl 1128.68475] \textit{Prestwich, Steven}, Random walk with continuously smoothed variable weights, 203-215 [Zbl 1128.68478] \textit{Rolf, Daniel}, Derandomization of PPSZ for unique-\(k\)-SAT, 216-225 [Zbl 1128.68479] \textit{Sang, Tian; Beame, Paul; Kautz, Henry}, Heuristics for fast exact model counting, 226-240 [Zbl 1128.68481] \textit{Sheini, Hossein M.; Sakallah, Karem A.}, A scalable method for solving satisfiability of integer linear arithmetic logic, 241-256 [Zbl 1128.68483] \textit{Sinz, Carsten; Dieringer, Edda-Maria}, DPvis -- a tool to visualize the structure of SAT instances, 257-268 [Zbl 1128.68484] \textit{Southey, Finnegan}, Constraint metrics for local search, 269-281 [Zbl 1128.68485] \textit{Van Gelder, Allen}, Input distance and lower bounds for propositional resolution proof length, 282-293 [Zbl 1128.03315] \textit{van Maaren, Hans; van Norden, Linda}, Sums of squares, satisfiability and maximum satisfiability, 294-308 [Zbl 1128.68489] \textit{Wahlström, Magnus}, Faster exact solving of SAT formulae with a low number of occurrences per variable, 309-323 [Zbl 1128.68486] \textit{Wei, Wei; Selman, Bart}, A new approach to model counting, 324-339 [Zbl 1128.68487] \textit{Zarpas, Emmanuel}, Benchmarking SAT solvers for bounded model checking, 340-354 [Zbl 1128.68368] \textit{Zhao, Xishun; Kleine Büning, Hans}, Model-equivalent reductions, 355-370 [Zbl 1128.68360] \textit{Alsinet, Teresa; Manyà, Felip; Planes, Jordi}, Improved exact solvers for weighted Max-SAT, 371-377 [Zbl 1124.68429] \textit{Benedetti, Marco}, Quantifier trees for QBFs, 378-385 [Zbl 1128.68452] \textit{Bubeck, Uwe; Kleine Büning, Hans; Zhao, Xishun}, Quantifier rewriting and equivalence models for quantified Horn formulas, 386-392 [Zbl 1128.68455] \textit{Coste-Marquis, Sylvie; Le Berre, Daniel; Letombe, Florian}, A branching heuristics for quantified renamable Horn formulas, 393-399 [Zbl 1128.68459] \textit{Dantsin, Evgeny; Wolpert, Alexander}, An improved upper bound for SAT, 400-407 [Zbl 1128.68460] \textit{Dershowitz, Nachum; Hanna, Ziyad; Katz, Jacob}, Bounded model checking with QBF, 408-414 [Zbl 1128.68366] \textit{Durairaj, Vijay; Kalla, Priyank}, Variable ordering for efficient SAT search by analyzing constraint-variable dependencies, 415-422 [Zbl 1128.68462] \textit{Gershman, Roman; Strichman, Ofer}, Cost-effective hyper-resolution for preprocessing CNF formulas, 423-429 [Zbl 1128.68465] \textit{Kulikov, Alexander S.}, Automated generation of simplification rules for SAT and MAXSAT, 430-436 [Zbl 1128.68469] \textit{Lewis, Matthew D. T.; Schubert, Tobias; Becker, Bernd W.}, Speedup techniques utilized in modern SAT solvers -- an analysis in the MIRA environment., 437-443 [Zbl 1128.68471] \textit{Ling, Andrew; Singh, Deshanand P.; Brown, Stephen D.}, FPGA logic synthesis using quantified Boolean satisfiability, 444-450 [Zbl 1128.94308] \textit{Manquinho, Vasco; Marques-Silva, João}, On applying cutting planes in DLL-based algorithms for pseudo-Boolean optimization, 451-458 [Zbl 1128.68474] \textit{Meier, Andreas; Sorge, Volker}, A new set of algebraic benchmark problems for SAT solvers, 459-466 [Zbl 1128.68476] \textit{Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem}, A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas, 467-474 [Zbl 1128.68477] \textit{Seitz, Sakari; Alava, Mikko; Orponen, Pekka}, Threshold behaviour of WalkSAT and focused Metropolis search on random 3-satisfiability, 475-481 [Zbl 1128.68482] \textit{Zhang, Lintao}, On subsumption removal and on-the-fly CNF simplification, 482-489 [Zbl 1128.68488]