Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. (English) Zbl 1077.68002

Lecture Notes in Computer Science 3569. Berlin: Springer (ISBN 3-540-26276-8/pbk). xii, 492 p. (2005).

Show indexed articles as search result.

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


68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
00B25 Proceedings of conferences of miscellaneous specific interest


Zbl 1075.68002
Full Text: DOI