Theory and applications of satisfiability testing – SAT 2017. 20th international conference, Melbourne, VIC, Australia, August 28 – September 1, 2017. Proceedings. (English) Zbl 1368.68008

Lecture Notes in Computer Science 10491. Cham: Springer (ISBN 978-3-319-66262-6/pbk; 978-3-319-66263-3/ebook). xiii, 476 p. (2017).

Show indexed articles as search result.

The articles of mathematical interest will be reviewed individually. For the preceding conference see [Zbl 1337.68009].
Indexed articles:
Achlioptas, Dimitris; Theodoropoulos, Panos, Probabilistic model counting with short XORs, 3-19 [Zbl 1496.68253]
Ganian, Robert; Ramanujan, M. S.; Szeider, Stefan, Backdoor treewidth for SAT, 20-37 [Zbl 1496.68256]
Ganian, Robert; Szeider, Stefan, New width parameters for model counting, 38-52 [Zbl 1496.68257]
Itsykson, Dmitry; Knop, Alexander, Hard satisfiable formulas for splittings by linear combinations, 53-61 [Zbl 06807218]
Baud-Berthier, Guillaume; Giráldez-Cru, Jesús; Simon, Laurent, On the community structure of bounded model checking SAT problems, 65-82 [Zbl 1496.68361]
Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice, Symmetric explanation learning: effective dynamic symmetry handling for SAT, 83-100 [Zbl 1496.68366]
Junttila, Tommi; Karppa, Matti; Kaski, Petteri; Kohonen, Jukka, An adaptive prefix-assignment technique for symmetry reduction, 101-118 [Zbl 1496.68301]
Liang, Jia Hui; Hari Govind, V. K.; Poupart, Pascal; Czarnecki, Krzysztof; Ganesh, Vijay, An empirical study of branching heuristics through the lens of global learning rate, 119-135 [Zbl 1496.68304]
Nabeshima, Hidetomo; Inoue, Katsumi, Coverage-based clause reduction heuristics for CDCL solvers, 136-144 [Zbl 1496.68305]
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao, On tackling the limits of resolution in SAT solving, 164-183 [Zbl 1496.68368]
Previti, Alessandro; Mencía, Carlos; Järvisalo, Matti; Marques-Silva, Joao, Improving MCS enumeration via caching, 184-194 [Zbl 1496.68258]
Terra-Neves, Miguel; Lynce, Inês; Manquinho, Vasco, Introducing Pareto minimal correction subsets, 195-211 [Zbl 1496.68307]
Blinkhorn, Joshua; Beyersdorff, Olaf, Shortening QBF proofs with dependency schemes, 263-280 [Zbl 1496.68364]
Kiesl, Benjamin; Heule, Marijn J. H.; Seidl, Martina, A little blocked literal goes a long way, 281-297 [Zbl 1496.68370]
Peitl, Tomáš; Slivovsky, Friedrich; Szeider, Stefan, Dependency learning for QBF, 298-313 [Zbl 1478.68330]
Rabe, Markus N., A resolution-style proof system for DQBF, 314-325 [Zbl 1496.03050]
Wimmer, Ralf; Karrenbauer, Andreas; Becker, Ruben; Scholl, Christoph; Becker, Bernd, From DQBF to QBF by dependency elimination, 326-343 [Zbl 1496.68372]
Hyvärinen, Antti E. J.; Asadi, Sepideh; Even-Mendoza, Karine; Fedyukovich, Grigory; Chockler, Hana; Sharygina, Natasha, Theory refinement for program verification, 347-363 [Zbl 1496.68191]
Jonáš, Martin; Strejček, Jan, On simplification of formulas with unconstrained variables and quantifiers, 364-379 [Zbl 1496.68369]
Kafle, Bishoksan; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J., A Benders decomposition approach to deciding modular linear integer arithmetic, 380-397 [Zbl 1496.68193]
Fichte, Johannes K.; Lodha, Neha; Szeider, Stefan, SAT-based local improvement for finding tree decompositions of small width, 401-411 [Zbl 1496.68154]
Kučera, Petr; Savický, Petr; Vorel, Vojtěch, A lower bound on CNF encodings of the at-most-one constraint, 412-428 [Zbl 1417.68198]
Lodha, Neha; Ordyniak, Sebastian; Szeider, Stefan, SAT-encodings for special treewidth and pathwidth, 429-445 [Zbl 1496.68266]


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


Zbl 1337.68009
Full Text: DOI