{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T15:04:50Z","timestamp":1746371090011,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540723967"},{"type":"electronic","value":"9783540723974"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-72397-4_6","type":"book-chapter","created":{"date-parts":[[2007,6,22]],"date-time":"2007-06-22T19:56:32Z","timestamp":1182542192000},"page":"71-83","source":"Crossref","is-referenced-by-count":11,"title":["Eliminating Redundant Clauses in SAT Instances"],"prefix":"10.1007","author":[{"given":"Olivier","family":"Fourdrinoy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9ric","family":"Gr\u00e9goire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Mazure","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lakhdar","family":"Sa\u00efs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"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\u201992), pp. 440\u2013446 (1992)"},{"issue":"7","key":"6_CR2","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"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\u201901), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"6_CR5","unstructured":"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\u201901), pp. 248\u2013253 (2001)"},{"key":"6_CR6","unstructured":"Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI\u201903), pp. 1173\u20131178 (2003)"},{"key":"6_CR7","unstructured":"Liberatore, P.: The complexity of checking redundancy of CNF propositional formulae. In: Proceedings of the 15th European Conference on Artificial Intelligence (ECAI\u201902), pp. 262\u2013266 (2002)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/11527695_10","volume-title":"Theory and Applications of Satisfiability Testing","author":"\u00c9. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, \u00c9., Ostrowski, R., Mazure, B., Sa\u00efs, L.: Automatic extraction of functional dependencies. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 122\u2013132. Springer, Heidelberg (2005)"},{"key":"6_CR9","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/800157.805047","volume-title":"Proceedings of the 3rd Annual ACM Symposium on Theory of Computing","author":"S.A. Cook","year":"1971","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151\u2013158. Association for Computing Machinery, New York (1971)"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput.\u00a01, 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1137\/0205048","volume":"5","author":"S. Even","year":"1976","unstructured":"Even, S., Itai, A., Shamir, A.: On the complexity of timetable and multicommodity flow problems. SIAM J. Comput.\u00a05, 691\u2013703 (1976)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"6_CR12","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W.H. Dowling","year":"1984","unstructured":"Dowling, W.H., Gallier, J.H.: Linear-time algorithms for testing satisfiability of propositional horn formulae. Journal of Logic Programming\u00a01(3), 267\u2013284 (1984)","journal-title":"Journal of Logic Programming"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-46135-3_15","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"W. Wei","year":"2002","unstructured":"Wei, W., Selman, B.: Accelerating random walks. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 216\u2013232. Springer, Heidelberg (2002)"},{"key":"6_CR14","unstructured":"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\u201901), pp. 351\u2013358 (2001)"},{"key":"6_CR15","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1090\/dimacs\/026\/20","volume-title":"Second DIMACS implementation challenge: cliques, coloring and satisfiability","author":"O. Dubois","year":"1996","unstructured":"Dubois, O., Andr\u00e9, 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.\u00a026, pp. 415\u2013436. American Mathematical Society, New York (1996)"},{"key":"6_CR16","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI\u201997), pp. 366\u2013371 (1997)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/11527695_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Subbarayan","year":"2005","unstructured":"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.\u00a03542, pp. 276\u2013291. Springer, Heidelberg (2005)"},{"key":"6_CR19","unstructured":"Crawford, J.: A polynomial-time preprocessor (\u201dcompact\u201d) (1996), http:\/\/www.cirl.uoregon.edu\/crawford\/"},{"issue":"1","key":"6_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2004.04.001","volume":"158","author":"W. Zhang","year":"2004","unstructured":"Zhang, W.: Configuration landscape analysis and backbone guided local search: Part i: Satisfiability and maximum satisfiability. Artificial Intelligence\u00a0158(1), 1\u201326 (2004)","journal-title":"Artificial Intelligence"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Le Berre, D.: Exploiting the real power of unit propagation lookahead. In: Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT\u201901), Boston University, Massachusetts, USA (2001)","DOI":"10.1016\/S1571-0653(04)00314-2"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Ostrowski, R., Mazure, B., Sa\u00efs, L., Gr\u00e9goire, \u00c9.: Eliminating redundancies in SAT search trees. In: Proceedings of the 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI\u20192003), Sacramento, pp. 100\u2013104 (2003)","DOI":"10.1109\/TAI.2003.1250176"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/11564751_59","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"S. Darras","year":"2005","unstructured":"Darras, S., Dequen, G., Devendeville, L., Mazure, B., Ostrowski, R., Sa\u00efs, L.: Using boolean constraint propagation for sub-clauses deduction. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 757\u2013761. Springer, Heidelberg (2005)"},{"key":"6_CR24","unstructured":"Boufkhad, Y., Roussel, O.: Redundancy in random SAT formulas. In: Proceedings of the 17th National Conference on Artificial Intelligence (AAAI\u201900), pp. 273\u2013278 (2000)"},{"issue":"2","key":"6_CR25","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.artint.2004.11.002","volume":"163","author":"P. Liberatore","year":"2005","unstructured":"Liberatore, P.: Redundancy in logic i: CNF propositional formulae. Artificial Intelligence\u00a0163(2), 203\u2013232 (2005)","journal-title":"Artificial Intelligence"},{"key":"6_CR26","unstructured":"Selman, B., Kautz, H.A.: Knowledge compilation using horn approximations. In: Proceedings of the 9th National Conference on Artificial Intelligence (AAAI\u201991), pp. 904\u2013909 (1991)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"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\u201994), pp. 551\u2013561 (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50146-9"},{"key":"6_CR28","unstructured":"Marquis, P.: Knowledge compilation using theory prime implicates. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI\u201995), Montr\u00e9al, Canada, pp. 837\u2013843 (1995)"},{"key":"6_CR29","unstructured":"Mazure, B., Marquis, P.: Theory reasoning within implicant cover compilations. In: Proceedings of the ECAI\u201996 Workshop on Advances in Propositional Deduction, Budapest, Hungary, pp. 65\u201369 (1996)"},{"key":"6_CR30","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: Extracting MUSes. In: Proceedings of the 17th European Conference on Artificial Intelligence (ECAI\u201906), Trento, Italy, pp. 387\u2013391 (2006)"}],"container-title":["Lecture Notes in Computer Science","Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72397-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T13:38:34Z","timestamp":1737121114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72397-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540723967","9783540723974"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72397-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}