An Incremental Branch-and-Bound Method for the Satisfiability Problem

References

• BAHIA Partie I de l'étude comparative des trois formalismes en calcul propositionnel, Projet BAHIA. PRC IA 4th national days (1993) (Marseille, France) Google Scholar
• Partie II de l'étude comparative des trois formalismes en calcul propositionnel, Projet BAHIA. PRC IA 5th national days (1995) (Nancy, France) . BAHIA Google Scholar
• Benhamou B. , Saïs L. Theoretical Study of Symetries and Applications. Proceedings CADE (1992) Google Scholar
• Bennaceur H. , Plateau G. FAST: une méthode de résolution du probléme linéaire de satisfaction de contraintes. Technique et science informatiques (1992) 11 3 33 57 Google Scholar
• Bennaceur H. , Plateau G. An Exact Algorithm for the Constraint Satisfaction Problem: Application to Logical Inference. Information Processing Letters (1993) 48 151 158 Crossref, Google Scholar
• Bennaceur H. , Plateau G. An Exact Method for the Linear Constraint Satisfaction Problem: Application to the Satisfiability Problem. Investigacion Operativa (1994) 4 3 247 264 Google Scholar
• Bennaceur H. , Plateau G. Constraint Satisfaction and Combinatorial Optimization. JORBEL (1995) 35 4 41 59 Google Scholar
• Blair C. E. , Jeroslow R. G. , Lowe J. K. Some Results and Experiments in Programming Techniques for Propositional Logic. Comput. Oper. Res. (1986) 13 5 633 645 Crossref, Google Scholar
• Boros E. , Crama Y. , Hammer P. L. Polynomialtime Inference of all Valid Implications for Horn and Related Formulae. Annnals of Mathematics and Artificial Intelligence (1990) 1 21 32 Crossref, Google Scholar
• Boros E. , Crama Y. , Hammer P. L. , Saks M. A Complexity Index for Satisfiability Problems. (1992) 9 92 . RUTCOR Research report Google Scholar
• Boros E. , Hammer P. L. A Generalization of the Pure Literal Rule for Satisfiability Problems. (1992) 20 92 . RUTCOR Research report Google Scholar
• Boros E. , Hammer P. L. , Sun X. Recognition of Q-Horn Formulae in Linear Time. (1992) 19 92 . RUTCOR Research Report Google Scholar
• Cook S. A. The Complexity of Theorem Proving Procedures. Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing (1971) (ACM, New York) 151 158 Crossref, Google Scholar
• Cot N. , Bellaiche C. Une nouvelle approche du probléme SAT. Comptes Rendus de l'Académie des Sciences de Paris (1991) 313 1 801 804 Google Scholar
• Cot N. , Bellaiche C. Une famille d'algorithmes polynomiaux pour la résolution de classes d'instances du probléme SAT. Comptes Rendus de l'Académie des Sciences de Paris (1991) 313 1 879 882 Google Scholar
• Davis M. , Putnam H. A Computing Procedure for Quantification Theory. Journal of the ACM (1960) 7 201 215 Crossref, Google Scholar
• Gallo G. , Petrolani D. A New Algorithm for the Propositional Satisfiability Problem. (1992) . Research report, Dipartimento di Informatica, University of Pisa, Italy Google Scholar
• Gallo G. , Urbani G. Algorithms for Testing the Satisfiability of Propositional Formulae. Journal of Logic Programming (1989) 7 45 61 Crossref, Google Scholar
• Glover F. Tabu Search-Part I. ORSA Journal on Computing 1 190 206 Link, Google Scholar
• Glover F. Tabu search-part II. ORSA Journal on Computing (1990) 2 4 32 Link, Google Scholar
• Guignard M. , Spielberg K. Some General Principles for Practical Mixed 0–1 Programming: Logical Inequalities, Disaggregation and Lifting. (1993) . APMOD93 Symposium, Budapest Google Scholar
• Harche F. , Hooker J. N. , Thompson G. L. A Computational Study of Satisfiability Algorithms for Propositional Logic,management Science Research Report MSRR-567. (1991) (Carnegie Mellon University) Google Scholar
• Hertz A. , de Werra D. The Tabu Search Metaheuristic: How we used it. Annals of Mathematics and Artificial Intelligence (1990) 1 111 121 Crossref, Google Scholar
• Hooker J. N. Resolution vs. Cutting Plane Solution of Inference Problems: Some Computational Experience. Operations Research Letters (1988) 7 1 7 Crossref, Google Scholar
• Hooker J. N. Generalized Resolution and Cutting Planes. Annals of Operations Research (1988) 12 217 239 Crossref, Google Scholar
• Hooker J. N. A Quantitative Approach to Logical Inference. Decision Support Systems (1988) 4 45 69 Crossref, Google Scholar
• Hooker J. N. Solving the Incremental Satisfiability Problem. Journal of Logic Programming (1993) 15 177 186 Crossref, Google Scholar
• Hooker J. N. , Fedjki C. Branch-and-Cut Solution of Inference Problems in Propositional Logic. Annals of Mathematics and Artificial Intelligence 1 123 139 Crossref, Google Scholar
• Hooker J. N. , Yan H. , Saraswat V. , Van Hentenryck P. Logic Circuit Verification by Benders Decomposition. Principles and Practice of Constraint Programming (1995) (MIT Press) 267 288 . The Newport Papers Google Scholar
• Hubbe P. , Freuder H. An Efficient Cross-Product Representation of the Constraint Satisfaction Problem Search Space. Proceedings of AAAI (1992) 421 427 Google Scholar
• Jaumard B. , Ow P. S. , Simeone B. A Selected Artificial Intelligence Bibliography for Operations Researchers. Annals of Operations Research (1988) 12 1 50 Crossref, Google Scholar
• Jaumard B. , Stan M. , Desrosiers J. Tabu Search and a Quadratic Relaxation for the Satisfiability Problem. Les cahiers du GERAD (1993) Google Scholar
• Jeroslow R. G. , Wang J. Solving Propositional Satisfiability Problems. Annals of Mathematics and Artificial Intelligence (1990) 1 167 187 Crossref, Google Scholar
• Kamath A. P. , Karmarkar N. K. , Ramakrishnan K. G. , Resende M. G. C. Computational Experience With an Interior Point Algorithm on the Satisfiability Problem. Annals of Operations Research (1990) 25 43 58 Crossref, Google Scholar
• Kamath A. P. , Karmarkar N. K. , Ramakrishnan K. G. , Resende M. G. C. A Continuous Approach to Inductive Inference. Mathematical Programming (1992) 57 215 238 Crossref, Google Scholar
• Koutsoupias E. , Papadimitriou C. H. On the Greedy Algorithm for Satisfiability. Information Processing Letters (1992) 43 53 55 Crossref, Google Scholar
• Loveland D. W. Automated Theorem Proving: A Logical Basis (1978) (North Holland, Amsterdam) Google Scholar
• Williams H. P. Linear and Integer Programming Applied to the Propositional Calculus. International Journal of Systems Research and Information Science (1987) 2 81 100 Google Scholar
• Williams H. P. Computational Logic and Integer Programming: Connections Between the Methods of Logic. (1991) . AI and OR, University of Southampton Research report Google Scholar
• Zimmerman H. J. , Morfroglio A. Linear Programs for Constraint Satisfaction Problems. European Journal of Operational Research (1997) 97 1 105 123 Crossref, Google Scholar