摘要: We present sKizzo, a system designed to evaluate and certify QBFs by means of propositional skolemization symbolic reasoning.
springer.com
sci-hub.st 参考文章(10)
Marco Benedetti, a QBF decision procedure based on Propositional Skolemization and Symbolic Reasoning ,(2004)
Marco Benedetti, Extracting certificates from quantified boolean formulas international joint conference on artificial intelligence. pp. 47- 53 ,(2005)
Daniel Le Berre, Massimo Narizzano, Laurent Simon, Armando Tacchella, The Second QBF Solvers Comparative Evaluation Theory and Applications of Satisfiability Testing. pp. 376- 392 ,(2005) , 10.1007/11527695_28
Armin Biere, Resolve and Expand Theory and Applications of Satisfiability Testing. pp. 59- 70 ,(2005) , 10.1007/11527695_5
Marco Benedetti, Quantifier Trees for QBFs Theory and Applications of Satisfiability Testing. pp. 378- 385 ,(2005) , 10.1007/11499107_28
Reinhold Letz, Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas theorem proving with analytic tableaux and related methods. pp. 160- 175 ,(2002) , 10.1007/3-540-45616-3_12
Marco Benedetti, Evaluating QBFs via Symbolic Skolemization international conference on logic programming. pp. 285- 300 ,(2005) , 10.1007/978-3-540-32275-7_20
Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella, QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability international joint conference on automated reasoning. pp. 364- 369 ,(2001) , 10.1007/3-540-45744-5_27
Lintao Zhang, Sharad Malik, Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation principles and practice of constraint programming. pp. 200- 215 ,(2002) , 10.1007/3-540-46135-3_14
Abdelwaheb Ayari, David Basin, Bounded Model Construction for Monadic Second-Order Logics computer aided verification. pp. 99- 112 ,(2000) , 10.1007/10722167_11