This paper is devoted to the complexity of the Boolean satisfiability problem. We consider a version of this problem, where the Boolean formula is specified in the conjunctive normal form. We prove an unexpected result that the CNF-satisfiability problem can be solved by a deterministic Turing machine in polynomial time.
In this paper, we analyze the argument made by Kumar in the technical report "Necessary and Sufficient Condition for Satisfiability of a Boolean Formula in CNF and Its Implications on P versus NP problem." The paper claims to present a polynomial-time algorithm that decides CNF-SAT. We show that the paper's analysis is flawed and that the fundamental underpinning of its algorithm requires an exponential number of steps on infinitely many inputs.
Boolean satisfiability problem has applications in various fields. An efficient algorithm to solve satisfiability problem can be used to solve many other problems efficiently. The input of satisfiability problem is a finite set of clauses. In this paper, properties of clauses have been studied. A type of clauses have been defined, called fully populated clauses, which contains each variable exactly once. A relationship between two unequal fully populated clauses has been defined, called sibling clauses. It has been found that, if one fully populated clause is false, for a truth assignment, the…
We describe an algorithm to solve the problem of Boolean CNF-Satisfiability when the input formula is chosen randomly. We build upon the algorithms of Sch{ö}ning 1999 and Dantsin et al.~in 2002. The Sch{ö}ning algorithm works by trying many possible random assignments, and for each one searching systematically in the neighborhood of that assignment for a satisfying solution. Previous algorithms for this problem run in time $O(2^{n (1- Ω(1)/k)})$. Our improvement is simple: we count how many clauses are satisfied by each randomly sampled assignment, and only search in the neighborhoods of assig…
University of British Columbia Okanagan(不列颠哥伦比亚大学奥肯那根分校)
We study random instances of the weighted $d$-CNF satisfiability problem (WEIGHTED $d$-SAT), a generic W[1]-complete problem. A random instance of the problem consists of a fixed parameter $k$ and a random $d$-CNF formula $\weicnf{n}{p}{k, d}$ generated as follows: for each subset of $d$ variables and with probability $p$, a clause over the $d$ variables is selected uniformly at random from among the $2^d - 1$ clauses that contain at least one negated literals. We show that random instances of WEIGHTED $d$-SAT can be solved in $O(k^2n + n^{O(1)})$-time with high probability, indicating that ty…
Given a CNF formula $F$, we present a new algorithm for deciding the satisfiability (SAT) of $F$ and computing all solutions of assignments. The algorithm is based on the concept of \emph{cofactors} known in the literature. This paper is a fallout of the previous work by authors on Boolean satisfiability \cite{sul1, sul2,sude}, however the algorithm is essentially independent of the orthogonal expansion concept over which previous papers were based. The algorithm selects a single concrete cofactor recursively by projecting the search space to the set which satisfies a CNF in the formula. This …
Open questions with respect to the computational complexity of linear CNF formulas in connection with regularity and uniformity are addressed. In particular it is proven that any l-regular monotone CNF formula is XSAT-unsatisfiable if its number of clauses m is not a multiple of l. For exact linear formulas one finds surprisingly that l-regularity implies k-uniformity, with m = 1 + k(l-1)) and allowed k-values obey k(k-1) = 0 (mod l). Then the computational complexity of the class of monotone exact linear and l-regular CNF formulas with respect to XSAT can be determined: XSAT-satisfiability is…
The aim of the paper is to answer a long-standing open problem on the relationship between NP and BQP. The paper shows that BQP contains NP by proposing a BQP quantum algorithm for the MAX-E3-SAT problem which is a fundamental NP-hard problem. Given an E3-CNF Boolean formula, the aim of the MAX-E3-SAT problem is to find the variable assignment that maximizes the number of satisfied clauses. The proposed algorithm runs in $O(m^2)$ for an E3-CNF Boolean formula with $m$ clauses and in the worst case runs in $O(n^6)$ for an E3-CNF Boolean formula with $n$ inputs. The proposed algorithm maximizes …
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.
The relationship between the complexity classes P and NP is an unsolved question in the field of theoretical computer science. In this paper, we investigate a descriptor approach based on lattice properties. This paper proposes a new way to decide the satisfiability of any 3-CNF-SAT problem. The analysis of this exact [non heuristical] algorithm shows a strictly bounded exponential complexity. The complexity of any 3-CNF-SAT solution is bounded by O(2^490). This over-estimated bound is reached by an algorithm working on the smallest description (via descriptor functions) of the evolving set of…
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 Schaefer's framework. They found dichotomies for the diameter of connected components and for the complexity of the st-connectivity question, and conjectured a…
Whether the satisfiability of any formula F of propositional calculus can be determined in polynomial time is an open question. I propose a simple procedure based on some real world mechanisms to tackle this problem. The main result is the blueprint for a machine which is able to test any formula in conjunctive normal form (CNF) for satisfiability in linear time. The device uses light and some electrochemical properties to function. It adapts itself to the scope of the problem without growing exponentially in mass with the size of the formula. It requires infinite precision in its components i…
The CNF formula satisfiability problem (CNF-SAT) has been reduced to many fundamental problems in P to prove tight lower bounds under the Strong Exponential Time Hypothesis (SETH). Recently, the works of Abboud, Hansen, Vassilevska W. and Williams (STOC 16), and later, Abboud and Bringmann (ICALP 18) have proposed basing lower bounds on the hardness of general boolean formula satisfiability (Formula-SAT). Reductions from Formula-SAT have two advantages over the usual reductions from CNF-SAT: (1) conjectures on the hardness of Formula-SAT are arguably much more plausible than those of CNF-SAT, …
By a probabilistic construction, we find a bipartite graph having average degree $d$ which can be expressed as a conjunctive normal form using $C \log d$ clauses. This contradicts research problem 1.33 of Jukna.
We consider the weighted antimonotone and the weighted monotone satisfiability problems on normalized circuits of depth at most $t \geq 2$, abbreviated {\sc wsat$^-[t]$} and {\sc wsat$^+[t]$}, respectively. These problems model the weighted satisfiability of antimonotone and monotone propositional formulas (including weighted anitmonoone/monotone {\sc cnf-sat}) in a natural way, and serve as the canonical problems in the definition of the parameterized complexity hierarchy. We characterize the parameterized complexity of {\sc wsat$^-[t]$} and {\sc wsat$^+[t]$} with respect to the genus of the …
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 Schaefer's famous …
We present a general framework for good CNF-representations of boolean constraints, to be used for translating decision problems into SAT problems (i.e., deciding satisfiability for conjunctive normal forms). We apply it to the representation of systems of XOR-constraints, also known as systems of linear equations over the two-element field, or systems of parity constraints. The general framework defines the notion of "representation", and provides several methods to measure the quality of the representation by the complexity ("hardness") needed for making implicit "knowledge" of the represent…
The study of regular linear conjunctive normal form (LCNF) formulas is of interest because exact satisfiability (XSAT) is known to be NP-complete for this class of formulas. In a recent paper it was shown that the subclass of regular exact LCNF formulas (XLCNF) is of sub-exponential complexity, i.e. XSAT can be determined in sub-exponential time. Here I show that this class is just a subset of a larger class of LCNF formulas which display this very kind of complexity. To this end I introduce the property of disjointedness of LCNF formulas, measured, for a single clause C, by the number of clau…
The relationship between the complexity classes $P$ and $NP$ is an unsolved question in the field of theoretical computer science. In the first part of this paper, a lattice framework is proposed to handle the 3-CNF-SAT problems, known to be in $NP$. In the second section, we define a multi-linear descriptor function ${\cal H}_φ$ for any 3-CNF-SAT problem $φ$ of size $n$, in the sense that ${\cal H}_φ: \{0,1\}^n \rightarrow \{0,1\}^n$ is such that $Im \; {\cal H}_φ$ is the set of all the solutions of $φ$. A new merge operation ${\cal H}_φ\bigwedge {\cal H}_ψ$ is defined, where $ψ$ is a single …
Quantum logic was introduced in 1936 by Garrett Birkhoff and John von Neumann as a framework for capturing the logical peculiarities of quantum observables. It generalizes, and on 1-dimensional Hilbert space coincides with, Boolean propositional logic. We introduce the weak and strong satisfiability problem for quantum logic terms. It turns out that in dimension two both are also NP-complete. For higher-dimensional spaces R^d and C^d with d>2 fixed, on the other hand, we show both problems to be complete for the nondeterministic Blum-Shub-Smale model of real computation. This provides a unifie…
A computational problem exhibits a "gap property" when there is no tractable boundary between two disjoint sets of instances. We establish a Gap Trichotomy Theorem for a family of constraint problem variants, completely classifying the complexity of possible ${\bf NP}$-hard gaps in the case of Boolean domains. As a consequence, we obtain a number of dichotomies for the complexity of specific variants of the constraint satisfaction problem: all are either polynomial-time tractable or $\mathbf{NP}$-complete. Schaefer's original dichotomy for $\textsf{SAT}$ variants is a notable particular case. …
This paper depicts algorithms for solving the decision Boolean Satisfiability Problem. An extreme problem is formulated to analyze the complexity of algorithms and the complexity for solving it. A novel and easy reformulation as a lottery for an extreme case is presented to determine a stable complexity around $2^n$. The reformulation point out that the decision Boolean Satisfiability Problem can only be solved in exponential time. This implies there is not an efficient algorithm for the NP Class.
We show conditional lower bounds for well-studied #P-hard problems: (a) The number of satisfying assignments of a 2-CNF formula with n variables cannot be counted in time exp(o(n)), and the same is true for computing the number of all independent sets in an n-vertex graph. (b) The permanent of an n x n matrix with entries 0 and 1 cannot be computed in time exp(o(n)). (c) The Tutte polynomial of an n-vertex multigraph cannot be computed in time exp(o(n)) at most evaluation points (x,y) in the case of multigraphs, and it cannot be computed in time exp(o(n/polylog n)) in the case of simple graphs…
Generalised Satisfiability Problems (or Boolean Constraint Satisfaction Problems), introduced by Schaefer in 1978, are a general class of problem which allow the systematic study of the complexity of satisfiability problems with different types of constraints. In 1979, Valiant introduced the complexity class parity P, the problem of counting the number of solutions to NP problems modulo two. Others have since considered the question of counting modulo other integers. We give a dichotomy theorem for the complexity of counting the number of solutions to Generalised Satisfiability Problems modulo…
Detecting and eliminating logic hazards in Boolean circuits is a fundamental problem in logic circuit design. We show that there is no $O(3^{(1-ε)n} \text{poly}(s))$ time algorithm, for any $ε> 0$, that detects logic hazards in Boolean circuits of size $s$ on $n$ variables under the assumption that the strong exponential time hypothesis is true. This lower bound holds even when the input circuits are restricted to be formulas of depth four. We also present a polynomial time algorithm for detecting $1$-hazards in DNF (or, $0$-hazards in CNF) formulas. Since $0$-hazards in DNF (or, $1$-hazards i…
We show that the CNF satisfiability problem can be solved $O^*(1.2226^m)$ time, where $m$ is the number of clauses in the formula, improving the known upper bounds $O^*(1.234^m)$ given by Yamamoto 15 years ago and $O^*(1.239^m)$ given by Hirsch 22 years ago. By using an amortized technique and careful case analysis, we successfully avoid the bottlenecks in previous algorithms and get the improvement.
The standard reasoning problem, concept satisfiability, in the basic description logic ALC is PSPACE-complete, and it is EXPTIME-complete in the presence of unrestricted axioms. Several fragments of ALC, notably logics in the FL, EL, and DL-Lite family, have an easier satisfiability problem; sometimes it is even tractable. All these fragments restrict the use of Boolean operators in one way or another. We look at systematic and more general restrictions of the Boolean operators and establish the complexity of the concept satisfiability problem in the presence of axioms. We separate tractable f…
These notes contain, among others, a proof that the average running time of an easy solution to the satisfiability problem for propositional calculus is, under some reasonable assumptions, linear (with constant 2) in the size of the input. Moreover, some suggestions are made about criteria for tractability of complex algorithms. In particular, it is argued that the distribution of probability on the whole input space of an algorithm constitutes an non-negligible factor in estimating whether the algorithm is tractable or not.
The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equivalence relations. We also consider different sets of modal and hybrid operators. We trace the border of decidability and give the precise complexity of most fragments, in particular for all fragments …
Let L be some extension of classical propositional logic. The non-iterated probabilistic logic over L, is the logic PL that is defined by adding non-nested probabilistic operators in the language of L. For example in PL we can express a statement like "the probability of truthfulness of A is at 0.3" where A is a formula of L. The iterated probabilistic logic over L is the logic PPL, where the probabilistic operators may be iterated (nested). For example, in PPL we can express a statement like "this coin is counterfeit with probability 0.6". In this paper we investigate the influence of probabi…
A knowledge base is redundant if it contains parts that can be inferred from the rest of it. We study the problem of checking whether a CNF formula (a set of clauses) is redundant, that is, it contains clauses that can be derived from the other ones. Any CNF formula can be made irredundant by deleting some of its clauses: what results is an irredundant equivalent subset (I.E.S.) We study the complexity of some related problems: verification, checking existence of a I.E.S. with a given size, checking necessary and possible presence of clauses in I.E.S.'s, and uniqueness. We also consider the pr…
Satisfiability solvers are increasingly playing a key role in software verification, with particularly effective use in the analysis of security vulnerabilities. String processing is a key part of many software applications, such as browsers and web servers. These applications are susceptible to attacks through malicious data received over network. Automated tools for analyzing the security of such applications, thus need to reason about strings. For efficiency reasons, it is desirable to have a solver that treats strings as first-class types. In this paper, we present some theories of strings…
We classify the computational complexity of the satisfiability, validity and model-checking problems for propositional independence, inclusion, and team logic. Our main result shows that the satisfiability and validity problems for propositional team logic are complete for alternating exponential-time with polynomially many alternations.
We determine the complexity of several constraint satisfaction problems using the quantum adiabatic algorithm in its simplest implementation. We do so by studying the size dependence of the gap to the first excited state of "typical" instances. We find that at large sizes N, the complexity increases exponentially for all models that we study. We also compare our results against the complexity of the analogous classical algorithm WalkSAT and show that the harder the problem is for the classical algorithm the harder it is also for the quantum adiabatic algorithm.
We present a general method for converting any family of unsatisfiable CNF formulas that is hard for one of the simplest proof systems, tree resolution, into formulas that require large rank in any proof system that manipulates polynomials or polynomial threshold functions of degree at most k (known as Th(k) proofs). Such systems include Lovasz-Schrijver and Cutting Planes proof systems as well as their high degree analogues. These are based on analyzing two new proof systems, denoted by T^cc(k) and R^cc(k). The proof lines of T^cc(k) are arbitrary Boolean functions, each of which can be evalu…
In this paper, we initiate a systematic study of the parametrised complexity in the field of Dependence Logics which finds its origin in the Dependence Logic of Väänänen from 2007. We study a propositional variant of this logic (PDL) and investigate a variety of parametrisations with respect to the central decision problems. The model checking problem (MC) of PDL is NP-complete. The subject of this research is to identify a list of parametrisations (formula-size, treewidth, treedepth, team-size, number of variables) under which MC becomes fixed-parameter tractable. Furthermore, we show that th…
We consider bounded width CNF-formulas where the width is measured by popular graph width measures on graphs associated to CNF-formulas. Such restricted graph classes, in particular those of bounded treewidth, have been extensively studied for their uses in the design of algorithms for various computational problems on CNF-formulas. Here we consider the expressivity of these formulas in the model of clausal encodings with auxiliary variables. We first show that bounding the width for many of the measures from the literature leads to a dramatic loss of expressivity, restricting the formulas to …
Motivated by description logics, we investigate what happens to the complexity of modal satisfiability problems if we only allow formulas built from literals, $\wedge$, $\Diamond$, and $\Box$. Previously, the only known result was that the complexity of the satisfiability problem for K dropped from PSPACE-complete to coNP-complete (Schmidt-Schauss and Smolka, 1991 and Donini et al., 1992). In this paper we show that not all modal logics behave like K. In particular, we show that the complexity of the satisfiability problem with respect to frames in which each world has at least one successor d…
This paper presents a complete algorithmic study of the decision Boolean Satisfiability Problem under the classical computation and quantum computation theories. The paper depicts deterministic and probabilistic algorithms, propositions of their properties and the main result is that the problem has not an efficient algorithm (NP is not P). Novel quantum algorithms and propositions depict that the complexity by quantum computation approach for solving the Boolean Satisfiability Problem or any NP problem is lineal time.
Hybrid logic with binders is an expressive specification language. Its satisfiability problem is undecidable in general. If frames are restricted to N or general linear orders, then satisfiability is known to be decidable, but of non-elementary complexity. In this paper, we consider monotone hybrid logics (i.e., the Boolean connectives are conjunction and disjunction only) over N and general linear orders. We show that the satisfiability problem remains non-elementary over linear orders, but its complexity drops to PSPACE-completeness over N. We categorize the strict fragments arising from dif…
A workflow specification defines a set of steps and the order in which those steps must be executed. Security requirements may impose constraints on which groups of users are permitted to perform subsets of those steps. A workflow specification is said to be satisfiable if there exists an assignment of users to workflow steps that satisfies all the constraints. An algorithm for determining whether such an assignment exists is important, both as a static analysis tool for workflow specifications, and for the construction of run-time reference monitors for workflow management systems. Finding su…
It is well known that modal satisfiability is PSPACE-complete (Ladner 1977). However, the complexity may decrease if we restrict the set of propositional operators used. Note that there exist an infinite number of propositional operators, since a propositional operator is simply a Boolean function. We completely classify the complexity of modal satisfiability for every finite set of propositional operators, i.e., in contrast to previous work, we classify an infinite number of problems. We show that, depending on the set of propositional operators, modal satisfiability is PSPACE-complete, coNP-…
The standard reasoning problem, concept satisfiability, in the basic description logic ALC is PSPACE-complete, and it is EXPTIME-complete in the presence of unrestricted axioms. Several fragments of ALC, notably logics in the FL, EL, and DL-Lite families, have an easier satisfiability problem; sometimes it is even tractable. We classify the complexity of the standard satisfiability problems for all possible Boolean and quantifier fragments of ALC in the presence of general axioms.
The following problem is considered. A Turing machine $M$, that accepts a string of fixed length $t$ as input, runs for a time not exceeding a fixed value $n$ and is guaranteed to produce a binary output, is given. It's required to find a string $X$ such that $M(X) = 1$ effectively in terms of $t$, $n$, the size of the alphabet of $M$ and the number of states of $M$. The problem is close to the well-known Circuit Satisfiability Problem. The difference from Circuit Satisfiability Problem is that when reduced to Circuit Satisfiability Problem, we get circuits with a rich internal structure (in p…
The question of whether the complexity class P is equal to the complexity class NP has been a seemingly intractable problem for over 4 decades. It has been clear that if an algorithm existed that would solve the problems in the NP class in polynomial time then P would equal NP. However, no one has yet been able to create that algorithm or to successfully prove that such an algorithm cannot exist. The algorithm that will be presented in this paper solves the 3-satisfiability or 3-CNF-SAT problem, which has been proven to be NP-complete.
We prove the #P-hardness of the counting problems associated with various satisfiability, graph and combinatorial problems, when restricted to planar instances. These problems include \begin{romannum} \item[{}] {\sc 3Sat, 1-3Sat, 1-Ex3Sat, Minimum Vertex Cover, Minimum Dominating Set, Minimum Feedback Vertex Set, X3C, Partition Into Triangles, and Clique Cover.} \end{romannum} We also prove the {\sf NP}-completeness of the {\sc Ambiguous Satisfiability} problems \cite{Sa80} and the {\sf D$^P$}-completeness (with respect to random polynomial reducibility) of the unique satisfiability problems \…
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 connecti…
In 1978, Schaefer proved his famous dichotomy theorem for generalized satisfiability problems. He defined an infinite number of propositional satisfiability problems (nowadays usually called Boolean constraint satisfaction problems) and showed that all these satisfiability problems are either in P or NP-complete. In recent years, similar results have been obtained for quite a few other problems for Boolean constraints.Almost all of these problems are variations of the satisfiability problem. In this paper, we address a problem that is not a variation of satisfiability, namely, the isomorphism …
Theoretical complexity is a vital subfield of computer science that enables us to mathematically investigate computation and answer many interesting queries about the nature of computational problems. It provides theoretical tools to assess time and space requirements of computations along with assessing the difficultly of problems - classifying them accordingly. It also garners at its core one of the most important problems in mathematics, namely, the $\textbf{P vs. NP}$ millennium problem. In essence, this problem asks whether solution and verification reside on two different levels of diffi…
We investigate the computational complexity of the satisfiability problem of modal inclusion logic. We distinguish two variants of the problem: one for the strict and another one for the lax semantics. Both problems turn out to be EXPTIME-complete on general structures. Finally, we show how for a specific class of structures NEXPTIME-completeness for these problems under strict semantics can be achieved.
We demonstrate that any logical problem can be solved by Bayesian inference. In this approach, the distinction between complexity classes vanishes. The method is illustrated by solving the 3-SAT problem in polynomial time. Beyond this, Bayesian inference could be the background of artificial neural network theory.