We propose a new approach to SAT solving which solves SAT problems in vector spaces as a cost minimization problem of a non-negative differentiable cost function J^sat. In our approach, a solution, i.e., satisfying assignment, for a SAT problem in n variables is represented by a binary vector u in {0,1}^n that makes J^sat(u) zero. We search for such u in a vector space R^n by cost minimization, i.e., starting from an initial u_0 and minimizing J to zero while iteratively updating u by Newton's method. We implemented our approach as a matrix-based differential SAT solver MatSat. Although existing main-stream SAT solvers decide each bit of a solution assignment one by one, be they of conflict driven clause learning (CDCL) type or of stochastic local search (SLS) type, MatSat fundamentally differs from them in that it continuously approach a solution in a vector space. We conducted an experiment to measure the scalability of MatSat with random 3-SAT problems in which MatSat could find a solution up to n=10^5 variables. We also compared MatSat with four state-of-the-art SAT solvers including winners of SAT competition 2018 and SAT Race 2019 in terms of time for finding a solution, using a random benchmark set from SAT 2018 competition and an artificial random 3-SAT instance set. The result shows that MatSat comes in second in both test sets and outperforms all the CDCL type solvers.
翻译:我们提出了一个解决沙特卫星的新方法,解决矢量空间中的沙特卫星问题,作为非负负式不同成本函数J ⁇ sat的成本最小化问题。在我们的方法中,一个解决方案,即满足分配,因为n变量中的沙特卫星问题由{0,1 ⁇ n的二进制矢量u 表示,使J ⁇ sat(u)为零。我们在矢量空间R ⁇ 中寻找这种u,费用最小化,即从最初的u_0开始,将J最小化为零,同时通过牛顿的方法反复更新。我们在方法中,将我们的方法作为基于矩阵的差异SAT解答器 MatSat 。尽管现有的正流SAT解答器通过一个分数来决定解决方案的每一个部分,不管是由冲突驱动的条款学习(CDCL)类型还是由本地随机搜索(SLIS)类型。MatSat在矢量空间中持续接近一个解决方案。我们进行了一个实验,用随机的3-SAT解算方法测量MatSat 3-SAT的可标度,在马萨萨德4级测试中,我们也可以找到一个标的Risal-Sat roal roal 。