![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
22nd SAT 2019: Lisbon, Portugal
- Mikolás Janota, Inês Lynce:
Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings. Lecture Notes in Computer Science 11628, Springer 2019, ISBN 978-3-030-24257-2 - Albert Atserias, Massimo Lauria
:
Circular (Yet Sound) Proofs. 1-18 - Olaf Beyersdorff
, Leroy Chew
, Judith Clymo, Meena Mahajan
:
Short Proofs in QBF Expansion. 19-35 - Joshua Blinkhorn, Olaf Beyersdorff
:
Proof Complexity of QBF Symmetry Recomputation. 36-52 - Oleksii Omelchenko, Andrei A. Bulatov:
Satisfiability Threshold for Power Law Random 2-SAT in Configuration Model. 53-70 - Sam Buss, Neil Thapen:
DRAT Proofs, Propagation Redundancy, and Extended Resolution. 71-89 - Florent Capelli
:
Knowledge Compilation Languages as Proof Systems. 90-99 - Leroy Chew
, Judith Clymo:
The Equivalences of Refutational QRAT. 100-116 - Akhil A. Dixit, Phokion G. Kolaitis:
A SAT-Based System for Consistent Query Answering. 117-135 - Katalin Fazekas
, Armin Biere
, Christoph Scholl:
Incremental Inprocessing in SAT Solving. 136-154 - Marijn J. H. Heule
, Manuel Kauers, Martina Seidl:
Local Search for Fast Matrix Multiplication. 155-163 - Randy Hickey, Fahiem Bacchus:
Speeding Up Assumption-Based SAT. 164-182 - Sima Jamali, David Mitchell:
Simplifying CDCL Clause Database Reduction. 183-192 - Benjamin Kiesl, Martina Seidl:
QRAT Polynomially Simulates ∀ \text -Exp+Res. 193-202 - Florian Lonsing
, Uwe Egly:
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. 203-210 - Carlos Mencía
, Oliver Kullmann, Alexey Ignatiev
, João Marques-Silva:
On Computing the Union of MUSes. 211-221 - Stefan Mengel, Romain Wallon
:
Revisiting Graph Width Measures for CNF-Encodings. 222-238 - António Morgado
, Alexey Ignatiev
, Maria Luisa Bonet, João Marques-Silva, Sam Buss:
DRMaxSAT with MaxHS: First Contact. 239-249 - Sibylle Möhle
, Armin Biere
:
Backing Backtracking. 250-266 - Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev
, João Marques-Silva:
Assessing Heuristic Machine Learning Explanations with Model Counting. 267-278 - Andres Nötzli
, Andrew Reynolds
, Haniel Barbosa
, Aina Niemetz
, Mathias Preiner
, Clark W. Barrett
, Cesare Tinelli
:
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. 279-297 - Alex Ozdemir
, Aina Niemetz
, Mathias Preiner
, Yoni Zohar
, Clark W. Barrett
:
DRAT-based Bit-Vector Proofs in CVC4. 298-305 - Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
:
Combining Resolution-Path Dependencies with Dependency Learning. 306-318 - Tomás Peitl, Friedrich Slivovsky, Stefan Szeider
:
Proof Complexity of Fragments of Long-Distance Q-Resolution. 319-335 - Daniel Selsam, Nikolaj S. Bjørner:
Guiding High-Performance SAT Solvers with Unsat-Core Predictions. 336-353 - Andy Shih, Adnan Darwiche, Arthur Choi:
Verifying Binarized Neural Networks by Angluin-Style Learning. 354-370 - Mate Soos, Raghav Kulkarni, Kuldeep S. Meel:
CrystalBall: Gazing in the Black Box of SAT Solving. 371-387 - Leander Tentrup
, Markus N. Rabe:
Clausal Abstraction for DQBF. 388-405 - Nikhil Vyas, R. Ryan Williams:
On Super Strong ETH. 406-423
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.