An extensible circuit-based SAT solver

References

• Asín, R., Nieuwenhuis, R., Oliveras, A., & Rodríguez-Carbonell, E. (2009). Cardinality networks and their applications. In O. Kullmann (Ed.), Theory and Applications of Satisfiability Testing (SAT) (pp. 167–180). Berlin, Heidelberg: Springer Berlin Heidelberg.
   Google Scholar
• Audemard, G., & Simon, L. (2009). Predicting learnt clauses quality in modern SAT solvers. Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI) (pp. 399–404). San Francisco, CA, USA: Morgan Kaufmann Publishers Inc.
   Google Scholar
• Audemard, G., & Simon, L. (2012a). Glucose 2.1: Aggressive but reactive clause database management, dynamic restarts. Proceedings of the Workshop on Pragmatics of SAT (Workshop of SAT’12), Trento, Italy.
   Google Scholar
• Audemard, G., & Simon, L. (2012b). Refining restarts strategies for SAT and UNSAT. Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP) (pp. 118–126). Berlin, Heidelberg: Springer-Verlag.
   Google Scholar
• Barrett, C., Roberto Sebastiani, S. A. S., & Tinelli, C. (2009). Satisfiability modulo theories. In Clarke, E. M., Henzinger, T. A., Veith, H., & Bloem, R. (Eds.), Handbook of Model Checking (pp. 305–343). Springer International Publishing, Cham.
   Google Scholar
• Batcher, K. E. (1968). Sorting networks and their applications. Proceedings of the April 30–May 2, 1968, Spring Joint Computer Conference, AFIPS ‘68 (Spring) (pp. 307–314). New York, NY, USA: ACM.
   Google Scholar
• Beanie, P., Kautz, H., & Sabharwal, A. (2003a). Using problem structure for efficient clause learning. In Giunchiglia, E., & Tacchella, A. (Eds.), Theory and Applications of Satisfiability Testing (pp. 242–256), Berlin, Heidelberg. Springer Berlin Heidelberg.
   Google Scholar
• Beanie, P., Kautz, H. A., & Sabharwal, A. (2003b). Understanding the power of clause learning. Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI) (pp. 1194–1201), San Francisco, CA, USA. Morgan Kaufmann Publishers Inc.
   Google Scholar
• Cook, S. A. (1971). The complexity of theorem-proving procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing, (STOC) (pp. 151–158). New York, NY, USA: ACM.
   Google Scholar
• Eén, N., & Sörensson, N. (2003). An extensible SAT-solver. In Giunchiglia, E., & Tacchella, A. (Eds.), Theory and Applications of Satisfiability Testing (SAT) (pp. 502–518), Berlin, Heidelberg. Springer Berlin Heidelberg.
   Google Scholar
• Manquinho, V. M., & Silva, J. P. M. (2005). Satisfiability-based algorithms for pseudoboolean optimization using gomory cuts and search restarts. 17th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2005), 14–16 November 2005 (pp. 150–155). Hong Kong, China.
   Google Scholar
• Marijn, J. H., Heule, M. J., & Suda, M. (2018). Proceedings of SAT competition 2018: Solver and benchmark descriptions (pp. B-2018-1). Helsink: Department of Computer Science Series of Publications B, Department of Computer Science, University of Helsinki.
   Google Scholar
• Marques-Silva, J. (2008). Practical applications of boolean satisfiability. Proceedings of the 9th International Workshop on Discrete Event Systems (pp. 74–80), Goteborg, Sweden.
   Google Scholar
• Metodi, A., Stern, R., Kalech, M., & Codish, M. (2014). A novel SAT-based approach to model based diagnosis. Journal of Artificial Intelligence Research, 51, 377–411.
   Web of Science ®Google Scholar
• Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient sat solver. Proceedings of the 38th conference on Design automation (DAC) (pp. 530–535). New York, NY, USA: ACM Press.
   Google Scholar
• Pipatsrisawat, K., & Darwiche, A. (2007). A lightweight component caching scheme for satisfiability solvers. In J. Marques-Silva & K. A. Sakallah (Eds.), Theory and Applications of Satisfiability Testing (SAT) (pp. 294–299). Berlin, Heidelberg: Springer Berlin Heidelberg.
   Google Scholar
• Reiter, R. (1987). A theory of diagnosis from first principles. Artificial Intelligence, 32(1), 57–95.
   Web of Science ®Google Scholar
• Siddiqi, S., & Huang, J. (2007). Hierarchical diagnosis of multiple faults. Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI) (pp. 581–586), San Francisco, CA, USA. Morgan Kaufmann Publishers Inc.
   Google Scholar
• Siddiqi, S. A. (2011). Computing minimum-cardinality diagnoses by model relaxation. Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI) (pp. 1087–1092), California, USA. AAAI Press.
   Google Scholar
• Thiffault, C., Bacchus, F., & Walsh, T. (2004). Solving non-clausal formulas with DPLL search. In Wallace, M. (Ed.), Principles and Practice of Constraint Programming (CP) (pp. 663–678), Berlin, Heidelberg. Springer Berlin Heidelberg.
   Google Scholar
• Tom Balyo, M. J. H. H., & Jrvisalo, M. (2017). Proceedings of SAT competition 2017: Solver and benchmark descriptions (pp. B-2017-1). Helsink: Department of Computer Science Series of Publications B, Department of Computer Science, University of Helsinki.
   Google Scholar
• Tseitin, G. S. (1970). On the complexity of derivation in propositional calculus. In J. Siekmann & G. Wrightson (Eds.), Automation of reasoning: Classical papers in computational logic 1967–1970 (Vol. 2) (pp. 466–483), Springer Berlin Heidelberg, Berlin, Heidelberg.
   Google Scholar
• Wu, C. A., Lin, T. H., Lee, C. C., & Huang, C. Y. (2007). QuteSAT: A robust circuit- based SAT solver for complex circuit structure. In R. Lauwereins & J. Madsen (Eds.), DATE (pp. 1313–1318). San Jose, CA, USA: EDA Consortium.
   Google Scholar
• Zhang, L., Madigan, C. F., Moskewicz, M. H., & Malik, S. (2001). Efficient conflict driven learning in a boolean satisfiability solver. Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design (ICCAD) (pp. 279–285). Piscat- away, NJ, USA: IEEE Press.
   Google Scholar