


default search action
19th SAT 2016: Bordeaux, France
- Nadia Creignou, Daniel Le Berre:

Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Lecture Notes in Computer Science 9710, Springer 2016, ISBN 978-3-319-40969-6
Complexity
- Stefan Mengel:

Parameterized Compilation Lower Bounds for Restricted CNF-Formulas. 3-12 - Mateus de Oliveira Oliveira:

Satisfiability via Smooth Pictures. 13-28 - Patrick Scharpfenecker

, Jacobo Torán:
Solution-Graphs of Boolean Formulas and Isomorphism. 29-44 - Johannes Klaus Fichte, Arne Meier

, Irina Schindler:
Strong Backdoors for Default Logic. 45-59 - Daniel Berend

, Yochai Twitto:
The Normalized Autocorrelation Length of Random Max r -Sat Converges in Probability to (1-1/2^r)/r. 60-76 - Vsevolod Oparin:

Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle. 77-84
Satisfiability Solving
- Gilles Audemard, Laurent Simon:

Extreme Cases in SAT Problems. 87-103 - Jo Devriendt, Bart Bogaerts

, Maurice Bruynooghe, Marc Denecker:
Improved Static Symmetry Breaking for SAT. 104-122 - Jia Hui Liang, Vijay Ganesh

, Pascal Poupart, Krzysztof Czarnecki:
Learning Rate Based Branching Heuristic for SAT Solvers. 123-140 - Nathan Mull, Daniel J. Fremont

, Sanjit A. Seshia:
On the Hardness of SAT with Community Structure. 141-159 - Jan Elffers, Jan Johannsen, Massimo Lauria

, Thomas Magnard, Jakob Nordström
, Marc Vinyals
:
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers. 160-176
Satisfiability Applications
- Neha Lodha, Sebastian Ordyniak

, Stefan Szeider
:
A SAT Approach to Branchwidth. 179-195 - C. K. Cuong, M. J. H. Heule

:
Computing Maximum Unavoidable Subgraphs Using SAT Solvers. 196-211 - Mathias Soeken, Alan Mishchenko, Ana Petkovska, Baruch Sterin, Paolo Ienne, Robert K. Brayton, Giovanni De Micheli:

Heuristic NPN Classification for Large Functions Using AIGs and LEXSAT. 212-227 - Marijn J. H. Heule

, Oliver Kullmann, Victor W. Marek:
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. 228-245
Satisfiability Modulo Theory
- Aleksandar Zeljic, Christoph M. Wintersteiger

, Philipp Rümmer:
Deciding Bit-Vector Formulas with mcSAT. 249-266 - Martin Jonás

, Jan Strejcek
:
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. 267-283 - Lorenzo Candeago

, Daniel Larraz
, Albert Oliveras, Enric Rodríguez-Carbonell
, Albert Rubio:
Speeding up the Constraint-Based Method in Difference Logic. 284-301 - Jeevana Priya Inala, Rohit Singh, Armando Solar-Lezama:

Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers. 302-320
Beyond SAT
- Giles Reger

, Martin Suda
, Andrei Voronkov:
Finding Finite Models in Multi-sorted First-Order Logic. 323-341 - Carlos Mencía

, Alexey Ignatiev
, Alessandro Previti, João Marques-Silva:
MCS Extraction with Sublinear Oracle Queries. 342-360 - Zurab Khasidashvili, Konstantin Korovin

:
Predicate Elimination for Preprocessing in First-Order Theorem Proving. 361-372
Quantified Boolean Formula
- Markus N. Rabe, Sanjit A. Seshia:

Incremental Determinization. 375-392 - Leander Tentrup:

Non-prenex QBF Solving Using Abstraction. 393-401 - Mikolás Janota

:
On Q-Resolution and CDCL QBF Solving. 402-418 - Uwe Egly:

On Stronger Calculi for QBFs. 419-434 - Florian Lonsing

, Uwe Egly, Martina Seidl:
Q-Resolution with Generalized Axioms. 435-452 - Valeriy Balabanov, Jie-Hong Roland Jiang, Christoph Scholl, Alan Mishchenko, Robert K. Brayton:

2QBF: Challenges and Solutions. 453-469
Dependency QBF
- Ralf Wimmer

, Christoph Scholl, Karina Wimmer, Bernd Becker
:
Dependency Schemes for DQBF. 473-489 - Olaf Beyersdorff

, Leroy Chew, Renate A. Schmidt
, Martin Suda
:
Lifting QBF Resolution Calculi to DQBF. 490-499 - Tomás Peitl, Friedrich Slivovsky, Stefan Szeider

:
Long Distance Q-Resolution with Dependency Schemes. 500-518
Tools
- M. Fareed Arif, Carlos Mencía

, Alexey Ignatiev
, Norbert Manthey, Rafael Peñaloza, João Marques-Silva:
BEACON: An Efficient SAT-Based Tool for Debugging EL^+ Ontologies. 521-530 - Tomás Balyo, Florian Lonsing

:
HordeQBF: A Modular and Massively Parallel QBF Solver. 531-538 - Paul Saikko

, Jeremias Berg
, Matti Järvisalo
:
LMHS: A SAT-IP Hybrid MaxSAT Solver. 539-546 - Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina

:
OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. 547-553 - Norbert Manthey, Marius Lindauer

:
SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers. 554-561

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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














