Relaxations of the Satisfiability Problem Using Semidefinite Programming

We derive a semidefinite relaxation of the satisfiability (SAT) problem and discuss its strength. We give both the primal and dual formulation of the relaxation. The primal formulation is an eigenvalue optimization problem, while the dual formulation is a semidefinite feasibility problem. We show that using the relaxation, a proof of the unsatisfiability of the notorious pigeonhole and mutilated chessboard problems can be computed in polynomial time. As a byproduct we find a new `sandwich" theorem that is similar to the sandwich theorem for Lovász' -function. Furthermore, the semidefinite relaxation gives a certificate of (un)satisfiability for 2SAT problems in polynomial time. By adding an objective function to the dual formulation, a specific class of polynomially solvable 3SAT instances can be identified. We conclude with discussing how the relaxation can be used to solve more general SAT problems and with some empirical observations.     

求解SAT问题的线性半定规划算法

将线性半定规划应用到SAT问题的求解过程中。首先将SAT实例转化为整数规划问题,然后松弛为线性规划模型,最后再转化为一般的线性半定规划模型去求解。用SDPA-M软件求解线性半定规划问题后,规定了如何根据目标函数值去判定SAT实例和当CNF公式可满足时如何根据最优指派的概率X^＊i（i=1,…,n）去进行变元赋值,以期求得该公式的可满足指派。上述算法不仅可以判定SAT问题,而且对于符合算法规定可满足的CNF公式皆可给出一个可满足指派。求解SAT问题的线性半定规划算法在文章中被描述并被给予相应算例。     

基于半定规划的量子状态最优无错区分

对于一般的量子状态最优无错区分问题.很难得到最优量子测量的解析形式.因此,有必要寻求有效实用的数值方法.基于半定规划理论,证明了无错状态区分的最优量子测肇的设计问题可以转化为标准的半定规划问题,以及能直接应用半定规划的最优性条件,从而更简明地推导了.一组无错状态区分的最优性条件;通过求解标准的半定规划问题.可在多项式时间内直接得到最优量子测量的数值解以及成功区分状态的最大概率值.实例仿真表明,方法易于计算机实现,能有效地设计出无错状态区分的最优量子测量算子.     

On Semidefinite Programming Relaxations of (2+p)-SAT

Recently, de Klerk, van Maaren and Warners [10] investigated a relaxation of 3-SAT via semidefinite programming. Thus a 3-SAT formula is relaxed to a semidefinite feasibility problem. If the feasibility problem is infeasible then a certificate of unsatisfiability of the formula is obtained. The authors proved that this approach is exact for several polynomially solvable classes of logical formulae, including 2-SAT, pigeonhole formulae and mutilated chessboard formulae. In this paper we further explore this approach, and investigate the strength of the relaxation on (2+p)-SAT formulae, i.e., formulae with a fraction p of 3-clauses and a fraction (1–p) of 2-clauses. In the first instance, we provide an empirical computational evaluation of our approach. Secondly, we establish approximation guarantees of randomized and deterministic rounding schemes when the semidefinite feasibility problem is feasible, and also present computational results for the rounding schemes. In particular, we do a numerical and theoretical comparison of this relaxation and the stronger relaxation by Karloff and Zwick [15].     

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints

Polynomial constraint solving plays a prominent role in several areas of hardware and software analysis and verification, e.g., termination proving, program invariant generation and hybrid system verification, to name a few. In this paper we propose a new method for solving non-linear constraints based on encoding the problem into an SMT problem considering only linear arithmetic. Unlike other existing methods, our method focuses on proving satisfiability of the constraints rather than on proving unsatisfiability, which is more relevant in several applications as we illustrate with several examples. Nevertheless, we also present new techniques based on the analysis of unsatisfiable cores that allow one to efficiently prove unsatisfiability too for a broad class of problems. The power of our approach is demonstrated by means of extensive experiments comparing our prototype with state-of-the-art tools on benchmarks taken both from the academic and the industrial world.     

Infra-chromatic bound for exact maximum clique search

Many efficient exact branch and bound maximum clique solvers use approximate coloring to compute an upper bound on the clique number for every subproblem. This technique reasonably promises tight bounds on average, but never tighter than the chromatic number of the graph.Li and Quan, 2010, AAAI Conference, p. 128–133 describe a way to compute even tighter bounds by reducing each colored subproblem to maximum satisfiability problem (MaxSAT). Moreover they show empirically that the new bounds obtained may be lower than the chromatic number.Based on this idea this paper shows an efficient way to compute related “infra-chromatic” upper bounds without an explicit MaxSAT encoding. The reported results show some of the best times for a stand-alone computer over a number of instances from standard benchmarks.     

Quadratic approximate dynamic programming for input‐affine systems

We consider the use of quadratic approximate value functions for stochastic control problems with input‐affine dynamics and convex stage cost and constraints. Evaluating the approximate dynamic programming policy in such cases requires the solution of an explicit convex optimization problem, such as a quadratic program, which can be carried out efficiently. We describe a simple and general method for approximate value iteration that also relies on our ability to solve convex optimization problems, in this case, typically a semidefinite program. Although we have no theoretical guarantee on the performance attained using our method, we observe that very good performance can be obtained in practice.Copyright © 2012 John Wiley & Sons, Ltd.     

Solving propositional satisfiability problems

We describe an algorithm for the satisfiability problem of prepositional logic, which is significantly more efficient for this problem than is a general mixed-integer programming code. Our algorithm is a list processor using a tree-search method, and is based on Loveland's form of the algorithm of Davis and Putnam.Deceased. Research partially supported by a research grant from the National Science Foundation (DMS-8513970).     

Tradeoffs in the empirical evaluation of competing algorithm designs

We propose an empirical analysis approach for characterizing tradeoffs between different methods for comparing a set of competing algorithm designs. Our approach can provide insight into performance variation both across candidate algorithms and across instances. It can also identify the best tradeoff between evaluating a larger number of candidate algorithm designs, performing these evaluations on a larger number of problem instances, and allocating more time to each algorithm run. We applied our approach to a study of the rich algorithm design spaces offered by three highly-parameterized, state-of-the-art algorithms for satisfiability and mixed integer programming, considering six different distributions of problem instances. We demonstrate that the resulting algorithm design scenarios differ in many ways, with important consequences for both automatic and manual algorithm design. We expect that both our methods and our findings will lead to tangible improvements in algorithm design methods.     

Cell formation in group technology using constraint programming and Boolean satisfiability

Cell formation consists in organizing a plant as a set of cells, each of them containing machines that process similar types or families of parts. The idea is to minimize the part flow among cells in order to reduce costs and increase productivity. The literature presents different approaches devoted to solve this problem, which are mainly based on mathematical programming and on evolutionary computing. Mathematical programming can guarantee a global optimal solution, however at a higher computational cost than an evolutionary algorithm, which can assure a good enough optimum in a fixed amount of time. In this paper, we model and solve this problem by using state-of-the-art constraint programming (CP) techniques and Boolean satisfiability (SAT) technology. We present different experimental results that demonstrate the efficiency of the proposed optimization models. Indeed, CP and SAT implementations are able to reach the global optima in all tested instances and in competitive runtime.     

Semidefinite spectral clustering

Multi-way partitioning of an undirected weighted graph where pairwise similarities are assigned as edge weights, provides an important tool for data clustering, but is an NP-hard problem. Spectral relaxation is a popular way of relaxation, leading to spectral clustering where the clustering is performed by the eigen-decomposition of the (normalized) graph Laplacian. On the other hand, semidefinite relaxation, is an alternative way of relaxing a combinatorial optimization, leading to a convex optimization. In this paper we employ a semidefinite programming (SDP) approach to the graph equipartitioning for clustering, where sufficient conditions for strong duality hold. The method is referred to as semidefinite spectral clustering, where the clustering is based on the eigen-decomposition of the optimal feasible matrix computed by SDP. Numerical experiments with several data sets, demonstrate the useful behavior of our semidefinite spectral clustering, compared to existing spectral clustering methods.     

Elimination of Boolean variables for probabilistic coherence

 In this paper we deal with the computational complexity problem of checking the coherence of a partial probability assessment (called CPA). The CPA problem, like its analogous PSAT, is NP-complete so we look for an heuristic procedure to make tractable reasonable instances of the problem. Starting from the characteristic feature of de Finetti's approach (i.e. the explicit distinction between the probabilistic assessment and the logical relations among the sentences) we introduce several rules for a sequential “elimination” of Boolean variables from the domain of the assessment. The procedure resembles the well-known Davis-Putnam rules for the satisfiability, however we have, as a drawback, the introduction of constraints (among real variables) whose satisfiability must be checked. In simple examples we test the efficiency of the procedure respect to the “traditional” approach of solving a linear system with a huge coefficient matrix built from the atoms generated by the domain of the assessment.     

基于抗原中介三链DNA结构的0-1整数规划

利用同源的存在抗原蛋白质的脱氧核苷酸定位于双链DNA中很容易形成三螺旋结构的DNA链,可以利用这种独特的结构来研究一些可能的或可行的的计算模型。尝试了用三螺旋结构的DNA链来解决简单的0-1整数规划问题。而对于整数规划和可满足问题都可以转化为0-1整数规划来解决,从而都可以利用三链DNA计算模型得以解决。     

可满足实例的归结复杂度

GRB模型是一种随机约束满足问题模型,此模型具有精确的可满足相变现象。针对实验中出现的GRB模型在相变区域产生的可满足实例都是难解的现象,利用子句宽度和归结复杂度的关系证明了GRB模型在相变点附近产生的可满足实例对于树型归结证明具有指数下界。因此从理论上证明了在相变区域产生的可满足实例对基于归结的算法是难解的。     

On the modelling and solving of the truss design problem with global stability constraints

The goal of this paper is to find a computationally tractable formulation of the optimum truss design problem involving a constraint on the global stability of the structure. The stability constraint is based on the linear buckling phenomenon. We formulate the problem as a nonconvex semidefinite programming problem and briefly discuss an interior point technique for the numerical solution of this problem. We further discuss relation to other models. The paper is concluded by a series of numerical examples.     

一类布尔方程组的可满足性阈值研究*

以一类布尔方程组形式的NP问题可满足性阈值估计为研究目的,通过将高斯消去算法与摘叶算法相结合的方法给出了一种求解该问题的完全算法,并通过不同参数条件下对大量随机实例进行数值实验得到了原问题可满足性阈值的算法估计值。所得研究结果不仅首次给出了该问题的可满足性阈值估计,而且可以作为相关启发式完全算法的设计依据。     

谓词模态逻辑到对应物理论的翻译

对应物理论(counterpart theory)是一阶逻辑的一种理论.Lewis利用谓词模态逻辑到对应物理论的翻译来研究谓词模态逻辑的性质,但是Lewis的翻译存在把不可满足的公式翻译为可满足公式的情况针对这个问题,提出了一种扩展语义的谓词模态逻辑,建立了扩展语义后谓词模态逻辑模型与对应物理论模型的一一对应关系,并在此基础上建立了谓词模态逻辑到对应物理论的语义忠实语义满翻译(faithful and full translation),其可确保将谓词模态逻辑的可满足公式和不可满足公式分别翻译为对应物理论的可满足公式和不可满足公式.由对应物理论是可靠的、完备的一阶逻辑的理论且语义忠实语义满翻译保持可靠性和完备性,进一步证明了扩展语义的谓词模态逻辑也是可靠和完备的.     

A note on assumptions about Skolem functions

Skolemization is not an equivalence preserving transformation. For the purposes of refutational theorem proving it is sufficient that skolemization preserves satisfiability and unsatisfiability. Therefore there is sometimes some freedom in interpreting Skolem functions in a particular way. We show that in certain cases it is possible to exploit this freedom for simplifying formulae considerably. Examples for cases where this occurs systematically are the relational translation from modal logics to predicate logic and the relativization of first-order logics with sorts.     

Hermite matrix in Lagrange basis for scaling static output feedback polynomial matrix inequalities

Using Hermite's formulation of polynomial stability conditions, static output feedback (SOF) controller design can be formulated as a polynomial matrix inequality (PMI), a (generally nonconvex) nonlinear semidefinite programming problem that can be solved (locally) with PENNON, an implementation of a penalty and augmented Lagrangian method. Typically, Hermite SOF PMI problems are badly scaled and experiments reveal that this has a negative impact on the overall performance of the solver. In this note we recall the algebraic interpretation of Hermite's quadratic form as a particular Bézoutian and we use results on polynomial interpolation to express the Hermite PMI in a Lagrange polynomial basis, as an alternative to the conventional power basis. Numerical experiments on benchmark problem instances show the improvement brought by the approach, in terms of problem scaling, number of iterations and convergence behaviour of PENNON.     

The satisfiability problem in regular CNF-formulas

 In this paper we deal with the propositional satisfiability (SAT) problem for a kind of multiple-valued clausal forms known as regular CNF-formulas and extend some known results from classical logic to this kind of formulas. We present a Davis–Putnam-style satisfiability checking procedure for regular CNF-formulas equipped with suitable data structures and prove its completeness. Then, we describe a series of experiments for regular random 3-SAT instances. We observe that, for the regular 3-SAT problem with this procedure, there exists a threshold of the ratio of clauses to variables such that (i) the most computationally difficult instances tend to be found near the threshold, (ii) there is a sharp transition from satisfiable to unsatisfiable instances at the threshold and (iii) the value of the threshold increases as the number of truth values considered increases. Instances in the hard part provide benchmarks for the evaluation of regular satisfiability solvers.