Portal - SAT 2023

SAT 2023	July 4-8, 2023, Alghero, Italy
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) Meena Mahajan and Friedrich Slivovsky (Eds.)
ISBN 978-3-95977-286-0, LIPICS Vol. 271	ISSN 1868-8969

Additional Information

License
Conference Website
Complete volume (PDF, 11 MB)
Search Publication Server

Authors

Heisinger, Maximilian

Spachmann, Luc Nicolas

Front Matter, Table of Contents, Preface, Conference Organization

Authors: Mahajan, Meena ; Slivovsky, Friedrich

Abstract | Document (571 KB) | BibTeX

Algorithms Transcending the SAT-Symmetry Interface

Authors: Anders, Markus ; Schweitzer, Pascal ; Soos, Mate

Abstract | Document (829 KB) | BibTeX

Proof Complexity of Propositional Model Counting

Authors: Beyersdorff, Olaf ; Hoffmann, Tim ; Spachmann, Luc Nicolas

Abstract | Document (760 KB) | BibTeX

CadiBack: Extracting Backbones with CaDiCaL

Authors: Biere, Armin ; Froleyks, Nils ; Wang, Wenxi

Abstract | Document (1,021 KB) | BibTeX

QCDCL vs QBF Resolution: Further Insights

Authors: Böhm, Benjamin ; Beyersdorff, Olaf

Abstract | Document (972 KB) | BibTeX

Polynomial Calculus for MaxSAT

Authors: Bonacina, Ilario ; Bonet, Maria Luisa ; Levy, Jordi

Abstract | Document (855 KB) | BibTeX

Certified Knowledge Compilation with Application to Verified Model Counting

Authors: Bryant, Randal E. ; Nawrocki, Wojciech ; Avigad, Jeremy ; Heule, Marijn J. H.

Abstract | Document (906 KB) | BibTeX

Separating Incremental and Non-Incremental Bottom-Up Compilation

Authors: de Colnet, Alexis

Abstract | Document (807 KB) | BibTeX

IPASIR-UP: User Propagators for CDCL

Authors: Fazekas, Katalin ; Niemetz, Aina ; Preiner, Mathias ; Kirchweger, Markus ; Szeider, Stefan ; Biere, Armin

Abstract | Document (797 KB) | BibTeX

AllSAT for Combinational Circuits

Authors: Fried, Dror ; Nadel, Alexander ; Shalmon, Yogev

Abstract | Document (852 KB) | BibTeX

On the Complexity of k-DQBF

Authors: Fung, Long-Hin ; Tan, Tony

Abstract | Document (724 KB) | BibTeX

Effective Auxiliary Variables via Structured Reencoding

Authors: Haberlandt, Andrew ; Green, Harrison ; Heule, Marijn J. H.

Abstract | Document (3,903 KB) | BibTeX

An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming

Authors: Katsirelos, George

Abstract | Document (789 KB) | BibTeX

A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture

Authors: Kirchweger, Markus ; Peitl, Tomáš ; Szeider, Stefan

Abstract | Document (770 KB) | BibTeX

SAT-Based Generation of Planar Graphs

Authors: Kirchweger, Markus ; Scheucher, Manfred ; Szeider, Stefan

Abstract | Document (707 KB) | BibTeX

On CNF Conversion for Disjoint SAT Enumeration

Authors: Masina, Gabriele ; Spallitta, Giuseppe ; Sebastiani, Roberto

Abstract | Document (2,027 KB) | BibTeX

Bounds on BDD-Based Bucket Elimination

Authors: Mengel, Stefan

Abstract | Document (609 KB) | BibTeX

Solving Huge Instances with Intel(R) SAT Solver

Authors: Nadel, Alexander

Abstract | Document (775 KB) | BibTeX

Learning Shorter Redundant Clauses in SDCL Using MaxSAT

Authors: Oliveras, Albert ; Li, Chunxiao ; Wu, Darryl ; Chung, Jonathan ; Ganesh, Vijay

Abstract | Document (800 KB) | BibTeX

UpMax: User Partitioning for MaxSAT

Authors: Orvalho, Pedro ; Manquinho, Vasco ; Martins, Ruben

Abstract | Document (920 KB) | BibTeX

QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas

Authors: Plank, Andreas ; Seidl, Martina

Abstract | Document (779 KB) | BibTeX

Faster LRAT Checking Than Solving with CaDiCaL

Authors: Pollitt, Florian ; Fleury, Mathias ; Biere, Armin

Abstract | Document (806 KB) | BibTeX

Even Shorter Proofs Without New Variables

Authors: Rebola-Pardo, Adrián

Abstract | Document (828 KB) | BibTeX

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Authors: Schwarzová, Tereza ; Strejček, Jan ; Major, Juraj

Abstract | Document (889 KB) | BibTeX

Validation of QBF Encodings with Winning Strategies

Authors: Shaik, Irfansha ; Heisinger, Maximilian ; Seidl, Martina ; van de Pol, Jaco

Abstract | Document (641 KB) | BibTeX

Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT

Authors: Sharma, Anshujit ; Burns, Matthew ; Huang, Michael C.

Abstract | Document (4,336 KB) | BibTeX

Cutting Planes Width and the Complexity of Graph Isomorphism Refutations

Authors: Torán, Jacobo ; Wörz, Florian

Abstract | Document (885 KB) | BibTeX

Limits of CDCL Learning via Merge Resolution

Authors: Vinyals, Marc ; Li, Chunxiao ; Fleming, Noah ; Kolokolova, Antonina ; Ganesh, Vijay

Abstract | Document (675 KB) | BibTeX

Explaining SAT Solving Using Causal Reasoning

Authors: Yang, Jiong ; Shaw, Arijit ; Baluta, Teodora ; Soos, Mate ; Meel, Kuldeep S.

Abstract | Document (864 KB) | BibTeX

LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem

Authors: Zhou, Junping ; Liang, Jiaxin ; Yin, Minghao ; He, Bo

Abstract | Document (1,071 KB) | BibTeX

A Comparison of SAT Encodings for Acyclicity of Directed Graphs

Authors: Zhou, Neng-Fa ; Wang, Ruiwei ; Yap, Roland H. C.

Abstract | Document (615 KB) | BibTeX

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI

26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)