Publications
2024
Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
Chew, L., De Colnet, A., Slivovsky, F., & Szeider, S. (n.d.). Hardness of Random Reordered Encodings of Parity for Resolution and CDCL. In Proceedings of the AAAI Conference on Artificial Intelligence Vol. 38 (pp. 7978-7986). Association for the Advancement of Artificial Intelligence (AAAI). doi:10.1609/aaai.v38i8.28635
2023
Circuit Minimization with QBF-Based Exact Synthesis
Reichl, F. -X., Slivovsky, F., & Szeider, S. (n.d.). Circuit Minimization with QBF-Based Exact Synthesis. Proceedings of the AAAI Conference on Artificial Intelligence, 37(4), 4087-4094. doi:10.1609/aaai.v37i4.25524
Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF
Fichte, J. K., Ganian, R., Hecher, M., Slivovsky, F., & Ordyniak, S. (2023). Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE. doi:10.1109/lics56636.2023.10175675
2022
Sum-of-Products with Default Values: Algorithms and Complexity Results
Ganian, R., Kim, E. J., Slivovsky, F., & Szeider, S. (n.d.). Sum-of-Products with Default Values: Algorithms and Complexity Results. Journal of Artificial Intelligence Research, 73, 535-552. doi:10.1613/jair.1.12370
2021
Engineering an Efficient Boolean Functional Synthesis Engine
Golia, P., Slivovsky, F., Roy, S., & Meel, K. S. (2021). Engineering an Efficient Boolean Functional Synthesis Engine. In 2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). IEEE. doi:10.1109/iccad51958.2021.9643583
Davis and Putnam Meet Henkin: Solving DQBF with Resolution
Blinkhorn, J., Peitl, T., & Slivovsky, F. (2021). Davis and Putnam Meet Henkin: Solving DQBF with Resolution. In Lecture Notes in Computer Science (pp. 30-46). Springer International Publishing. doi:10.1007/978-3-030-80223-3_4
2020
Fixed-Parameter Tractability of Dependency QBF with Structural Parameters
Ganian, R., Peitl, T., Slivovsky, F., & Szeider, S. (2020). Fixed-Parameter Tractability of Dependency QBF with Structural Parameters. In Proceedings of the Seventeenth International Conference on Principles of Knowledge Representation and Reasoning (pp. 392-402). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/kr.2020/40
2019
Qute in the QBF Evaluation 2018
Peitl, T., Slivovsky, F., & Szeider, S. (n.d.). Qute in the QBF Evaluation 2018. Journal on Satisfiability, Boolean Modeling and Computation, 11(1), 261-272. doi:10.3233/sat190124
Dependency Learning for QBF
Peitl, T., Slivovsky, F., & Szeider, S. (n.d.). Dependency Learning for QBF. Journal of Artificial Intelligence Research, 65, 181-208. doi:10.1613/jair.1.11529
Long-Distance Q-Resolution with Dependency Schemes.
Peitl, T., Slivovsky, F., & Szeider, S. (2019). Long-Distance Q-Resolution with Dependency Schemes.. Journal of automated reasoning, 63(1), 127-155. doi:10.1007/s10817-018-9467-3
2018
Sum-of-Products with Default Values: Algorithms and Complexity Results
Ganian, R., Kim, E. J., Slivovsky, F., & Szeider, S. (2018). Sum-of-Products with Default Values: Algorithms and Complexity Results. In 2018 IEEE 30th International Conference on Tools with Artificial Intelligence (ICTAI). IEEE. doi:10.1109/ictai.2018.00115
2017
On Compiling Structured CNFs to OBDDs.
Bova, S., & Slivovsky, F. (2017). On Compiling Structured CNFs to OBDDs.. Theory of computing systems, 61(2), 637-655. doi:10.1007/s00224-016-9715-z
2016
Model Counting for CNF Formulas of Bounded Modular Treewidth
Paulusma, D., Slivovsky, F., & Szeider, S. (2016). Model Counting for CNF Formulas of Bounded Modular Treewidth. Algorithmica, 76(1), 168-194. doi:10.1007/s00453-015-0030-x
Quantifier Reordering for QBF
Slivovsky, F., & Szeider, S. (2016). Quantifier Reordering for QBF. Journal of Automated Reasoning, 56(4), 459-477. doi:10.1007/s10817-015-9353-1
Meta-kernelization with structural parameters
Ganian, R., Slivovsky, F., & Szeider, S. (2016). Meta-kernelization with structural parameters. Journal of Computer and System Sciences, 82(2), 333-346. doi:10.1016/j.jcss.2015.08.003
Soundness of Q-resolution with dependency schemes
Slivovsky, F., & Szeider, S. (2016). Soundness of Q-resolution with dependency schemes. Theoretical Computer Science, 612, 83-101. doi:10.1016/j.tcs.2015.10.020