Recently many researchers are devoted into seeking for new ideas as well as developing more efficient satisfiability (SAT) solvers. In this paper, we propose a new scheme for solving SAT. According to the scheme, the original SAT problem is first translated into a Traveling Sales Problem (TSP), which will then be solved by Ant Colony Optimization (ACO). The reason we adopt the idea is ACO is suitable for solving TSPs whose weights (or distances) between cities are changed dynamically. We give a detailed description of the SAT solver by ACO, namely ACSAT. Experimental Results show that ACSAT behaves fairly stably and robustly in handling instances with up to 10k variables.
展开▼
