اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدThe Connectivity of Boolean Satisfiability: Dichotomies for Formulas and Circuits
128
0
0.0
(
0
)
نشر من قبل
Konrad W. Schwerdtfeger
تاريخ النشر
2013
مجال البحث
الهندسة المعلوماتية
والبحث باللغة
English
تأليف
Konrad W. Schwerdtfeger
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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. For this implicitly define
d 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. st
udied 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.
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 h
euristics 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.
Efficient solutions to NP-complete problems would significantly benefit both science and industry. However, such problems are intractable on digital computers based on the von Neumann architecture, thus creating the need for alternative solutions to
tackle such problems. Recently, a deterministic, continuous-time dynamical system (CTDS) was proposed (Nat.Phys. {bf 7}(12), 966 (2011)) to solve a representative NP-complete problem, Boolean Satisfiability (SAT). This solver shows polynomial analog time-complexity on even the hardest benchmark $k$-SAT ($k geq 3$) formulas, but at an energy cost through exponentially driven auxiliary variables. This paper presents a novel analog hardware SAT solver, AC-SAT, implementing the CTDS via incorporating novel, analog circuit design ideas. AC-SAT is intended to be used as a co-processor and is programmable for handling different problem specifications. It is especially effective for solving hard $k$-SAT problem instances that are challenging for algorithms running on digital machines. Furthermore, with its modular design, AC-SAT can readily be extended to solve larger size problems, while the size of the circuit grows linearly with the product of the number of variables and number of clauses. The circuit is designed and simulated based on a 32nm CMOS technology. SPICE simulation results show speedup factors of $sim$10$^4$ on even the hardest 3-SAT problems, when compared with a state-of-the-art SAT solver on digital computers. As an example, for hard problems with $N=50$ variables and $M=212$ clauses, solutions are found within from a few $ns$ to a few hundred $ns$.
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 cla
sses 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.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
