The unsatisfiability threshold revisited

The problem of determining the unsatisfiability threshold for random 3-SAT formulas consists in determining the clause to variable ratio that marks the experimentally observed abrupt change from almost surely satisfiable formulas to almost surely unsatisfiable. Up to now, there have been rigorously established increasingly better lower and upper bounds to the actual threshold value. In this paper, we consider the problem of bounding the threshold value from above using methods that, we believe, are of interest on their own right. More specifically, we show how the method of local maximum satisfying truth assignments can be combined with results for the occupancy problem in schemes of random allocation of balls into bins in order to achieve an upper bound for the unsatisfiability threshold less than 4.571. In order to obtain this value, we establish a bound on the q-binomial coefficients (a generalization of the binomial coefficients). No such bound was previously known, despite the extensive literature on q-binomial coefficients. Finally, to prove our result we had to establish certain relations among the conditional probabilities of an event in various probabilistic models for random formulas. It turned out that these relations were considerably harder to prove than the corresponding ones for unconditional probabilities, which were previously known.     

The fluted fragment with transitive relations

The fluted fragment is a fragment of first-order logic (without equality) in which, roughly speaking, the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that this fragment has the finite model property. We consider extensions of the fluted fragment with various numbers of transitive relations, as well as the equality predicate. In the presence of one transitive relation (together with equality), the finite model property is lost; nevertheless, we show that the satisfiability and finite satisfiability problems for this extension remain decidable. We also show that the corresponding problems in the presence of two transitive relations (with equality) or three transitive relations (without equality) are undecidable, even for the two-variable sub-fragment.     

GO-MOCE: Greedy Order Method of Conditional Expectations for Max Sat

In this paper we present and study a new algorithm for the Maximum Satisfiability (Max Sat) problem. The algorithm is based on the Method of Conditional Expectations (MOCE, also known as Johnson’s Algorithm) and applies a greedy variable ordering to MOCE. Thus, we name it Greedy Order MOCE (GO-MOCE). We also suggest a combination of GO-MOCE with CCLS, a state-of-the-art solver. We refer to this combined solver as GO-MOCE-CCLS.We conduct a comprehensive comparative evaluation of GO-MOCE versus MOCE on random instances and on public competition benchmark instances. We show that GO-MOCE reduces the number of unsatisfied clauses by tens of percents, while keeping the runtime almost the same. The worst case time complexity of GO-MOCE is linear. We also show that GO-MOCE-CCLS improves on CCLS consistently by up to about 80%.We study the asymptotic performance of GO-MOCE. To this end, we introduce three measures for evaluating the asymptotic performance of algorithms for Max Sat. We point out to further possible improvements of GO-MOCE, based on an empirical study of the main quantities managed by GO-MOCE during its execution.     

Linear phase transition in random linear constraint satisfaction problems

Our model is a generalized linear programming relaxation of a much studied random K-SAT problem. Specifically, a set of linear constraints on K variables is fixed. From a pool of n variables, K variables are chosen uniformly at random and a constraint is chosen from also uniformly at random. This procedure is repeated m times independently. We are interested in whether the resulting linear programming problem is feasible. We prove that the feasibility property experiences a linear phase transition, when n and m = cn for a constant c. Namely, there exists a critical value c^* such that, when c < c^*, the problem is feasible or is asymptotically almost feasible, as n, but, when c>c^*, the distance to feasibility is at least a positive constant independent of n. Our result is obtained using the combination of a powerful local weak convergence method developed in Aldous [Ald92], [Ald01], Aldous and Steele [AS03], Steele [Ste02] and martingale techniques. By exploiting a linear programming duality, our theorem implies the following result in the context of sparse random graphs G(n, cn) on n nodes with cn edges, where edges are equipped with randomly generated weights. Let (n, c) denote maximum weight matching in G(n, cn). We prove that when c is a constant and n , the limit lim_n (n, c)/n, exists, with high probability. We further extend this result to maximum weight b-matchings also in G(n, cn).     

The threshold for random -SAT is

Let be a random -CNF formula formed by selecting uniformly and independently out of all possible -clauses on variables. It is well known that if , then is unsatisfiable with probability that tends to 1 as . We prove that if , where , then is satisfiable with probability that tends to 1 as .

Our technique, in fact, yields an explicit lower bound for the random -SAT threshold for every . For our bounds improve all previously known such bounds.

     

时序电路等价验证的触发器匹配

通常的时序电路等价性验证方法是将触发器按时序展开,从而将时序电路转化为组合电路进行验证。而一般在待验证的两个时序电路中,触发器是一一对应的,找到触发器的对应关系,时序电路的验证就会得到很大的简化。该文通过一种新的基于布尔可满足性(SAT)算法的自动测试模式生成(ATPG)匹配模型建立联接电路,使用时序帧展开传递算法比较触发器的帧时序状态输出,同时在SAT解算中加入信息学习继承等启发式算法,将时序电路的触发器一一匹配。在ISCAS89电路上的实验结果表明,该文算法在对触发器的匹配问题上是非常有效的。     

Testing satisfiability

Let Φ be a set of general boolean functions on n variables, such that each function depends on exactly k variables, and each variable can take a value from [1,d]. We say that Φ is ε-far from satisfiable, if one must remove at least εn^k functions in order to make the set of remaining functions satisfiable. Our main result is that if Φ is ε-far from satisfiable, then most of the induced sets of functions, on sets of variables of size c(k,d)/ε², are not satisfiable, where c(k,d) depends only on k and d. Using the above claim, we obtain similar results for k-SAT and k-NAEQ-SAT.Assume we relax the decision problem of whether an instance of one of the above mentioned problems is satisfiable or not, to the problem of deciding whether an instance is satisfiable or ε-far from satisfiable. While the above decision problems are NP-hard, our result implies that we can solve their relaxed versions, that is, distinguishing between satisfiable and ε-far from satisfiable instances, in randomized constant time.From the above result we obtain as a special case, previous results of Alon and Krivelevich, and of Czumaj and Sohler, concerning testing of graphs and hypergraphs colorability. We also discuss the difference between testing with one-sided and two-sided error.     

Satisfiability of algebraic circuits over sets of natural numbers

We investigate the complexity of satisfiability problems for {∪,∩,⁻,+,×}-circuits computing sets of natural numbers. These problems are a natural generalization of membership problems for expressions and circuits studied by Stockmeyer and Meyer (1973) [10] and McKenzie and Wagner (2003) [8].Our work shows that satisfiability problems capture a wide range of complexity classes such as NL, P, NP, PSPACE, and beyond. We show that in several cases, satisfiability problems are harder than membership problems. In particular, we prove that testing satisfiability for {∩,+,×}-circuits is already undecidable. In contrast to this, the satisfiability for {∪,+,×}-circuits is decidable in PSPACE.     

Order preserving reductions and polynomial improving paths

This paper shows that neighborhood transformations and data-independent order transformations preserve the length of improving paths and order of local optima of neighborhood functions. These results imply that finding effective neighborhood functions for Zero-One IP is at least as hard as finding effective neighborhood functions for any other NPO problem.