The Community for Technology Leaders
Green Image
Issue No. 03 - June (1994 vol. 6)
ISSN: 1041-4347
pp: 361-381
<p>The satisfiability (SAT) problem is a fundamental problem in mathematical logic, inference, automated reasoning, VLSI engineering, and computing theory. Following CNF and DNF local search methods, we introduce the Universal SAT problem model, UniSAT, which transforms the discrete SAT problem on Boolean space {0, 1}/sup m/ into an unconstrained global optimization problem on real space E/sup m/. A direct correspondence between the solution of the SAT problem and the global minimum point of the UniSAT objective function is established. Many existing global optimization algorithms can be used to solve the UniSAT problems. Combined with backtracking/resolution procedures, a global optimization algorithm is able to verify satisfiability as well as unsatisfiability. This approach achieves significant performance improvements for certain classes of conjunctive normal form (CNF) formulas. It offers a complementary approach to the existing SAT algorithms.</p>
search problems; optimisation; formal logic; inference mechanisms; global optimization algorithms; satisfiability problem; SAT problem; mathematical logic; inference; automated reasoning; VLSI engineering; computing theory; CNF; DNF local search methods; Universal SAT problem model; UniSAT; discrete SAT problem; Boolean space; unconstrained global optimization problem; real space; direct correspondence; global minimum point; backtracking/resolution procedures; conjunctive normal form
J. Gu, "Global Optimization for Satisfiability (SAT) Problem", IEEE Transactions on Knowledge & Data Engineering, vol. 6, no. , pp. 361-381, June 1994, doi:10.1109/69.334864
98 ms
(Ver )