Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Markus Anders, Sofia Brenner, and Gaurav Rattan. The Complexity of Symmetry Breaking Beyond Lex-Leader. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{anders_et_al:LIPIcs.CP.2024.3, author = {Anders, Markus and Brenner, Sofia and Rattan, Gaurav}, title = {{The Complexity of Symmetry Breaking Beyond Lex-Leader}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {3:1--3:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.3}, URN = {urn:nbn:de:0030-drops-206881}, doi = {10.4230/LIPIcs.CP.2024.3}, annote = {Keywords: symmetry breaking, boolean satisfiability, matrix models, graph isomorphism} }
Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Alexandre Dubray, Pierre Schaus, and Siegfried Nijssen. Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dubray_et_al:LIPIcs.CP.2024.10, author = {Dubray, Alexandre and Schaus, Pierre and Nijssen, Siegfried}, title = {{Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {10:1--10:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.10}, URN = {urn:nbn:de:0030-drops-206956}, doi = {10.4230/LIPIcs.CP.2024.10}, annote = {Keywords: Projected Weighted Model Counting, Limited Discrepancy Search, Approximate Method, Probabilistic Inference} }
Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)
Oleg Zaikin. Inverting Step-Reduced SHA-1 and MD5 by Parameterized SAT Solvers. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{zaikin:LIPIcs.CP.2024.31, author = {Zaikin, Oleg}, title = {{Inverting Step-Reduced SHA-1 and MD5 by Parameterized SAT Solvers}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {31:1--31:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.31}, URN = {urn:nbn:de:0030-drops-207165}, doi = {10.4230/LIPIcs.CP.2024.31}, annote = {Keywords: cryptographic hash function, MD5, SHA-1, preimage attack, SAT, Cube-and-Conquer} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Markus Anders, Sofia Brenner, and Gaurav Rattan. Satsuma: Structure-Based Symmetry Breaking in SAT. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{anders_et_al:LIPIcs.SAT.2024.4, author = {Anders, Markus and Brenner, Sofia and Rattan, Gaurav}, title = {{Satsuma: Structure-Based Symmetry Breaking in SAT}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.4}, URN = {urn:nbn:de:0030-drops-205269}, doi = {10.4230/LIPIcs.SAT.2024.4}, annote = {Keywords: symmetry breaking, boolean satisfiability, graph isomorphism} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. Clausal Congruence Closure. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{biere_et_al:LIPIcs.SAT.2024.6, author = {Biere, Armin and Fazekas, Katalin and Fleury, Mathias and Froleyks, Nils}, title = {{Clausal Congruence Closure}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {6:1--6:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.6}, URN = {urn:nbn:de:0030-drops-205287}, doi = {10.4230/LIPIcs.SAT.2024.6}, annote = {Keywords: Satisfiability Solving, Congruence Closure, Structural Hashing, SAT Sweeping, Conjunctive Normal Form, Combinational Equivalence Checking, Hardware Equivalence Checking} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon. Entailing Generalization Boosts Enumeration. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{fried_et_al:LIPIcs.SAT.2024.13, author = {Fried, Dror and Nadel, Alexander and Sebastiani, Roberto and Shalmon, Yogev}, title = {{Entailing Generalization Boosts Enumeration}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {13:1--13:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.13}, URN = {urn:nbn:de:0030-drops-205351}, doi = {10.4230/LIPIcs.SAT.2024.13}, annote = {Keywords: Generalization, Minimization, Prime Implicant, AllSAT, SAT, Circuits} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Lukáš Holík and Pavol Vargovčík. Antichain with SAT and Tries. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{holik_et_al:LIPIcs.SAT.2024.15, author = {Hol{\'\i}k, Luk\'{a}\v{s} and Vargov\v{c}{\'\i}k, Pavol}, title = {{Antichain with SAT and Tries}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {15:1--15:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15}, URN = {urn:nbn:de:0030-drops-205372}, doi = {10.4230/LIPIcs.SAT.2024.15}, annote = {Keywords: SAT, Trie, Antichain, Alternating automata, Subset query} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards Universally Accessible SAT Technology. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ignatiev_et_al:LIPIcs.SAT.2024.16, author = {Ignatiev, Alexey and Tan, Zi Li and Karamanos, Christos}, title = {{Towards Universally Accessible SAT Technology}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {16:1--16:11}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.16}, URN = {urn:nbn:de:0030-drops-205382}, doi = {10.4230/LIPIcs.SAT.2024.16}, annote = {Keywords: PySAT, Python, Prototyping, Practical Applicability} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Yoichiro Iida, Tomohiro Sonobe, and Mary Inaba. Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{iida_et_al:LIPIcs.SAT.2024.17, author = {Iida, Yoichiro and Sonobe, Tomohiro and Inaba, Mary}, title = {{Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {17:1--17:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.17}, URN = {urn:nbn:de:0030-drops-205392}, doi = {10.4230/LIPIcs.SAT.2024.17}, annote = {Keywords: SAT Solver, Structure of SAT, Parallel application, Clause Learning} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Jean-Marie Lagniez, Pierre Marquis, and Armin Biere. Dynamic Blocked Clause Elimination for Projected Model Counting. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{lagniez_et_al:LIPIcs.SAT.2024.21, author = {Lagniez, Jean-Marie and Marquis, Pierre and Biere, Armin}, title = {{Dynamic Blocked Clause Elimination for Projected Model Counting}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {21:1--21:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.21}, URN = {urn:nbn:de:0030-drops-205430}, doi = {10.4230/LIPIcs.SAT.2024.21}, annote = {Keywords: Projected model counting, blocked clause elimination, propositional logic} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Speeding up Pseudo-Boolean Propagation. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2024.22, author = {Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui}, title = {{Speeding up Pseudo-Boolean Propagation}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.22}, URN = {urn:nbn:de:0030-drops-205449}, doi = {10.4230/LIPIcs.SAT.2024.22}, annote = {Keywords: SAT, Pseudo-Boolean Solving, Implementation-level Details} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Christoph Scholl, Tobias Seufert, and Fabian Siegwolf. Hierarchical Stochastic SAT and Quality Assessment of Logic Locking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{scholl_et_al:LIPIcs.SAT.2024.24, author = {Scholl, Christoph and Seufert, Tobias and Siegwolf, Fabian}, title = {{Hierarchical Stochastic SAT and Quality Assessment of Logic Locking}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {24:1--24:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.24}, URN = {urn:nbn:de:0030-drops-205462}, doi = {10.4230/LIPIcs.SAT.2024.24}, annote = {Keywords: Stochastic Boolean Satisfiability, Hierarchical Stochastic SAT, Binary Decision Diagrams, Decision Procedure} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Dominik Schreiber. Trusted Scalable SAT Solving with On-The-Fly LRAT Checking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{schreiber:LIPIcs.SAT.2024.25, author = {Schreiber, Dominik}, title = {{Trusted Scalable SAT Solving with On-The-Fly LRAT Checking}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {25:1--25:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.25}, URN = {urn:nbn:de:0030-drops-205477}, doi = {10.4230/LIPIcs.SAT.2024.25}, annote = {Keywords: SAT solving, distributed algorithms, proofs} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn J. H. Heule, and Bruno Dutertre. Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{yang_et_al:LIPIcs.SAT.2024.29, author = {Yang, Jiong and Kharkov, Yaroslav A. and Shi, Yunong and Heule, Marijn J. H. and Dutertre, Bruno}, title = {{Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {29:1--29:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.29}, URN = {urn:nbn:de:0030-drops-205517}, doi = {10.4230/LIPIcs.SAT.2024.29}, annote = {Keywords: Quantum computing, Quantum compilation, SAT solving, Incremental solving, Parallel solving} }
Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Markus Anders, Pascal Schweitzer, and Mate Soos. Algorithms Transcending the SAT-Symmetry Interface. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{anders_et_al:LIPIcs.SAT.2023.1, author = {Anders, Markus and Schweitzer, Pascal and Soos, Mate}, title = {{Algorithms Transcending the SAT-Symmetry Interface}}, booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)}, pages = {1:1--1:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-286-0}, ISSN = {1868-8969}, year = {2023}, volume = {271}, editor = {Mahajan, Meena and Slivovsky, Friedrich}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.1}, URN = {urn:nbn:de:0030-drops-184635}, doi = {10.4230/LIPIcs.SAT.2023.1}, annote = {Keywords: boolean satisfiability, symmetry exploitation, computational group theory} }
Feedback for Dagstuhl Publishing