KMS Chongqing Institute of Green and Intelligent Technology, CAS
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. |
语种 | 英语 |
DOI | 10.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 |