@Proceedings{meel_et_al:LIPIcs.SAT.2022,
title = {{LIPIcs, Volume 236, SAT 2022, Complete Volume}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {1--618},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022},
URN = {urn:nbn:de:0030-drops-166736},
doi = {10.4230/LIPIcs.SAT.2022},
annote = {Keywords: LIPIcs, Volume 236, SAT 2022, Complete Volume}
}
@InProceedings{meel_et_al:LIPIcs.SAT.2022.0,
author = {Meel, Kuldeep S. and Strichman, Ofer},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.0},
URN = {urn:nbn:de:0030-drops-166746},
doi = {10.4230/LIPIcs.SAT.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{anders:LIPIcs.SAT.2022.1,
author = {Anders, Markus},
title = {{SAT Preprocessors and Symmetry}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {1:1--1:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.1},
URN = {urn:nbn:de:0030-drops-166752},
doi = {10.4230/LIPIcs.SAT.2022.1},
annote = {Keywords: boolean satisfiability, symmetry exploitation, graph isomorphism}
}
@InProceedings{bach_et_al:LIPIcs.SAT.2022.2,
author = {Bach, Jakob and Iser, Markus and B\"{o}hm, Klemens},
title = {{A Comprehensive Study of k-Portfolios of Recent SAT Solvers}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {2:1--2:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.2},
URN = {urn:nbn:de:0030-drops-166767},
doi = {10.4230/LIPIcs.SAT.2022.2},
annote = {Keywords: Propositional satisfiability, solver portfolios, runtime prediction, machine learning, integer programming}
}
@InProceedings{garzon_et_al:LIPIcs.SAT.2022.3,
author = {Garz\'{o}n, Iv\'{a}n and Mesejo, Pablo and Gir\'{a}ldez-Cru, Jes\'{u}s},
title = {{On the Performance of Deep Generative Models of Realistic SAT Instances}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {3:1--3:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.3},
URN = {urn:nbn:de:0030-drops-166775},
doi = {10.4230/LIPIcs.SAT.2022.3},
annote = {Keywords: Realistic SAT generators, pseudo-industrial random SAT, deep generative models, deep learning}
}
@InProceedings{kirchweger_et_al:LIPIcs.SAT.2022.4,
author = {Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
title = {{A SAT Attack on Rota’s Basis Conjecture}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {4:1--4:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.4},
URN = {urn:nbn:de:0030-drops-166780},
doi = {10.4230/LIPIcs.SAT.2022.4},
annote = {Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, Rota’s basis conjecture, matroid}
}
@InProceedings{schleitzer_et_al:LIPIcs.SAT.2022.5,
author = {Schleitzer, Agnes and Beyersdorff, Olaf},
title = {{Classes of Hard Formulas for QBF Resolution}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {5:1--5:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.5},
URN = {urn:nbn:de:0030-drops-166792},
doi = {10.4230/LIPIcs.SAT.2022.5},
annote = {Keywords: QBF, proof complexity, resolution, separations}
}
@InProceedings{itsykson_et_al:LIPIcs.SAT.2022.6,
author = {Itsykson, Dmitry and Riazanov, Artur and Smirnov, Petr},
title = {{Tight Bounds for Tseitin Formulas}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {6:1--6:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.6},
URN = {urn:nbn:de:0030-drops-166805},
doi = {10.4230/LIPIcs.SAT.2022.6},
annote = {Keywords: Proof complexity, Tseitin formulas, treewidth, resolution, OBDD-based proof systems}
}
@InProceedings{janota_et_al:LIPIcs.SAT.2022.7,
author = {Janota, Mikol\'{a}\v{s} and Piepenbrock, Jelle and Piotrowski, Bartosz},
title = {{Towards Learning Quantifier Instantiation in SMT}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.7},
URN = {urn:nbn:de:0030-drops-166810},
doi = {10.4230/LIPIcs.SAT.2022.7},
annote = {Keywords: satisfiability modulo theories, quantifier instantiation, machine learning}
}
@InProceedings{nadel:LIPIcs.SAT.2022.8,
author = {Nadel, Alexander},
title = {{Introducing Intel(R) SAT Solver}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {8:1--8:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.8},
URN = {urn:nbn:de:0030-drops-166825},
doi = {10.4230/LIPIcs.SAT.2022.8},
annote = {Keywords: SAT, CDCL, MaxSAT}
}
@InProceedings{mosse_et_al:LIPIcs.SAT.2022.9,
author = {Moss\'{e}, Milan and Sha, Harry and Tan, Li-Yang},
title = {{A Generalization of the Satisfiability Coding Lemma and Its Applications}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.9},
URN = {urn:nbn:de:0030-drops-166837},
doi = {10.4230/LIPIcs.SAT.2022.9},
annote = {Keywords: Prime Implicants, Satisfiability Coding Lemma, Blake Canonical Form, k-SAT}
}
@InProceedings{chew_et_al:LIPIcs.SAT.2022.10,
author = {Chew, Leroy and Heule, Marijn J. H.},
title = {{Relating Existing Powerful Proof Systems for QBF}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {10:1--10:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.10},
URN = {urn:nbn:de:0030-drops-166845},
doi = {10.4230/LIPIcs.SAT.2022.10},
annote = {Keywords: QBF, Proof Complexity, Verification, Strategy Extraction, Sequent Calculus}
}
@InProceedings{bohm_et_al:LIPIcs.SAT.2022.11,
author = {B\"{o}hm, Benjamin and Peitl, Tom\'{a}\v{s} and Beyersdorff, Olaf},
title = {{Should Decisions in QCDCL Follow Prefix Order?}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.11},
URN = {urn:nbn:de:0030-drops-166850},
doi = {10.4230/LIPIcs.SAT.2022.11},
annote = {Keywords: QBF, CDCL, proof complexity, lower bounds}
}
@InProceedings{jabs_et_al:LIPIcs.SAT.2022.12,
author = {Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J\"{a}rvisalo, Matti},
title = {{MaxSAT-Based Bi-Objective Boolean Optimization}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.12},
URN = {urn:nbn:de:0030-drops-166863},
doi = {10.4230/LIPIcs.SAT.2022.12},
annote = {Keywords: Multi-objective optimization, Pareto front enumeration, bi-objective optimization, maximum satisfiability, incremental SAT}
}
@InProceedings{smirnov_et_al:LIPIcs.SAT.2022.13,
author = {Smirnov, Pavel and Berg, Jeremias and J\"{a}rvisalo, Matti},
title = {{Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.13},
URN = {urn:nbn:de:0030-drops-166871},
doi = {10.4230/LIPIcs.SAT.2022.13},
annote = {Keywords: constraint optimization, pseudo-Boolean optimization, implicit hitting sets, solution-improving search, unsatisfiable cores}
}
@InProceedings{niskanen_et_al:LIPIcs.SAT.2022.14,
author = {Niskanen, Andreas and Berg, Jeremias and J\"{a}rvisalo, Matti},
title = {{Incremental Maximum Satisfiability}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {14:1--14:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.14},
URN = {urn:nbn:de:0030-drops-166885},
doi = {10.4230/LIPIcs.SAT.2022.14},
annote = {Keywords: maximum satisfiability, MaxSAT, incremental optimization, API, implicit hitting set approach}
}
@InProceedings{ganian_et_al:LIPIcs.SAT.2022.15,
author = {Ganian, Robert and Pokr\'{y}vka, Filip and Schidler, Andr\'{e} and Simonov, Kirill and Szeider, Stefan},
title = {{Weighted Model Counting with Twin-Width}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.15},
URN = {urn:nbn:de:0030-drops-166896},
doi = {10.4230/LIPIcs.SAT.2022.15},
annote = {Keywords: Weighted model counting, twin-width, parameterized complexity, SAT}
}
@InProceedings{gocht_et_al:LIPIcs.SAT.2022.16,
author = {Gocht, Stephan and Martins, Ruben and Nordstr\"{o}m, Jakob and Oertel, Andy},
title = {{Certified CNF Translations for Pseudo-Boolean Solving}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {16:1--16:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.16},
URN = {urn:nbn:de:0030-drops-166901},
doi = {10.4230/LIPIcs.SAT.2022.16},
annote = {Keywords: pseudo-Boolean solving, 0-1 integer linear program, proof logging, certifying algorithms, certified translation, CNF encoding, cutting planes}
}
@InProceedings{mengel:LIPIcs.SAT.2022.17,
author = {Mengel, Stefan},
title = {{Changing Partitions in Rectangle Decision Lists}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {17:1--17:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.17},
URN = {urn:nbn:de:0030-drops-166913},
doi = {10.4230/LIPIcs.SAT.2022.17},
annote = {Keywords: rectangle decision lists, QBF proof complexity, OBDD}
}
@InProceedings{berent_et_al:LIPIcs.SAT.2022.18,
author = {Berent, Lucas and Burgholzer, Lukas and Wille, Robert},
title = {{Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.18},
URN = {urn:nbn:de:0030-drops-166927},
doi = {10.4230/LIPIcs.SAT.2022.18},
annote = {Keywords: Satisfiability, Quantum Computing, Design Automation, Clifford Circuits}
}
@InProceedings{bannach_et_al:LIPIcs.SAT.2022.19,
author = {Bannach, Max and Skambath, Malte and Tantau, Till},
title = {{On the Parallel Parameterized Complexity of MaxSAT Variants}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {19:1--19:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.19},
URN = {urn:nbn:de:0030-drops-166934},
doi = {10.4230/LIPIcs.SAT.2022.19},
annote = {Keywords: max-sat, almost-sat, parallel algorithms, fixed-parameter tractability}
}
@InProceedings{reichl_et_al:LIPIcs.SAT.2022.20,
author = {Reichl, Franz-Xaver and Slivovsky, Friedrich},
title = {{Pedant: A Certifying DQBF Solver}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {20:1--20:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.20},
URN = {urn:nbn:de:0030-drops-166941},
doi = {10.4230/LIPIcs.SAT.2022.20},
annote = {Keywords: DQBF, DQBF Solver, Decision Procedure, Certificates}
}
@InProceedings{subercaseaux_et_al:LIPIcs.SAT.2022.21,
author = {Subercaseaux, Bernardo and Heule, Marijn J.H.},
title = {{The Packing Chromatic Number of the Infinite Square Grid Is at Least 14}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {21:1--21:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.21},
URN = {urn:nbn:de:0030-drops-166951},
doi = {10.4230/LIPIcs.SAT.2022.21},
annote = {Keywords: packing coloring, SAT solvers, encodings}
}
@InProceedings{mahajan_et_al:LIPIcs.SAT.2022.22,
author = {Mahajan, Meena and Sood, Gaurav},
title = {{QBF Merge Resolution Is Powerful but Unnatural}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {22:1--22:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.22},
URN = {urn:nbn:de:0030-drops-166969},
doi = {10.4230/LIPIcs.SAT.2022.22},
annote = {Keywords: QBF, proof complexity, resolution, weakening, restrictions}
}
@InProceedings{wang_et_al:LIPIcs.SAT.2022.23,
author = {Wang, Hao-Ren and Tu, Kuan-Hua and Jiang, Jie-Hong Roland and Scholl, Christoph},
title = {{Quantifier Elimination in Stochastic Boolean Satisfiability}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.23},
URN = {urn:nbn:de:0030-drops-166970},
doi = {10.4230/LIPIcs.SAT.2022.23},
annote = {Keywords: Stochastic Boolean Satisfiability, Quantifier Elimination, Decision Procedure}
}
@InProceedings{slivovsky:LIPIcs.SAT.2022.24,
author = {Slivovsky, Friedrich},
title = {{Quantified CDCL with Universal Resolution}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {24:1--24:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.24},
URN = {urn:nbn:de:0030-drops-166986},
doi = {10.4230/LIPIcs.SAT.2022.24},
annote = {Keywords: QBF, Q-Resolution, QU-Resolution, CDCL}
}
@InProceedings{alos_et_al:LIPIcs.SAT.2022.25,
author = {Al\`{o}s, Josep and Ans\'{o}tegui, Carlos and Salvia, Josep M. and Torres, Eduard},
title = {{OptiLog V2: Model, Solve, Tune and Run}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.25},
URN = {urn:nbn:de:0030-drops-166996},
doi = {10.4230/LIPIcs.SAT.2022.25},
annote = {Keywords: Tool framework, Satisfiability, Modelling, Solving}
}
@InProceedings{narodytska_et_al:LIPIcs.SAT.2022.26,
author = {Narodytska, Nina and Bj{\o}rner, Nikolaj},
title = {{Analysis of Core-Guided MaxSat Using Cores and Correction Sets}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {26:1--26:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.26},
URN = {urn:nbn:de:0030-drops-167006},
doi = {10.4230/LIPIcs.SAT.2022.26},
annote = {Keywords: maximum satisfiability, unsatisfiable cores, correction sets}
}
@InProceedings{biere_et_al:LIPIcs.SAT.2022.27,
author = {Biere, Armin and Chowdhury, Md Solimul and Heule, Marijn J. H. and Kiesl, Benjamin and Whalen, Michael W.},
title = {{Migrating Solver State}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {27:1--27:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.27},
URN = {urn:nbn:de:0030-drops-167015},
doi = {10.4230/LIPIcs.SAT.2022.27},
annote = {Keywords: SAT, SMT, Cloud Computing, Serverless Computing}
}
@InProceedings{audemard_et_al:LIPIcs.SAT.2022.28,
author = {Audemard, Gilles and Lagniez, Jean-Marie and Miceli, Marie},
title = {{A New Exact Solver for (Weighted) Max#SAT}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {28:1--28:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.28},
URN = {urn:nbn:de:0030-drops-167022},
doi = {10.4230/LIPIcs.SAT.2022.28},
annote = {Keywords: Max#SAT, EMaj-SAT, Weighted Projected Model Counting, SSAT}
}
@InProceedings{cabral_et_al:LIPIcs.SAT.2022.29,
author = {Cabral, Miguel and Janota, Mikol\'{a}\v{s} and Manquinho, Vasco},
title = {{SAT-Based Leximax Optimisation Algorithms}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {29:1--29:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.29},
URN = {urn:nbn:de:0030-drops-167030},
doi = {10.4230/LIPIcs.SAT.2022.29},
annote = {Keywords: Multi-Objective Optimisation, Leximax, Sorting Networks}
}
@InProceedings{fichte_et_al:LIPIcs.SAT.2022.30,
author = {Fichte, Johannes K. and Hecher, Markus and Roland, Valentin},
title = {{Proofs for Propositional Model Counting}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {30:1--30:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.30},
URN = {urn:nbn:de:0030-drops-167043},
doi = {10.4230/LIPIcs.SAT.2022.30},
annote = {Keywords: Model Counting, Verification, Certified Counting}
}
@InProceedings{jung_et_al:LIPIcs.SAT.2022.31,
author = {Jung, Jean Christoph and Mayer-Eichberger, Valentin and Saffidine, Abdallah},
title = {{QBF Programming with the Modeling Language Bule}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {31:1--31:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.31},
URN = {urn:nbn:de:0030-drops-167058},
doi = {10.4230/LIPIcs.SAT.2022.31},
annote = {Keywords: Modeling, QBF Programming, CNF Encodings}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing