中文版 | English
CSpace
An efficient method to transform a sat problem to a mixed integer linear programming problem
Guo, Wenxia1; Wang, Jin2; He, Majun1; Ren, Xiaoqin1; Wang, Qingxian1; Tian, Wenhong1
2018
摘要There exists a method to reduce a 3-SAT (Satifiability) problem to a Subset Sum Problem (SSP) in the literature, however, it can only be applied to small or medium size problems. Our study is to find an efficient method to transform general SAT problems to binary integer linear programming (BILP) problems in larger size. Observing the feature of variable-clauses constraints in SAT, we apply linear inequality model (LIM) to the problem and propose a method called LIMSAT which is based on the reduction from 3SAT to Sub-set Sum problem (SSP). Being different from the classical one, the new method treats each bit as an element in the matrix of SSP, sets matrix as A without those slack variables, sets b as the target value and x as the binary solution. Therefore, we build the model as \mathbf{xA}\leq \mathbf{b}. The experimental results show that the new method works efficiently for very large size problems with thousands of variables and clauses and has comparable performance against the best solver tested by one of the hardest SAT 2016 competition benchmarks. © 2018 IEEE.
语种英语
DOI10.1109/CompComm.2018.8780844
会议(录)名称4th IEEE International Conference on Computer and Communications, ICCC 2018
页码1992-1996
收录类别EI
会议地点Chengdu, China
会议日期December 7, 2018 - December 10, 2018