In this paper we propose a structural parameter of CNF formulas and use it to identify instances of weighted MaxSAT and #SAT that can be solved in polynomial time. Given a CNF formula we say that a set of clauses is precisely satisfiable if there is some complete assignment satisfying these clauses only. Let the ps-value of the formula be the number of precisely satisfiable sets of clauses. Applying the notion of branch decompositions to CNF formulas and using ps-value as cut function, we define the ps-width of a formula. For a formula given with a decomposition of polynomial ps-width we show dynamic programming algorithms solving weighted MaxSAT and #SAT in polynomial time. Combining with results of 'Belmonte and Vatshelle, Graph classes with structured neighborhoods and algorithmic applications, Theor. Comput. Sci. 511: 54-65 (2013)' we get polynomial-time algorithms solving weighted MaxSAT and #SAT for some classes of structured CNF formulas. For example, we get $O(m^2(m + n)s)$ algorithms for formulas $F$ of $m$ clauses and $n$ variables and size $s$, if $F$ has a linear ordering of the variables and clauses such that for any variable $x$ occurring in clause $C$, if $x$ appears before $C$ then any variable between them also occurs in $C$, and if $C$ appears before $x$ then $x$ occurs also in any clause between them. Note that the class of incidence graphs of such formulas do not have bounded clique-width.
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, …
The natural generalization of the Boolean satisfiability problem to optimization problems is the task of determining the maximum number of clauses that can simultaneously be satisfied in a propositional formula in conjunctive normal form. In the weighted maximum satisfiability problem each clause has a positive weight and one seeks an assignment of maximum weight. The literature almost solely considers the case of positive weights. While the general case of the problem is only restricted slightly by this constraint, many special cases become trivial in the absence of negative weights. In this …
Majority-SAT is the problem of determining whether an input $n$-variable formula in conjunctive normal form (CNF) has at least $2^{n-1}$ satisfying assignments. Majority-SAT and related problems have been studied extensively in various AI communities interested in the complexity of probabilistic planning and inference. Although Majority-SAT has been known to be PP-complete for over 40 years, the complexity of a natural variant has remained open: Majority-$k$SAT, where the input CNF formula is restricted to have clause width at most $k$. We prove that for every $k$, Majority-$k$SAT is in P. In …
NP-Complete problems have an important attribute that if one NP-Complete problem can be solved in polynomial time, all NP-Complete problems will have a polynomial solution. The 3-CNF-SAT problem is a NP-Complete problem and the primary method to solve it checks all values of the truth table. This task is of the Ω(2^n) time order. This paper shows that by changing the viewpoint towards the problem, it is possible to know if a 3-CNF-SAT problem is satisfiable in time O(n^10) or not? In this paper, the value of all clauses are considered as false. With this presumption, any of the values inside t…
We take an algorithmic approach to studying the solution space geometry of relatively sparse random and bounded degree $k$-CNFs for large $k$. In the course of doing so, we establish that with high probability, a random $k$-CNF $Φ$ with $n$ variables and clause density $α= m/n \lesssim 2^{k/6}$ has a giant component of solutions that are connected in a graph where solutions are adjacent if they have Hamming distance $O_k(\log n)$ and that a similar result holds for bounded degree $k$-CNFs at similar densities. We are also able to deduce looseness results for random and bounded degree $k$-CNFs …
A novel parallel algorithm for solving the classical Decision Boolean Satisfiability problem with clauses in conjunctive normal form is depicted. My approach for solving SAT is without using algebra or other computational search strategies such as branch and bound, back-forward, tree representation, etc. The method is based on the special class of SAT problems, Simple SAT (SSAT). The algorithm's design includes parallel execution, object oriented, and short termination as my previous versions but it keep track of the tested unsatisfactory binary values to improve the efficiency and to favor sh…
We introduce the problem of finding a satisfying assignment to a CNF formula that must further belong to a prescribed input subspace. Equivalent formulations of the problem include finding a point outside a union of subspaces (the Union-of-Subspace Avoidance (USA) problem), and finding a common zero of a system of polynomials over $\F_2$ each of which is a product of affine forms. We focus on the case of k-CNF formulas (the k-SUB-SAT problem). Clearly, it is no easier than k-SAT, and might be harder. Indeed, via simple reductions we show NP-hardness for k=2 and W[1]-hardness parameterized by t…
Boolean Satisfiability Problem (SAT) is one of the core problems in computer science. As one of the fundamental NP-complete problems, it can be used - by known reductions - to represent instances of variety of hard decision problems. Additionally, those representations can be passed to a program for finding satisfying assignments to Boolean formulas, for example, to a program called MiniSat. Those programs (called SAT-solvers) have been intensively developed for many years and - despite their worst-case exponential time complexity - are able to solve a multitude of hard practical instances. A …
We give the first efficient algorithm to approximately count the number of solutions in the random $k$-SAT model when the density of the formula scales exponentially with $k$. The best previous counting algorithm for the permissive version of the model was due to Montanari and Shah and was based on the correlation decay method, which works up to densities $(1+o_k(1))\frac{2\log k}{k}$, the Gibbs uniqueness threshold for the model. Instead, our algorithm harnesses a recent technique by Moitra to work for random formulas. The main challenge in our setting is to account for the presence of high-d…
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.
Bonnet et al. (FOCS 2020) introduced the graph invariant twin-width and showed that many NP-hard problems are tractable for graphs of bounded twin-width, generalizing similar results for other width measures, including treewidth and clique-width. In this paper, we investigate the use of twin-width for solving the propositional satisfiability problem (SAT) and propositional model counting. We particularly focus on Bounded-ones Weighted Model Counting (BWMC), which takes as input a CNF formula $F$ along with a bound $k$ and asks for the weighted sum of all models with at most $k$ positive litera…
Learning CNF formulas from uniform random solutions in the local lemma regime
School of Computing and Data Science, The University of Hong Kong（计算与数据科学学院，香港大学）；Department of Computer Science, University of California, Santa Barbara（计算机科学系，加州大学圣芭芭拉分校）；State Key Laboratory for Novel Software Technology, New Cornerstone Science Laboratory, Nanjing University（新型软件技术国家重点实验室，南京大学）
In this paper, we prove that the general CNF satisfiability problem can be solved in $O^*(1.0638^L)$ time, where $L$ is the length of the input CNF-formula (i.e., the total number of literals in the formula), which improves the previous result of $O^*(1.0652^L)$ obtained in 2009. Our algorithm was analyzed by using the measure-and-conquer method. Our improvements are mainly attributed to the following two points: we carefully design branching rules to deal with degree-5 and degree-4 variables to avoid previous bottlenecks; we show that some worst cases will not always happen, and then we can u…
在这项工作中，我们提出并分析了一个简单的随机算法，以找到一个可满足的分配的布尔公式在合取范式（CNF）在每个子句中有最多3个文字。给定n个变量的k-CNF公式phi，{0，1}^n中的alpha满足phi，如果在赋值alpha下恰好满足该子句的一个文字，则phi子句是关键的。Paturi et.等人（Chicago Journal of Theoretical计算机科学1999）提出了一种用于k-SAT的简单随机算法（PPZ），其成功概率随着关键子句的数量（相对于输入公式的固定可满足解）而增加。在这里，我们首先描述另一个简单的随机算法DEL的执行更好，如果关键条款的数量较少（相对于一个固定的可满足的解决方案的输入公式）。随后，我们结合这两个简单的算法，使得组合算法的成功概率是PPZ和DEL在每个输入实例上的成功概率的最大值。我们发现，当出现在一个或多个关键条款中的一个或多个关键条款中的每个变量的条款的平均数量在1和1.9317之间时，组合算法的性能优于PPZ算法。
