A novel structure-exploiting encoding for SAT-based diagnosis

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). Springer.
   Google Scholar
• Audemard, G., & Simon, L. (2012a). Glucose 2.1: Aggressive - but reactive – clause database management, dynamic restarts. In International Workshop of Pragmatics of SAT (Affiliated to SAT), Trento, Italy.
   Google Scholar
• Audemard, G., & Simon, L. (2012b). Refining restarts strategies for SAT and UNSAT. In Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP), pp. 118–126, Berlin, Heidelberg. Springer-Verlag.
   Google Scholar
• Beanie, P., Kautz, H. A., & Sabharwal, A. (2003). Understanding the power of clause learning. In 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. In Proceedings of the Third Annual ACM Symposium on Theory of Computing (STOC), pp. 151–158, New York, NY, USA. ACM.
   Google Scholar
• Cook, S. A. (1976). A short proof of the pigeon hole principle using extended resolution. Sigact News, 8(4), 28–32. https://doi.org/10.1145/1008335.1008338
   Google Scholar
• Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem- proving. Communications of the ACM, 5(7), 394–397. https://doi.org/10.1145/368273.368557
   Web of Science ®Google Scholar
• Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM, 7(3), 201–215. https://doi.org/10.1145/321033.321034
   Web of Science ®Google Scholar
• Hansen, M. C., Yalcin, H., & Hayes, J. P. (1999). Unveiling the ISCAS-85 benchmarks: A case study in reverse engineering. Ieee Design & Test of Computers, 16(3), 72–80. https://doi.org/10.1109/54.785838
   Web of Science ®Google Scholar
• Huang, J., & Darwiche, A. (2005). On compiling system models for faster and more scalable diagnosis. In Proceedings of the 20th National Conference on Artificial Intelligence (AAAI), pp. 300–306 .
   Google Scholar
• Kirkland, T., & Mercer, M. R. (1987). A topological search algorithm for ATPG. In Proceedings of the 24th Conference on Design Automation (DAC) Florida, USA, pp. 502–508.
   Google Scholar
• Lu, F., Wang, L.-C., Cheng, K.-T., & Huang, R.-C.-Y. (2003b). A circuit SAT solver with signal correlation guided learning. In Proceedings of Design, Automation and Test in Europe (DATE), pp. 10892–10897.
   Google Scholar
• Lu, F., Wang, L.-C., Cheng, K.-T.-T., Moondanos, J., & Hanna, Z. (2003a). A signal correlation guided ATPG solver and its applications for solving difficult industrial cases. In Proceedings of the 40th Conference on Design automation (DAC), Anaheim CA USA, pp. 436–441.
   Google Scholar
• Marques-Silva, J. (2008). Practical applications of Boolean satisfiability. In 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. The Journal of Artificial Intelligence Research, 51, 377–411. https://doi.org/10.1613/jair.4503
   Web of Science ®Google Scholar
• Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient SAT solver. In 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). Springer.
   Google Scholar
• Reiter, R. (1987). A theory of diagnosis from first principles. Artificial Intelligence, 32(1), 57–95. https://doi.org/10.1016/0004-3702(87)90062-2
   Web of Science ®Google Scholar
• Sabharwal, A., Beame, P., & Kautz, H. (2004). Using problem structure for efficient clause learning. In E. Giunchiglia & A. Tacchella (Eds.), Theory and applications of satisfiability testing (pp. 242–256). Springer.
   Google Scholar
• Siddiqi, S. (2020). An extensible circuit-based SAT solver. Journal of Experimental & Theoretical Artificial Intelligence, 32(5), 751–768. https://doi.org/10.1080/0952813X.2019.1672798
   Web of Science ®Google Scholar
• Siddiqi, S., & Huang, J. (2007). Hierarchical diagnosis of multiple faults. In 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., & Huang, J. (2011). Sequential diagnosis by abstraction. Journal of Artificial Intelligence Research (JAIR), 41, 329–365.
   Web of Science ®Google Scholar
• Smith, A., Veneris, A., & Viglas, A. (2004). Design diagnosis using Boolean satisfiability. In Proceedings of the Ninth Asia and South Pacific Design Automation Conference (ASP-DAC), Pacifico Yokohama, Yokohama, Japan, pp. 218–223.
   Google Scholar
• Thiffault, C., Bacchus, F., & Walsh, T. (2004). Solving non-clausal formulas with DPLL search. In M. Wallace (Ed.), Principles and practice of constraint programming (CP) (pp. 663–678). Springer.
   Google Scholar
• Tseitin, G. S. (1983). On the complexity of derivation in propositional calculus. In J. H. Siekmann & G. Wrightson (Eds.), Automation of reasoning: 2: Classical papers on computational logic 1967–1970 (pp. 466–483). Springer.
   Google Scholar
• Zhang, L., Madigan, C. F., Moskewicz, M. H., & Malik, S. (2001). Efficient conflict driven learning in a Boolean satisfiability solver. In Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design (ICCAD), pp. 279–285, Piscataway, NJ, USA. IEEE Press.
   Google Scholar