arXiv 0806.11482008-06cs.DM

Unsatisfiable CNF Formulas need many Conflicts

Dominik Scheder, Philipp Zumstein

备注：: new version; added an upper bound on the number of conflicts

英文摘要：

A pair of clauses in a CNF formula constitutes a conflict if there is a variable that occurs positively in one clause and negatively in the other. A CNF formula without any conflicts is satisfiable. The Lovasz Local Lemma implies that a k-CNF formula is satisfiable if each clause conflicts with at most 2^k/e-1 clauses. It does not, however, give any good bound on how many conflicts an unsatisfiable formula has globally. We show here that every unsatisfiable k-CNF formula requires 2.69^k conflicts and there exist unsatisfiable k-CNF formulas with 3.51^k conflicts.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Unsatisfiable Linear CNF Formulas Are Large and Complex

We call a CNF formula linear if any two clauses have at most one variable in common. We show that there exist unsatisfiable linear k-CNF formulas with at most 4k^2 4^k clauses, and on the other hand, any linear k-CNF formula with at most 4^k/(8e^2k^2) clauses is satisfiable. The upper bound uses probabilistic means, and we have no explicit construction coming even close to it. One reason for this is that unsatisfiable linear formulas exhibit a more complex structure than general (non-linear) formulas: First, any treelike resolution refutation of any unsatisfiable linear k-CNF formula has size …

2010-10-28cs.DM

Unsatisfiable (k,(4*2^k/k))-CNF formulas

A boolean formula in a conjuctive normal form is called a (k,s)-formula if every clause contains exactly k variables and every variable occurs in at most s clauses. We prove the existence of a (k, 4 * (2^k/k))-CNF formula which is unsatisfiable.

2008-10-10cs.DMcs.GT

Unsatisfiable Linear k-CNFs Exist, for every k

We call a CNF formula linear if any two clauses have at most one variable in common. Let Linear k-SAT be the problem of deciding whether a given linear k-CNF formula is satisfiable. Here, a k-CNF formula is a CNF formula in which every clause has size exactly k. It was known that for k >= 3, Linear k-SAT is NP-complete if and only if an unsatisfiable linear k-CNF formula exists, and that they do exist for k >= 4. We prove that unsatisfiable linear k-CNF formulas exist for every k. Let f(k) be the minimum number of clauses in an unsatisfiable linear k-CNF formula. We show that f(k) is Omega(k2^…

2007-08-17cs.CCcs.DMcs.LO

Satisfiability Thresholds for k-CNF Formula with Bounded Variable Intersections

We determine the thresholds for the number of variables, number of clauses, number of clause intersection pairs and the maximum clause degree of a k-CNF formula that guarantees satisfiability under the assumption that every two clauses share at most $α$ variables. More formally, we call these formulas $α$-intersecting and define, for example, a threshold $μ_i(k,α)$ for the number of clause intersection pairs $i$, such that every $α$-intersecting k-CNF formula in which at most $μ_i(k,α)$ pairs of clauses share a variable is satisfiable and there exists an unsatisfiable $α$-intersecting k-CNF fo…

2010-06-15cs.DM

具有有界文字出现次数的小规模不可满足 $k$-CNF 公式

Small unsatisfiable $k$-CNFs with bounded literal occurrence

本文研究了有界出现次数的 $k$-CNF 子类中最小不可满足公式，结合理论论证与基于 SMS 的对称性破缺穷举搜索，确定了 3-CNF 子类的最小规模并改进了 4-CNF 的已知结果，为 MaxSAT 不可近似性提供了更强依据。

2024-07-19cs.CCcs.DMcs.LO

The complete set of minimal simple graphs that support unsatisfiable 2-CNFs

A propositional logic sentence in conjunctive normal form that has clauses of length two (a 2-CNF) can be associated with a multigraph in which the vertices correspond to the variables and edges to clauses. We first show that every such sentence that has been reduced, that is, which is unchanged under application of certain tautologies, is equisatisfiable to a 2-CNF whose associated multigraph is, in fact, a simple graph. Our main result is a complete characterization of graphs that can support unsatisfiable 2-CNF sentences. We show that a simple graph can support an unsatisfiable reduced 2-CN…

2019-03-16cs.DMmath.COmath.LO

更多相关论文收起更多论文

A new upper bound for 3-SAT

We show that a randomly chosen 3-CNF formula over n variables with clauses-to-variables ratio at least 4.4898 is, as n grows large, asymptotically almost surely unsatisfiable. The previous best such bound, due to Dubois in 1999, was 4.506. The first such bound, independently discovered by many groups of researchers since 1983, was 5.19. Several decreasing values between 5.19 and 4.506 were published in the years between. The probabilistic techniques we use for the proof are, we believe, of independent interest.

2008-07-23cs.DM

The Local Lemma is asymptotically tight for SAT

The Local Lemma is a fundamental tool of probabilistic combinatorics and theoretical computer science, yet there are hardly any natural problems known where it provides an asymptotically tight answer. The main theme of our paper is to identify several of these problems, among them a couple of widely studied extremal functions related to certain restricted versions of the k-SAT problem, where the Local Lemma does give essentially optimal answers. As our main contribution, we construct unsatisfiable k-CNF formulas where every clause has k distinct literals and every variable appears in at most (…

2016-04-19cs.CCcs.DMmath.CO

A novel weighting scheme for random $k$-SAT

Consider a random $k$-CNF formula $F_{k}(n, rn)$ with $n$ variables and $rn$ clauses. For every truth assignment $σ\in \{0, 1\}^{n}$ and every clause $c=\ell_{1}\vee\cdots\vee\ell_{k}$, let $d=d(σ, c)$ be the number of satisfied literal occurrences in $c$ under $σ$. For fixed $β>-1$ and $λ>0$, we take $ω(σ, c)=0$, if $d=0$; $ω(σ, c)=λ(1+β)$, if $d=1$ and $ω(σ, c)=λ^{d}$, if $d>1$. Applying the above weighting scheme, we get that if $F_{k}(n, rn)$ is unsatisfiable with probability tending to one as $n\rightarrow\infty$, then $r\geq2.83, 8.09, 18.91, 40.81, 84.87$ for $k=3, 4, 5, 6$ and $7,$ res…

2013-10-16cs.DM

A New Lower Bound on the Maximum Number of Satisfied Clauses in Max-SAT and its Algorithmic Applications

A pair of unit clauses is called conflicting if it is of the form $(x)$, $(\bar{x})$. A CNF formula is unit-conflict free (UCF) if it contains no pair of conflicting unit clauses. Lieberherr and Specker (J. ACM 28, 1981) showed that for each UCF CNF formula with $m$ clauses we can simultaneously satisfy at least $\pp m$ clauses, where $\pp =(\sqrt{5}-1)/2$. We improve the Lieberherr-Specker bound by showing that for each UCF CNF formula $F$ with $m$ clauses we can find, in polynomial time, a subformula $F'$ with $m'$ clauses such that we can simultaneously satisfy at least $\pp m+(1-\pp)m'+(2-…

2011-07-08cs.DMcs.DS