×

zbMATH — the first resource for mathematics

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 this volume 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 06807215]
Ganian, Robert; Ramanujan, M. S.; Szeider, Stefan, Backdoor treewidth for SAT, 20-37 [Zbl 06807216]
Ganian, Robert; Szeider, Stefan, New width parameters for model counting, 38-52 [Zbl 06807217]
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 06807219]
Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice, Symmetric explanation learning: effective dynamic symmetry handling for SAT, 83-100 [Zbl 06807220]
Junttila, Tommi; Karppa, Matti; Kaski, Petteri; Kohonen, Jukka, An adaptive prefix-assignment technique for symmetry reduction, 101-118 [Zbl 06807221]
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 06807222]
Nabeshima, Hidetomo; Inoue, Katsumi, Coverage-based clause reduction heuristics for CDCL solvers, 136-144 [Zbl 06807223]
Cohen, Eldan; Huang, Guoyu; Beck, J. Christopher, (I can get) satisfaction: preference-based scheduling for concert-goers at multi-venue music festivals, 147-163 [Zbl 06807224]
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao, On tackling the limits of resolution in SAT solving, 164-183 [Zbl 06807225]
Previti, Alessandro; Mencía, Carlos; Järvisalo, Matti; Marques-Silva, Joao, Improving MCS enumeration via caching, 184-194 [Zbl 06807226]
Terra-Neves, Miguel; Lynce, Inês; Manquinho, Vasco, Introducing Pareto minimal correction subsets, 195-211 [Zbl 06807227]
Audemard, Gilles; Lagniez, Jean-Marie; Szczepanski, Nicolas; Tabary, Sébastien, A distributed version of Syrup, 215-232 [Zbl 06807228]
Le Frioux, Ludovic; Baarir, Souheib; Sopena, Julien; Kordon, Fabrice, Painless: a framework for parallel SAT solving, 233-250 [Zbl 06807229]
Nejati, Saeed; Newsham, Zack; Scott, Joseph; Liang, Jia Hui; Gebotys, Catherine; Poupart, Pascal; Ganesh, Vijay, A propagation rate based splitting heuristic for divide-and-conquer solvers, 251-260 [Zbl 06807230]
Blinkhorn, Joshua; Beyersdorff, Olaf, Shortening QBF proofs with dependency schemes, 263-280 [Zbl 06807231]
Kiesl, Benjamin; Heule, Marijn J. H.; Seidl, Martina, A little blocked literal goes a long way, 281-297 [Zbl 06807232]
Peitl, Tomáš; Slivovsky, Friedrich; Szeider, Stefan, Dependency learning for QBF, 298-313 [Zbl 06807233]
Rabe, Markus N., A resolution-style proof system for DQBF, 314-325 [Zbl 06807234]
Wimmer, Ralf; Karrenbauer, Andreas; Becker, Ruben; Scholl, Christoph; Becker, Bernd, From DQBF to QBF by dependency elimination, 326-343 [Zbl 06807235]
Hyvärinen, Antti E. J.; Asadi, Sepideh; Even-Mendoza, Karine; Fedyukovich, Grigory; Chockler, Hana; Sharygina, Natasha, Theory refinement for program verification, 347-363 [Zbl 06807236]
Jonáš, Martin; Strejček, Jan, On simplification of formulas with unconstrained variables and quantifiers, 364-379 [Zbl 06807237]
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 06807238]
Fichte, Johannes K.; Lodha, Neha; Szeider, Stefan, SAT-based local improvement for finding tree decompositions of small width, 401-411 [Zbl 06807239]
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 06807241]
Korhonen, Tuukka; Berg, Jeremias; Saikko, Paul; Järvisalo, Matti, Maxpre: an extended maxsat preprocessor, 449-456 [Zbl 06807242]
Lammich, Peter, The GRAT tool chain – efficient (UN)SAT certificate checking with formal correctness guarantees, 457-463 [Zbl 06807243]
Lauria, Massimo; Elffers, Jan; Nordström, Jakob; Vinyals, Marc, CNFgen: a generator of crafted benchmarks, 464-473 [Zbl 06807244]

MSC:
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
PDF BibTeX XML Cite
Full Text: DOI