The Multi-SAT algorithm

Many efficient algorithms have been developed for satisfiability testing. T hey complement rather than exclude each other by being effective for partic ular problem instances. In this research, we give a Multi-SAT algorithm for the SAT problem. The Multi-SAT algorithm integrates several efficient SAT algorithms. It makes use of different algorithmic niches for satisfiability testing. Based on cost-effective cluster computing, Multi-SAT can perform simultaneous satisfiability testing, using several "stones" to shoot one "b ird". The software architecture for Multi-SAT has been designed. A number o f software tools have been developed. This software tool kit can support ef ficient satisfiability testing with uncertain problem structure, facilitati ng multiple tracking of an algorithm structure, and allow a detailed study of the entire problem spectrum. It provides a cost-effective multi-tool kit for practical satisfiability testing. (C) 1999 Elsevier Science B.V. All r ights reserved.