SOLVING THE SATISFIABILITY PROBLEM USING MESSAGE-PASSING TECHNIQUES
S. J. Pumphrey · 2001
INTRODUCTION The propositional satisfiability (or SAT) problem is one of the oldest and most researched problems in computer science and computational physics. It is one of the major problems in machine vision, and has applications in many fields of artificial intelligence, including natural language parsing, task scheduling, 3D object semantics, and logical reasoning[12]. A technique to rapidly solve SAT problems would revolutionise the field of computational science. However, such an algorithm is thought impossible and the best achievable is likely to be a method which finds a solution most of the time. The objective in a SAT problem is to find an assignment to a set of Boolean 1 variables such that a logic statement about those variables is `satisfied', i.e. true. At first sight this can seem a fairly abstract problem, so consider the following example[13]: You are chief of protocol for the embassy ball. The crown p