A Fast Approximation Algorithm for MIN-ONE SAT

In this paper, we propose a novel approximation algorithm (RelaxSAT) for MIN-ONE SAT. RelaxSAT generates a set of constraints from the objective function to guide the search. The constraints are gradually relaxed to eliminate the conflicts with the original Boolean SAT formula until a solution is found. The experiments demonstrate that RelaxSAT is able to handle very large instances which cannot be solved by existing MIN-ONE algorithms; furthermore, very tight bounds on the solution were obtained with one to two orders of magnitude speedup.

• Type: Conference
• Year: 2008
• Where: DATE
• Authors: Lei Fang, Michael S. Hsiao
• Keywords: DATE 2008, Hardware, MIN-ONE SAT, Objective Function, Original Boolean Sat