A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers

Because of the inherent NP-completeness of SAT, many SAT problems currently cannot be solved in a reasonable time. Usually, in order to tackle a new class of SAT problems, new ad hoc algorithms must be designed. Another way to solve a new problem is to use a generic solver and employ parallelism to reduce the solve time. In this paper we propose a parallelization scheme for a class of SAT solvers based on the DPLL procedure. The scheme uses a dynamic load-balancing mechanism based on work-stealing techniques to deal with the irregularity of SAT problems. We parallelize Satz, one of the best generic SAT solvers, with our scheme to obtain a parallel solver called PSatz. The first experimental results on random 3-SAT problems and a set of well-known structured problems show the efficiency of PSatz. PSatz is freely available and runs on any networked workstations under Unix/Linux.     

Many hard examples in exact phase transitions

This paper analyzes the resolution complexity of two random constraint satisfaction problem (CSP) models (i.e. Model RB/RD) for which we can establish the existence of phase transitions and identify the threshold points exactly. By encoding CSPs into CNF formulas, it is proved that almost all instances of Model RB/RD have no tree-like resolution proofs of less than exponential size. Thus, we not only introduce new families of CSPs and CNF formulas hard to solve, which can be useful in the experimental evaluation of CSP and SAT algorithms, but also propose models with both many hard instances and exact phase transitions. Finally, conclusions are presented, as well as a detailed comparison of Model RB/RD with the Hamiltonian cycle problem and random 3-SAT, which, respectively, exhibit three different kinds of phase transition behavior in NP-complete problems.     

Regular Random k-SAT: Properties of Balanced Formulas

We consider a model for generating random k-SAT formulas, in which each literal occurs approximately the same number of times in the formula clauses (regular random and k-SAT). Our experimental results show that such regular random k-SAT instances are much harder than the usual uniform random k-SAT problems. This is in agreement with other results that show that more balanced instances of random combinatorial problems are often much more difficult to solve than uniformly random instances, even at phase transition boundaries. There are almost no formal results known for such problem distributions. The balancing constraints add a dependency between variables that complicates a standard analysis. Regular random 3-SAT exhibits a phase transition as a function of the ratio α of clauses to variables. The transition takes place at approximately α = 3.5. We show that for α > 3.78 with high probability (w.h.p.) random regular 3-SAT formulas are unsatisfiable. Specifically, the events hold with high probability if Pr when n → ∞. We also show that the analysis of a greedy algorithm proposed by Kaporis et al. for the uniform 3-SAT model can be adapted for regular random 3-SAT. In particular, we show that for formulas with ratio α < 2.46, a greedy algorithm finds a satisfying assignment with positive probability.     

Random 2-SAT with Prescribed Literal Degrees

Two classic "phase transitions" in discrete mathematics are the emergence of a giant component in a random graph as the density of edges increases, and the transition of a random 2-SAT formula from satisfiable to unsatisfiable as the density of clauses increases. The random-graph result has been extended to the case of prescribed degree sequences, where the almost-sure nonexistence or existence of a giant component is related to a simple property of the degree sequence. We similarly extend the satisfiability result, by relating the almost-sure satisfiability or unsatisfiability of a random 2-SAT formula to an analogous property of its prescribed literal-degree sequence. The extension has proved useful in analyzing literal-degree-based algorithms for (uniform) random 3-SAT.     

More efficient two-mode stochastic local search for random 3-satisfiability

Stochastic local search (SLS) is a popular paradigm in incomplete solving for the Boolean satisfiability problem (SAT). Most SLS solvers for SAT switch between two modes, i.e., the greedy (intensification) mode and the diversification mode. However, the performance of these two-mode SLS algorithms lags far behind on solving random 3-satisfiability (3-SAT) problem, which is a significant special case of the SAT problem. In this paper, we propose a new hybrid scoring function called M C based on a linear combination of a greedy property m a k e and a diversification property C o n f T i m e s, and then utilize M C to develop a new two-mode SLS solver called CCMC. To evaluate the performance of CCMC, we conduct extensive experiments to compare CCMC with five state-of-the-art two-mode SLS solvers (i.e., Sparrow2011, Sattime2011, EagleUP, gNovelty+PCL and CCASat) on a broad range of random 3-SAT instances, including all large 3-SAT ones from SAT Competition 2009 and SAT Competition 2011 as well as 200 generated satisfiable huge random 3-SAT ones. The experiments illustrate that CCMC obviously outperforms its competitors, indicating the effectiveness of CCMC. We also analyze the effectiveness of the underlying ideas in CCMC and further improve the performance of CCMC on solving random 5-SAT instances.     

Randomized constraint solvers: a comparative study

The complexity of constraints is a major obstacle for constraint-based software verification. Automatic constraint solvers are fundamentally incomplete: input constraints often build on some undecidable theory or some theory the solver does not support. This paper proposes and evaluates several randomized solvers to address this issue. We compared the effectiveness of a symbolic solver (CVC3), a random solver, two heuristic search solvers, and seven hybrid solvers (i.e. mix of random, symbolic, and heuristic solvers). We evaluated the solvers on a benchmark generated with a concolic execution of 9 subjects. The performance of each solver was measured by its precision, which is the fraction of constraints that the solver can find solution out of the total number of constraints that some solver can find solution. As expected, symbolic solving subsumes the other approaches for the 4 subjects that only generate decidable constraints. For the remaining 5 subjects, which contain undecidable constraints, the hybrid solvers achieved the highest precision (fraction of constraints that a solver can find a solution out of the total number of satisfiable constraints). We also observed that the solvers were complementary, which suggests that one should alternate their use in iterations of a concolic execution driver.     

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.     

Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances

An analysis of the average-case complexity of solving random 3-Satisfiability (SAT) instances with backtrack algorithms is presented. We first interpret previous rigorous works in a unifying framework based on the statistical physics notions of dynamical trajectories, phase diagram and growth process. It is argued that, under the action of the Davis–Putnam–Loveland–Logemann (DPLL) algorithm, 3-SAT instances are turned into 2+p-SAT instances whose characteristic parameters (ratio of clauses per variable, fraction p of 3-clauses) can be followed during the operation, and define resolution trajectories. Depending on the location of trajectories in the phase diagram of the 2+p-SAT model, easy (polynomial) or hard (exponential) resolutions are generated. Three regimes are identified, depending on the ratio of the 3-SAT instance to be solved. Lower satisfiable (sat) phase: for small ratios, DPLL almost surely finds a solution in a time growing linearly with the number N of variables. Upper sat phase: for intermediate ratios, instances are almost surely satisfiable but finding a solution requires exponential time (2^Nω with ω>0) with high probability. Unsat phase: for large ratios, there is almost always no solution and proofs of refutation are exponential. An analysis of the growth of the search tree in both upper sat and unsat regimes is presented, and allows us to estimate ω as a function of . This analysis is based on an exact relationship between the average size of the search tree and the powers of the evolution operator encoding the elementary steps of the search heuristic.     

A deterministic (2−2/(k+1))n algorithm for k-SAT based on local search

Local search is widely used for solving the propositional satisfiability problem. Papadimitriou (1991) showed that randomized local search solves 2-SAT in polynomial time. Recently, Schöning (1999) proved that a close algorithm for k-SAT takes time (2−2/k)ⁿ up to a polynomial factor. This is the best known worst-case upper bound for randomized 3-SAT algorithms (cf. also recent preprint by Schuler et al.).We describe a deterministic local search algorithm for k-SAT running in time (2−2/(k+1))ⁿ up to a polynomial factor. The key point of our algorithm is the use of covering codes instead of random choice of initial assignments. Compared to other “weakly exponential” algorithms, our algorithm is technically quite simple. We also describe an improved version of local search. For 3-SAT the improved algorithm runs in time 1.481ⁿ up to a polynomial factor. Our bounds are better than all previous bounds for deterministic k-SAT algorithms.     

基于寻找可满足2SAT子问题的SAT算法*

可满足问题（SAT）是一个NP-Hard问题。提出了一种求解SAT的新算法（FFSAT）。该算法将SAT问题转换为寻找一个可满足的2-SAT子问题。SAT问题虽然是NP完全问题,但是当所有子句长度不大于2时,SAT问题可以在线性时间求解。使用2-SAT算法-BinSat求解2-SAT子问题,当它不满足时,根据赋值选择新的2-SAT子问题。实验结果表明,采用本算法的结果优于UnitWalk。     

随机正则(k,r)-SAT问题的可满足临界

研究k-SAT问题实例中每个变元恰好出现r=2s次,且每个变元对应的正、负文字都出现s次的严格随机正则（k,r）-SAT问题.通过构造一个特殊的独立随机实验,结合一阶矩方法,给出了严格随机正则（k,r）-SAT问题可满足临界值的上界.由于严格正则情形与正则情形的可满足临界值近似相等,因此得到了随机正则（k,r）-SAT问题可满足临界值的新上界.该上界不仅小于当前已有的随机正则（k,r）-SAT问题的可满足临界值上界,而且还小于一般的随机k-SAT问题的可满足临界值.因此,这也从理论上解释了在相变点处的随机正则（k,r）-SAT问题实例通常比在相应相变点处同规模的随机k-SAT问题实例更难满足的原因.最后,数值分析结果验证了所给上界的正确性.     

可满足实例的归结复杂度

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

An optical solution to the 3-SAT problem using wavelength based selectors

In this paper, an optical wavelength-based method to solve a well-known NP-complete problem 3-SAT is provided. In the 3-SAT problem, a formula F in the form of conjunction of some clauses over Boolean variables is given and the question is to find if F is satisfiable or not. The provided method uses exponential number of different wavelengths in a light ray and considers each group of wavelengths as a possible value-assignment for the variables. It then uses optical devices to drop wavelengths not satisfying F from the light ray. At the end, remaining wavelengths indicate satisfiability of the formula. The method provides two ways to arrange the optical devices to select satisfying wavelengths for a given clause: simple clause selectors and combined clause selectors, both requiring exponential preprocessing time. After preprocessing phase, the provided method requires polynomial time and optical devices to solve each problem instance.     

Complexity results for answer set programming with bounded predicate arities and implications

Answer set programming is a declarative programming paradigm rooted in logic programming and non-monotonic reasoning. This formalism has become a host for expressing knowledge representation problems, which reinforces the interest in efficient methods for computing answer sets of a logic program. The complexity of various reasoning tasks for general answer set programming has been amply studied and is understood quite well. In this paper, we present a language fragment in which the arities of predicates are bounded by a constant. Subsequently, we analyze the complexity of various reasoning tasks and computational problems for this fragment, comprising answer set existence, brave and cautious reasoning, and strong equivalence. Generally speaking, it turns out that the complexity drops significantly with respect to the full non-ground language, but is still harder than for the respective ground or propositional languages. These results have several implications, most importantly for solver implementations: Virtually all currently available solvers have exponential (in the size of the input) space requirements even for programs with bounded predicate arities, while our results indicate that for those programs polynomial space should be sufficient. This can be seen as a manifestation of the “grounding bottleneck” (meaning that programs are first instantiated and then solved) from which answer set programming solvers currently suffer. As a final contribution, we provide a sketch of a method that can avoid the exponential space requirement for programs with bounded predicate arities. Some results in this paper have been presented in preliminary form at KR 2004 [15].     

A Probabilistic Algorithm for k -SAT Based on Limited Local Search and Restart

A simple probabilistic algorithm for solving the NP-complete problem k -SAT is reconsidered. This algorithm follows a well-known local-search paradigm: randomly guess an initial assignment and then, guided by those clauses that are not satisfied, by successively choosing a random literal from such a clause and changing the corresponding truth value, try to find a satisfying assignment. Papadimitriou [11] introduced this random approach and applied it to the case of 2-SAT, obtaining an expected O(n ² ) time bound. The novelty here is to restart the algorithm after 3n unsuccessful steps of local search. The analysis shows that for any satisfiable k -CNF formula with n variables the expected number of repetitions until a satisfying assignment is found this way is (2? (k-1)/ k) ⁿ . Thus, for 3-SAT the algorithm presented here has a complexity which is within a polynomial factor of (\frac 4 3 ) ⁿ . This is the fastest and also the simplest among those algorithms known up to date for 3-SAT achieving an o(2 ⁿ ) time bound. Also, the analysis is quite simple compared with other such algorithms considered before.     

Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances

An enhanced concept of sub-optimal reverse Horn fraction of a CNF-formula was introduced in [18]. It was shown that this fraction is very useful in effectively (almost) separating 3-colorable random graphs with fixed node-edge density from the non-3-colorable ones. A correlation between this enhanced sub-optimal reverse Horn fraction and satisfiability of random 3-SAT instances with a fixed density was observed. In this paper, we present experimental evidence that this correlation scales to larger-sized instances and that it extends to solver performances as well, both of complete and incomplete solvers. Furthermore, we give a motivation for various phases in the algorithm aHS, establishing the enhanced sub-optimal reverse Horn fraction, and we present clear evidence for the fact that the observed correlations are stronger than correlations between satisfiability and sub-optimal MAXSAT-fractions established similarly to the enhanced sub-optimal reverse Horn fraction. The latter observation is noteworthy because the correlation between satisfiability and the optimal MAXSAT-fraction is obviously 100%. AMS subject classification 90C05, 03B99, 68Q01, 68W01     

Exact algorithms for a scheduling problem with unrelated parallel machines and sequence and machine-dependent setup times

A scheduling problem with unrelated parallel machines, sequence and machine-dependent setup times, due dates and weighted jobs is considered in this work. A branch-and-bound algorithm (B&B) is developed and a solution provided by the metaheuristic GRASP is used as an upper bound. We also propose a set of instances for this type of problem. The results are compared to the solutions provided by two mixed integer programming models (MIP) with the solver CPLEX 9.0. We carry out computational experiments and the algorithm performs extremely well on instances with up to 30 jobs.     

SAT问题中局部搜索法的改进

局部搜索方法在求解SAT问题的高效率使其成为一研究热点．提出用初始概率的方法对局部搜索算法中变量的初始随机指派进行适当的约束．使在局部搜索的开始阶段,可满足的子句数大大增加,减少了翻转的次数,加快了求解的速度．用该方法对目前的一些重要的SAT问题的局部搜索算法(如WSAT,TSAT,NSAT,SDF等)进行改进,通过对不同规模的随机3-SAT问题的实例和一些不同规模的结构性SAT问题的实例,以及利用相变现象构造的难解SAT实例测试表明,改进后的这些局部搜索算法的求解效率有了很大的提高．该方法对其他局部搜索法的改进具有参考价值。     

一种布尔公式的代数逻辑约化新方法

布尔可满足问题是最早被证明的NP完全问题之一,1-in-3-SAT问题是一个NP完全的布尔可满足子类问题。1-in-3-SAT的计算复杂度取决于对应公式的变量以及子句的个数。将1-in-3公式归约为一个变量数或者子句数更少的1-in-3公式,是提高1-in-3-SAT问题求解效率的一个关键。基于一个新的范式形式——XCNF,针对1-in-3-SAT问题提出一种新的代数逻辑约化方法,用于在多项式时间内约减一个1-in-3公式的变量数和子句数。所提算法的主要思想为:首先将1-in-3公式转化为XCNF公式,然后尝试找出XCNF公式中的X-纯文字,并利用X-纯文字法则对1-in-3公式中相应的布尔变量赋值,最后得到一个约减公式,该约减公式与原公式的1-in-3可满足性等价。     

A GRASP metaheuristic for microarray data analysis

The Weighted Gene Regulatory Network (WGRN) problem consists in pruning a regulatory network obtained from DNA microarray gene expression data, in order to identify a reduced set of candidate elements which can explain the expression of all other genes. Since the problem appears to be particularly hard for general-purpose solvers, we develop a Greedy Randomized Adaptive Search Procedure (GRASP) and refine it with three alternative Path Relinking procedures. For comparison purposes, we also develop a Tabu Search algorithm with a self-adapting tabu tenure. The experimental results show that GRASP performs better than Tabu Search and that Path Relinking significantly contributes to its effectiveness.