A Structural Entropy Measurement Principle of Propositional Formulas in Conjunctive Normal Form.

The satisfiability (SAT) problem is a core problem in computer science. Existing studies have shown that most industrial SAT instances can be effectively solved by modern SAT solvers while random SAT instances cannot. It is believed that the structural characteristics of different SAT formula classes are the reasons behind this difference. In this paper, we study the structural properties of propositional formulas in conjunctive normal form (CNF) by the principle of structural entropy of formulas. First, we used structural entropy to measure the complex structure of a formula and found that the difficulty solving the formula is related to the structural entropy of the formula. The smaller the compressing information of a formula, the more difficult it is to solve the formula. Secondly, we proposed a λ-approximation strategy to approximate the structural entropy of large formulas. The experimental results showed that the proposed strategy can effectively approximate the structural entropy of the original formula and that the approximation ratio is more than 92%. Finally, we analyzed the structural properties of a formula in the solution process and found that a local search solver tends to select variables in different communities to perform the next round of searches during a search and that the structural entropy of a variable affects the probability of the variable being flipped. By using these conclusions, we also proposed an initial candidate solution generation strategy for a local search for SAT, and the experimental results showed that this strategy effectively improves the performance of the solvers CCAsat and Sparrow2011 when incorporated into these two solvers.

Uniquely Satisfiable d-Regular (k,s)-SAT Instances.

Unique k-SAT is the promised version of k-SAT where the given formula has 0 or 1 solution and is proved to be as difficult as the general k-SAT. For any k ≥ 3 , s ≥ f ( k , d ) and ( s + d ) / 2 > k - 1 , a parsimonious reduction from k-CNF to d-regular (k,s)-CNF is given. Here regular (k,s)-CNF is a subclass of CNF, where each clause of the formula has exactly k distinct variables, and each variable occurs in exactly s clauses. A d-regular (k,s)-CNF formula is a regular (k,s)-CNF formula, in which the absolute value of the difference between positive and negative occurrences of every variable is at most a nonnegative integer d. We prove that for all k ≥ 3 , f ( k , d ) ≤ u ( k , d ) + 1 and f ( k , d + 1 ) ≤ u ( k , d ) . The critical function f ( k , d ) is the maximal value of s, such that every d-regular (k,s)-CNF formula is satisfiable. In this study, u ( k , d ) denotes the minimal value of s such that there exists a uniquely satisfiable d-regular (k,s)-CNF formula. We further show that for s ≥ f ( k , d ) + 1 and ( s + d ) / 2 > k - 1 , there exists a uniquely satisfiable d-regular ( k , s + 1 ) -CNF formula. Moreover, for k ≥ 7 , we have that u ( k , d ) ≤ f ( k , d ) + 1 .

(1,0)-Super Solutions of (k,s)-CNF Formula.

A (1,0)-super solution is a satisfying assignment such that if the value of any one variable is flipped to the opposite value, the new assignment is still a satisfying assignment. Namely, every clause must contain at least two satisfied literals. Because of its robustness, super solutions are concerned in combinatorial optimization problems and decision problems. In this paper, we investigate the existence conditions of the (1,0)-super solution of ( k , s ) -CNF formula, and give a reduction method that transform from k-SAT to (1,0)- ( k + 1 , s ) -SAT if there is a ( k + 1 , s )-CNF formula without a (1,0)-super solution. Here, ( k , s ) -CNF is a subclass of CNF in which each clause has exactly k distinct literals, and each variable occurs at most s times. (1,0)- ( k , s ) -SAT is a problem to decide whether a ( k , s ) -CNF formula has a (1,0)-super solution. We prove that for k > 3 , if there exists a ( k , s ) -CNF formula without a (1,0)-super solution, (1,0)- ( k , s ) -SAT is NP-complete. We show that for k > 3 , there is a critical function φ ( k ) such that every ( k , s ) -CNF formula has a (1,0)-super solution for s ≤ φ ( k ) and (1,0)- ( k , s ) -SAT is NP-complete for s > φ ( k ) . We further show some properties of the critical function φ ( k ) .

The Convergence of a Cooperation Markov Decision Process System.

In a general Markov decision progress system, only one agent's learning evolution is considered. However, considering the learning evolution of a single agent in many problems has some limitations, more and more applications involve multi-agent. There are two types of cooperation, game environment among multi-agent. Therefore, this paper introduces a Cooperation Markov Decision Process (CMDP) system with two agents, which is suitable for the learning evolution of cooperative decision between two agents. It is further found that the value function in the CMDP system also converges in the end, and the convergence value is independent of the choice of the value of the initial value function. This paper presents an algorithm for finding the optimal strategy pair (πk0,πk1) in the CMDP system, whose fundamental task is to find an optimal strategy pair and form an evolutionary system CMDP(πk0,πk1). Finally, an example is given to support the theoretical results.

Accurate intravoxel incoherent motion parameter estimation using Bayesian fitting and reduced number of low b-values.

PURPOSE: Intravoxel incoherent motion (IVIM) magnetic resonance imaging is a potential noninvasive technique for the diagnosis of brain tumors. However, perfusion-related parameter mapping is a persistent problem. The purpose of this paper is to investigate the IVIM parameter mapping of brain tumors using Bayesian fitting and low b-values. METHODS: Bayesian shrinkage prior (BSP) fitting method and different low b-value distributions were used to estimate IVIM parameters (diffusion D, pseudo-diffusion D*, and perfusion fraction F). The results were compared to those obtained by least squares (LSQ) on both simulated and in vivo brain data. Relative error (RE) and reproducibility were used to evaluate the results. The differences of IVIM parameters between brain tumor and normal regions were compared and used to assess the performance of Bayesian fitting in the IVIM application of brain tumor. RESULTS: In tumor regions, the value of D* tended to be decreased when the number of low b-values was insufficient, especially with LSQ. BSP required less low b-values than LSQ for the correct estimation of perfusion parameters of brain tumors. The IVIM parameter maps of brain tumors yielded by BSP had smaller variability, lower RE, and higher reproducibility with respect to those obtained by LSQ. Obvious differences were observed between tumor and normal regions in parameters D (P < 0.05) and F (P < 0.001), especially F. BSP generated fewer outliers than LSQ, and distinguished better tumors from normal regions in parameter F. CONCLUSIONS: Intravoxel incoherent motion parameters clearly allow brain tumors to be differentiated from normal regions. Bayesian fitting yields robust IVIM parameter mapping with fewer outliers and requires less low b-values than LSQ for the parameter estimation.

Estimation of intravoxel incoherent motion parameters using low b-values.

Intravoxel incoherent motion (IVIM) imaging is a magnetic resonance imaging (MRI) technique widely used in clinical applications for various organs. However, IVIM imaging at low b-values is a persistent problem. This paper aims to investigate in a systematic and detailed manner how the number of low b-values influences the estimation of IVIM parameters. To this end, diffusion-weighted (DW) data with different low b-values were simulated to get insight into the distributions of subsequent IVIM parameters. Then, in vivo DW data with different numbers of low b-values and different number of excitations (NEX) were acquired. Finally, least-squares (LSQ) and Bayesian shrinkage prior (BSP) fitting methods were implemented to estimate IVIM parameters. The influence of the number of low b-values on IVIM parameters was analyzed in terms of relative error (RE) and structural similarity (SSIM). The results showed that the influence of the number of low b-values on IVIM parameters is variable. LSQ is more dependent on the number of low b-values than BSP, but the latter is more sensitive to noise.