Do you want to publish a course? Click here

The Connectivity of Boolean Satisfiability: No-Constants and Quantified Variants

170   0   0.0 ( 0 )
 Publication date 2014
and research's language is English




Ask ChatGPT about the research

For Boolean satisfiability problems, the structure of the solution space is characterized by the solution graph, where the vertices are the solutions, and two solutions are connected iff they differ in exactly one variable. Motivated by research on heuristics and the satisfiability threshold, Gopalan et al. in 2006 studied connectivity properties of the solution graph and related complexity issues for constraint satisfaction problems in Schaefers framework. They found dichotomies for the diameter of connected components and for the complexity of the st-connectivity question, and conjectured a trichotomy for the connectivity question that we recently were able to prove. While Gopalan et al. considered CNF(S)-formulas with constants, we here look at two important variants: CNF(S)-formulas without constants, and partially quantified formulas. For the diameter and the st-connectivity question, we prove dichotomies analogous to those of Gopalan et al. in these settings. While we cannot give a complete classification for the connectivity problem yet, we identify fragments where it is in P, where it is coNP-complete, and where it is PSPACE-complete, in analogy to Gopalan et al.s trichotomy.



rate research

Read More

For Boolean satisfiability problems, the structure of the solution space is characterized by the solution graph, where the vertices are the solutions, and two solutions are connected iff they differ in exactly one variable. For this implicitly defined graph, we here study the st-connectivity and connectivity problems. Building on the work of Gopalan et al. (The Connectivity of Boolean Satisfiability: Computational and Structural Dichotomies, 2006/2009), we first investigate satisfiability problems given by CSPs, more exactly CNF(S)-formulas with constants (as considered in Schaefers famous 1978 dichotomy theorem); we prove a computational dichotomy for the st-connectivity problem, asserting that it is either solvable in polynomial time or PSPACE-complete, and an aligned structural dichotomy, asserting that the maximal diameter of connected components is either linear in the number of variables, or can be exponential; further, we show a trichotomy for the connectivity problem, asserting that it is either in P, coNP-complete, or PSPACE-complete. Next we investigate two important variants: CNF(S)-formulas without constants, and partially quantified formulas; in both cases, we prove analogous dichotomies for st-connectivity and the diameter; for for the connectivity problem, we show a trichotomy in the case of quantified formulas, while in the case of formulas without constants, we identify fragments of a possible trichotomy. Finally, we consider the connectivity issues for B-formulas, which are arbitrarily nested formulas built from some fixed set B of connectives, and for B-circuits, which are Boolean circuits where the gates are from some finite set B; we prove a common dichotomy for both connectivity problems and the diameter; for partially quantified B-formulas, we show an analogous dichotomy.
For Boolean satisfiability problems, the structure of the solution space is characterized by the solution graph, where the vertices are the solutions, and two solutions are connected iff they differ in exactly one variable. In 2006, Gopalan et al. studied connectivity properties of the solution graph and related complexity issues for CSPs, motivated mainly by research on satisfiability algorithms and the satisfiability threshold. They proved dichotomies for the diameter of connected components and for the complexity of the st-connectivity question, and conjectured a trichotomy for the connectivity question. Recently, we were able to establish the trichotomy [arXiv:1312.4524]. Here, we consider connectivity issues of satisfiability problems defined by Boolean circuits and propositional formulas that use gates, resp. connectives, from a fixed set of Boolean functions. We obtain dichotomies for the diameter and the two connectivity problems: on one side, the diameter is linear in the number of variables, and both problems are in P, while on the other side, the diameter can be exponential, and the problems are PSPACE-complete. For partially quantified formulas, we show an analogous dichotomy.
For Boolean satisfiability problems, the structure of the solution space is characterized by the solution graph, where the vertices are the solutions, and two solutions are connected iff they differ in exactly one variable. In 2006, Gopalan et al. studied connectivity properties of the solution graph and related complexity issues for CSPs, motivated mainly by research on satisfiability algorithms and the satisfiability threshold. They proved dichotomies for the diameter of connected components and for the complexity of the st-connectivity question, and conjectured a trichotomy for the connectivity question. Building on this work, we here prove the trichotomy: Connectivity is either in P, coNP-complete, or PSPACE-complete. Also, we correct a minor mistake of Gopalan et al., which leads to a slight shift of the boundaries towards the hard side.
86 - Bernd. R. Schuh 2020
The paper explores the correspondence between balanced incomplete block designs (BIBD) and certain linear CNF formulas by identifying the points of a block design with the clauses of the Boolean formula and blocks with Boolean variables. Parallel classes in BIBDs correspond to XSAT solutions in the corresponding formula. This correspondence allows for transfers of results from one field to the other. As a new result we deduce from known satisfiability theorems that the problem of finding a parallel class in a partially balanced incomplete block design is NP-complete.
Transient chaos is an ubiquitous phenomenon characterizing the dynamics of phase space trajectories evolving towards a steady state attractor in physical systems as diverse as fluids, chemical reactions and condensed matter systems. Here we show that transient chaos also appears in the dynamics of certain efficient algorithms searching for solutions of constraint satisfaction problems that include scheduling, circuit design, routing, database problems or even Sudoku. In particular, we present a study of the emergence of hardness in Boolean satisfiability ($k$-SAT), a canonical class of constraint satisfaction problems, by using an analog deterministic algorithm based on a system of ordinary differential equations. Problem hardness is defined through the escape rate $kappa$, an invariant measure of transient chaos of the dynamical system corresponding to the analog algorithm, and it expresses the rate at which the trajectory approaches a solution.We show that for a given density of constraints and fixed number of Boolean variables $N$, the hardness of formulas in random $k$-SAT ensembles has a wide variation, approximable by a lognormal distribution. We also show that when increasing the density of constraints $alpha$, hardness appears through a second-order phase transition at $alpha_{chi}$ in the random 3-SAT ensemble where dynamical trajectories become transiently chaotic. A similar behavior is found in 4-SAT as well, however, such transition does not occur for 2-SAT. This behavior also implies a novel type of transient chaos in which the escape rate has an exponential-algebraic dependence on the critical parameter $kappa sim N^{B|alpha - alpha_{chi}|^{1-gamma}}$ with $0< gamma < 1$. We demonstrate that the transition is generated by the appearance of metastable basins in the solution space as the density of constraints $alpha$ is increased.
comments
Fetching comments Fetching comments
Sign in to be able to follow your search criteria
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا