The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing , STOC '71, pp.151-158, 1971. ,
DOI : 10.1145/800157.805047
Using Boolean Constraint Propagation for Sub-clauses Deduction, Proceedings of the Eleventh International Conference on Principles and Practice of Constraint Programming (CP'05), pp.757-761, 2005. ,
DOI : 10.1007/11564751_59
A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962. ,
DOI : 10.1145/368273.368557
Linear-time algorithms for testing the satisfiability of propositional horn formulae, The Journal of Logic Programming, vol.1, issue.3, pp.267-284, 1984. ,
DOI : 10.1016/0743-1066(84)90014-1
Second DIMACS implementation challenge : cliques, coloring and satisfiability, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, chapter SAT vs. UNSAT, pp.415-436, 1996. ,
A backbone-search heuristic for efficient solving of hard 3-SAT formulae, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI'01), pp.248-253, 2001. ,
On the Complexity of Timetable and Multicommodity Flow Problems, SIAM Journal on Computing, vol.5, issue.4, pp.691-703, 1976. ,
DOI : 10.1137/0205048
Effective preprocessing in SAT through variable and clause elimination, Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT'05), pp.61-75, 2005. ,
An extensible SATsolver Extracting MUSes Automatic extraction of functional dependencies, Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT'03) Proceedings of the 17th European Conference on Artificial Intelligence (ECAI'06) Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT'04), pp.502-518, 2003. ,
Exploiting the real power of unit propagation lookahead, Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT'01), 2001. ,
DOI : 10.1016/S1571-0653(04)00314-2
Heuristics based on unit propagation for satisfiability problems, Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), pp.366-371, 1997. ,
The complexity of checking redundancy of CNF propositional formulae [17] P. Liberatore. Redundancy in logic i : CNF propositional formulae, Proceedings of the 15th European Conference on Artificial Intelligence (ECAI'02), pp.262-266203, 2002. ,
Knowledge compilation using theory prime implicates, Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI'95), pp.837-843, 1995. ,
Theory reasoning within implicant cover compilations, Proceedings of the ECAI-96 Workshop on Advances in Propositional Deduction, pp.65-69, 1996. ,
Chaff, Proceedings of the 38th conference on Design automation , DAC '01, pp.530-535, 2001. ,
DOI : 10.1145/378239.379017
Eliminating redundancies in SAT search trees, Proceedings. 15th IEEE International Conference on Tools with Artificial Intelligence, pp.100-104, 2003. ,
DOI : 10.1109/TAI.2003.1250176
Nonincreasing variable elimination resolution for preprocessing SAT instances, Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT'04), pp.276-291, 2004. ,
Knowledge compilation using horn approximations, Proceedings of the Ninth National Conference on Artificial Intelligence (AAAI'91), pp.904-909, 1991. ,
A new method for solving hard satisfiability problems, Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI'92), pp.440-446, 1992. ,
Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972. ,
DOI : 10.1137/0201010
Backdoors to typical case complexity, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI'03), pp.1173-1178, 2003. ,
Configuration landscape analysis and backbone guided local search., Artificial Intelligence, vol.158, issue.1, pp.1-26, 2004. ,
DOI : 10.1016/j.artint.2004.04.001
URL : http://doi.org/10.1016/j.artint.2004.04.001