Eliminating Redundant Clauses in SAT Instances

1. Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI’92), pp. 440–446 (1992)

   Google Scholar 

2. Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Communications of the ACM 5(7), 394–397 (1962)

   Article  MATH  MathSciNet  Google Scholar 

3. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC’01), pp. 530–535 (2001)

   Google Scholar 

4. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

   Google Scholar 

5. Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI’01), pp. 248–253 (2001)

   Google Scholar 

6. Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI’03), pp. 1173–1178 (2003)

   Google Scholar 

7. Liberatore, P.: The complexity of checking redundancy of CNF propositional formulae. In: Proceedings of the 15th European Conference on Artificial Intelligence (ECAI’02), pp. 262–266 (2002)

   Google Scholar 

8. Grégoire, É., Ostrowski, R., Mazure, B., Saïs, L.: Automatic extraction of functional dependencies. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 122–132. Springer, Heidelberg (2005)

   Google Scholar 

9. Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151–158. Association for Computing Machinery, New York (1971)

   Chapter  Google Scholar 

10. Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1, 146–160 (1972)

    Article  MATH  MathSciNet  Google Scholar 

11. Even, S., Itai, A., Shamir, A.: On the complexity of timetable and multicommodity flow problems. SIAM J. Comput. 5, 691–703 (1976)

    Article  MATH  MathSciNet  Google Scholar 

12. Dowling, W.H., Gallier, J.H.: Linear-time algorithms for testing satisfiability of propositional horn formulae. Journal of Logic Programming 1(3), 267–284 (1984)

    Article  MathSciNet  Google Scholar 

13. Wei, W., Selman, B.: Accelerating random walks. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 216–232. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

14. Kautz, H.A., Ruan, Y., Achlioptas, D., Gomes, C.P., Selman, B., Stickel, M.E.: Balance and filtering in structured satisfiable problems. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI’01), pp. 351–358 (2001)

    Google Scholar 

15. Dubois, O., André, P., Boufkhad, Y., Carlier, Y.: SAT vs. UNSAT. In: Second DIMACS implementation challenge: cliques, coloring and satisfiability. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 415–436. American Mathematical Society, New York (1996)

    Google Scholar 

16. Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI’97), pp. 366–371 (1997)

    Google Scholar 

17. Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)

    Google Scholar 

18. Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276–291. Springer, Heidelberg (2005)

    Google Scholar 

19. Crawford, J.: A polynomial-time preprocessor (”compact”) (1996), http://www.cirl.uoregon.edu/crawford/

20. Zhang, W.: Configuration landscape analysis and backbone guided local search: Part i: Satisfiability and maximum satisfiability. Artificial Intelligence 158(1), 1–26 (2004)

    Article  MATH  MathSciNet  Google Scholar 

21. Le Berre, D.: Exploiting the real power of unit propagation lookahead. In: Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT’01), Boston University, Massachusetts, USA (2001)

    Google Scholar 

22. Ostrowski, R., Mazure, B., Saïs, L., Grégoire, É.: Eliminating redundancies in SAT search trees. In: Proceedings of the 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI’2003), Sacramento, pp. 100–104 (2003)

    Google Scholar 

23. Darras, S., Dequen, G., Devendeville, L., Mazure, B., Ostrowski, R., Saïs, L.: Using boolean constraint propagation for sub-clauses deduction. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 757–761. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

24. Boufkhad, Y., Roussel, O.: Redundancy in random SAT formulas. In: Proceedings of the 17th National Conference on Artificial Intelligence (AAAI’00), pp. 273–278 (2000)

    Google Scholar 

25. Liberatore, P.: Redundancy in logic i: CNF propositional formulae. Artificial Intelligence 163(2), 203–232 (2005)

    Article  MATH  MathSciNet  Google Scholar 

26. Selman, B., Kautz, H.A.: Knowledge compilation using horn approximations. In: Proceedings of the 9th National Conference on Artificial Intelligence (AAAI’91), pp. 904–909 (1991)

    Google Scholar 

27. del Val, A.: Tractable databases: How to make propositional unit resolution complete through compilation. In: Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR’94), pp. 551–561 (1994)

    Google Scholar 

28. Marquis, P.: Knowledge compilation using theory prime implicates. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI’95), Montréal, Canada, pp. 837–843 (1995)

    Google Scholar 

29. Mazure, B., Marquis, P.: Theory reasoning within implicant cover compilations. In: Proceedings of the ECAI’96 Workshop on Advances in Propositional Deduction, Budapest, Hungary, pp. 65–69 (1996)

    Google Scholar 

30. Grégoire, É., Mazure, B., Piette, C.: Extracting MUSes. In: Proceedings of the 17th European Conference on Artificial Intelligence (ECAI’06), Trento, Italy, pp. 387–391 (2006)

    Google Scholar 

Download references