AN EXACT ALGORITHM FOR THE CONSTRAINT SATISFACTION PROBLEM - APPLICATION TO LOGICAL INFERENCE

The inference problem in propositional logic realizes a strong connect ion between Artificial Intelligence and Operational Research. It is no w well-known that this problem can be formulated as a constraint satis faction problem (CSP), whose system has a generalized covering type (w e recall that a CSP consists in proving the emptiness of a domain defi ned by a set of diophantine constraints, or the existence of a solutio n). We propose a new method - denoted by FAST (Fast Algorithm for the constraint Satisfaction Test problems) - which allows an efficient sol ution of the CSP instances for logical inference. Computational result s are reported for 3-SAT, 4-SAT and system expert type instances.