A Parallel Quantum Algorithm for the Satisfiability Problem

In this paper we present a classical parallel quantum algorithm for the satisfiability problem. We have exploited the classical parallelism of quantum algorithms developed in [G.L. Long and L. Xiao, Phys. Rev. A 69 （2004） 052303], so that additional acceleration can be gained by using classical parallelism. The quantum algorithm first estimates the number of solutions using the quantum counting algorithm, and then by using the quantum searching algorithm, the explicit solutions are found.

Modified extremal optimization for the hard maximum satisfiability problem

Based on our recent study on probability distributions for evolution in extremal optimization (EO),we propose a modified framework called EOSAT to approximate ground states of the hard maximum satisfiability (MAXSAT) problem,a generalized version of the satisfiability (SAT) problem.The basic idea behind EOSAT is to generalize the evolutionary probability distribution in the Bose-Einstein-EO (BE-EO) algorithm,competing with other popular algorithms such as simulated annealing and WALKSAT.Experimental results on the hard MAXSAT instances from SATLIB show that the modified algorithms are superior to the original BE-EO algorithm.

Determination of Consistency between Quantitative Evaluation and Non-quantitative Evaluation

The combination of quantitative evaluation(QE)and non-quantitative evaluation(NQE)is an important evaluation tool in the fields of academic level evaluation(e.g.,EasyChair,Academic paper review form)and internet commodity evaluation(e.g.,Amazon’s review,Feedback).But the inconsistency between QE and NQE greatly reduces the correctness and usability of the evaluation.Therefore,it is a necessary task to judge whether QE is consistent with NQE.In this paper,the predicate formula satisfiability problem is firstly reduced in polynomial time to the consistency problem of QE and NQE,and the uncertainty of the consistency problem is proved.Then the approximate solution to the problem is investigated by using a natural language processing method,which performs sentiment analysis on NQE and finally invokes a database query statement to determine whether QE is consistent with NQE.The results shed light on the feasibility of using the natural language processing method to solve undecidable problems.

Properties of the satisfiability threshold of the strictly d-regular random(3,2s)-SAT problem

A k-CNF(conjunctive normal form)formula is a regular(k,s)-CNF one if every variable occurs s times in the formula,where k≥2 and s>0 are integers.Regular(3,s)-CNF formulas have some good structural properties,so carry-ing out a probability analysis of the structure for random formulas of this type is easier than conducting such an analysisfor random 3-CNF formulas.Some subclasses of the regular(3,s)-CNF formula have also characteristics of intractabilitythat differ from random 3-CNF formulas.For this purpose,we propose strictly d-regular(k,2s)-CNF formula,which is aregular(k,2s)-CNF formula for which d≥0 is an even num-ber and each literal occurs s-d/2 or s+d/2 times(the literals from a variable x are x and-x,where x is positive and-x isnegative).In this paper,we present a new model to generatestrictly d-regular random(k,2s)-CNF formulas,and focuson the strictly d-regular random(3,2s)-CNF formulas.Let F be a strictly d-regular random(3,2s)-CNF formula suchthat 2s>d.We show that there exists a real number so suchthat the formula F is unsatisfiable with high probability whens>so,and present a numerical solution for the real numberso.The result is supported by simulated experiments,and isconsistent with the existing conclusion for the case of d=0.Furthermore,we have a conjecture:for a given d,the strictlyd-regular random(3,2s)-SAT problem has an SAT-UNSAT(satisfiable-unsatisfiable)phase transition.Our experimentssupport this conjecture.Finally,our experiments also showthat the parameter d is correlated with the intractability of the 3-SAT problem.Therefore,our research maybe helpful for generating random hard instances of the 3-CNF formula.

On Optimizing the Satisfiability (SAT) Problem

The satisfiability(SAT) problem is a basic problem in computing theory. Presently, an active area of research on SAT problem is to design efficient optimization algorithms for finding a solution for a satisfiable CNF formula. A new formulation, the Universal SAT problem model, which transforms the SAT problem on Boofean space into an optimization problem on real space has been developed. Many optimization techniques, such as the steepest descent method, Newton's method, and the coordinate descent method, can be used to solve the Universal SAT problem. In this paper, we prove that, when the initial solution is sufficiently close to the optimal solution, the steepest descent method has a linear convergence ratio β<1, Newton's method has a convergence ratio of order two, and the convergence ratio of the coordinate descent method is approximately (1-β/m) for the Universal SAT problem with m variables. An algorithm based on the coordinate descent method for the Universal SAT problem is also presented in this paper.

A Practical Parallel Algorithm for Propositional Knowledge Base Revision

Different methods for revising propositional knowledge base have been proposed recently by several researchers, but all methods are intractable in the general case. For practical application, this paper presents a revision method in special case, and gives a corresponding polynomial algorithm as well as its parallel version on CREW PRAM.

Defeating constraint based program analysis with temporal correlation function

Constraint based program analysis is widely used in program validation, program vulnerability analysis, etc. This paper proposes a temporal correlation function to protect programs from analysis. The temporal correlation function can be applied to resist against both static and dynamic function summary and eoncolie testing. What＇ s more, the temporal correlation function can produce different outputs even with same input. This feature can be used to damage the premise of function summary as well as prevent concolie testing process to run the new branch with new input. Experiment results show that this method can reduce efficiency and path coverage of concolic testing, while greatly in- creasing the difficulty of constraint based program analysis.

A unified pre-training and adaptation framework for combinatorial optimization on graphs

Combinatorial optimization(CO)on graphs is a classic topic that has been extensively studied across many scientific and industrial fields.Recently,solving CO problems on graphs through learning methods has attracted great attention.Advanced deep learning methods,e.g.,graph neural networks(GNNs),have been used to effectively assist the process of solving COs.However,current frameworks based on GNNs are mainly designed for certain CO problems,thereby failing to consider their transferable and generalizable abilities among different COs on graphs.Moreover,simply using original graphs to model COs only captures the direct correlations among objects,which does not consider the mathematical logicality and properties of COs.In this paper,we propose a unified pre-training and adaptation framework for COs on graphs with the help of the maximum satisfiability(Max-SAT)problem.We first use Max-SAT to bridge different COs on graphs since they can be converted to Max-SAT problems represented by standard formulas and clauses with logical information.Then we further design a pre-training and domain adaptation framework to extract the transferable and generalizable features so that different COs can benefit from them.In the pre-training stage,Max-SAT instances are generated to initialize the parameters of the model.In the fine-tuning stage,instances from CO and Max-SAT problems are used for adaptation so that the transferable ability can be further improved.Numerical experiments on several datasets show that features extracted by our framework exhibit superior transferability and Max-SAT can boost the ability to solve COs on graphs.

Task-resource Scheduling Problem

Cloud computing is a new and rapidly emerging computing paradigm where applications, data and IT services are provided over the Internet. The task-resource management is the key role in cloud computing systems. Task-resource scheduling problems are premier which relate to the efficiency of the whole cloud computing facilities. Task-resource scheduling problem is NP-complete. In this paper, we consider an approach to solve this problem optimally. This approach is based on constructing a logical model for the problem. Using this model, we can apply algorithms for the satisfiability problem (SAT) to solve the task-resource scheduling problem. Also, this model allows us to create a testbed for particle swarm optimization algorithms for scheduling workflows.

Satisfiability with Index Dependency

We study the Boolean satisfiability problem （SAT） restricted on input formulas for which there are linear arithmetic constraints imposed on the indices of variables occurring in the same clause. This can be seen as a structural counterpart of Schaefer＇s dichotomy theorem which studies the SAT problem with additional constraints on the assigned values of variables in the same clause. More precisely, let k-SAT（m, A） denote the SAT problem restricted on instances of k-CNF formulas, in every clause of which the indices of the last k - m variables are totally decided by the first m ones through some linear equations chosen from A. For example, if A contains i3 = il ＋ 2i2 and i4 = i2 - i1 ＋ 1, then a clause of the input to 4-SAT（2, A） has the form Yi1 V Yi2 V Yi1＋2i2 V yi2-i1＋1, with yi being xi or xi^-. We obtain the following results： 1） If m ≥ 2, then for any set .4 of linear constraints, the restricted problem k-SAT（m, A） is either in P or NP-complete assuming P ≠ NP. Moreover, the corresponding #SAT problem is always #P-complete, and the MAx-SAT problem does not allow a polynomial time approximation scheme assuming P ≠ NP. 2） m = 1, that is, in every clause only one index can be chosen freely. In this case, we develop a general framework together with some techniques for designing polynomial-time algorithms for the restricted SAT problems. Using these, we prove that for any .A, #2-SAT（1, .A） and MAX-2-SAT（1, A） are both polynomial-time solvable, which is in sharp contrast with the hardness results of general #2-SAT and MAX-2-SAT. For fixed k ≥ 3, we obtain a large class of non-trivial constraints .4, under which the problems k-SAT（1, A）, #k-SAT（1, .A） and MAx-k-SAT（1, A） can all be solved in polynomial time or quasi-polynomial time.

Solving SAT by Algorithm Transform of Wu's Method

Recently algorithms for solving propositional satisfiability problem,or SAT, have aroused great illterest, and more attention has been paid to trans-formation problem solving. The commonly used transformation is representationtransform, but since its ifltermediate computing procedure is a black box from theviewpoint of the original problem, this aPproach has many limitations. In this paper, a new approach called algorithm transform is proposed and applied to solvingSAT by Wu's method, a general algorithm for solving polynomial equations. By es-tablishing the correspondellce between the primitive operation in Wu's method andclause resolution in SAT, it is shown that Wu's method, when used for solving SAT,is primarily a restricted clause resolution procedure. While Wu's method illtroduceselltirely new concepts, e.g. characteristic set of clauses, to resolution procedure, thecomplexity result of resolution procedure suggests an exponential lower bound toWu's method for solving general polynomial equations. Moreover, this algorithmtransform can help achieve a more efficiellt imp1ementation of Wu's method since itcan avoid the complex manipulation of polynomials and can make the best use ofdomain specific knowledge.

Experimental Study on Strategy of CombiningSAT Algorithms

The effectiveness of many SAT algorithms is mainly reflected by their significant performances on one or several classes of specific SAT problems. Different kinds of SAT algorithmsall have their own hard instances respectively. Therefore, to get the better performance onall kinds of problems, SAT solver should know how to select different algorithms according tothe feature of instances. In this paper the differences of several effective SAT algorithms areanalyzed and two new parameters gb and & are proposed to characterize the feature of SATinstances. Experiments are performed to study the relationship between SAT algorithms andsome statistical parameters including Φ, δ. Based on this analysis, a strategy is presented fordesigning a faster SAT tester by carefully combining some existing SAT algorithms. With thisstrategy, a faster SAT tester to solve many kinds of SAT problem is obtained.

A Practical Propositional Knowledge Base Revision Algorithm

This paper gives an outline of knowledge base revision and some recently presented complexity results about propositional knowledge base revision. Different methods for revising propositional knowledge baize have been proposed recently by several researchers, but all methods are intractable in the general case. For practical application, this paper presents a revision method for special case, and gives its corresponding polynomial algorithm.

Polynomial algorithm of limited propositional deduction

For the problem of propositional satisfiability a polynomial algorithm of limited propositional deduction is proposed which can be viewed as a sort of boolean constraint propagation mechanism. It can be embodied in a backtracking search program for propositional satisfiability problems to make search efficient. The efficiency is gained in two ways:One is to use the algorithm to derive literals so as to overcome the ambiguities in search. The other is to exploit the consequence sets of unbound atoms generated during limited deduction as a heuristic measure for possible choices. The experiments have shown remarkable improvement in reducing search space.