Conjunctive Normal Form SAT (Boolean Satisfiability)

Description

CNF-SAT restricts the boolean formula to conjunctive normal form (CNF), meaning it is the AND of ORs.

Related Problems

Generalizations: SAT

Subproblem: All-Equal-SAT, k-SAT, XOR-SAT, Horn SAT, MaxSAT

Related: Disjunctive Normal Form SAT, 1-in-3SAT, Monotone 1-in-3SAT, Monotone Not-Exactly-1-in-3SAT, Not-All-Equal 3-SAT (NAE 3SAT), Monotone Not-All-Equal 3-SAT (Monotone NAE 3SAT), k-SAT, 2SAT, 3SAT, 3SAT-5, 4SAT, Monotone 3SAT, XOR-SAT, Horn SAT, Dual-Horn SAT, Renamable Horn, MaxSAT

Parameters

n: number of variables

Table of Algorithms

Currently no algorithms in our database for the given problem.

Reductions TO Problem

Problem	Implication	Year	Citation	Reduction
k-OV	If: to-time: $N^{(k-\epsilon)} poly(m)$ where $m$-dimensional vectors, $k$-OV, $N$ vectors per set Then: from-time: ${2}^{(n-\epsilon')} \poly(m)$ where $\epsilon' = \epsilon/k > {0}$, $n$ variables, $m$ clauses	2005		link
Frechet Distance	If: to-time: $O({2}^{({2}-\epsilon)}$ for any $\epsilon > {0}$ Then: from-time: $O({2}^{({1}-\delta/{2})N}$ where $N$ is s.t there are $n=\tilde{O}({2}^{N/2})$ vertices on each curve	2014	https://people.mpi-inf.mpg.de/~kbringma/paper/2014FOCS.pdf	link
Local Alignment	if: to-time: $N^{2-\epsilon}$ for some $\epsilon > {0}$ on two binary strings of length $N$ then: from-time: ${2}^{(n-\epsilon')}$ for some $\epsilon' > {0}$	2014	https://link.springer.com/chapter/10.1007/978-3-662-43948-7_4	link
Longest Common Substring with don't cares	if: to-time: $N^{2-\epsilon}$ for some $\epsilon > {0}$ then: from-time: ${2}^{(n-\epsilon')}$ for some $\epsilon' > {0}$	2014	https://link.springer.com/chapter/10.1007/978-3-662-43948-7_4	link
Multiple Local Alignment	if: to-time: $N^{k-\epsilon}$ for some $\epsilon > {0}$ on $k$ binary strings of length $n$ with $k$-wise scoring then: from-time: ${2}^{(n-\epsilon')}$ for some $\epsilon' > {0}$	2014	https://link.springer.com/chapter/10.1007/978-3-662-43948-7_4	link
Approximate Diameter	if: to-time: $O(m^{2-\epsilon})$ for some $\epsilon > {0}$ for a $({3}/{2} - \epsilon)$-approximation then: from-time: $O*(({2}-\delta)^n)$ for constant $\delta > {0}$	2013	https://people.csail.mit.edu/virgi/diam.pdf	link
Positive Betweenness Centrality	if: to-time: $O(m^{2-\epsilon})$ for some $\epsilon > {0}$ then: from-time: $O*({2}^{({1}-\delta)n})$ for some $\delta > {0}$	2015	https://epubs.siam.org/doi/10.1137/1.9781611973730.112, Theorem 4.3	link
Approximate Betweenness Centrality	if: to-time: $O(m^{2-\epsilon})$ for some $\epsilon > {0}$ then: from-time: $O*({2}^{({1}-\delta)n})$ for some $\delta > {0}$	2015	https://epubs.siam.org/doi/10.1137/1.9781611973730.112, Corollary 4.2	link
Approximate Reach Centrality	if: to-time: $O(m^{2-\epsilon})$ for some $\epsilon > {0}$ then: from-time: $O*({2}^{({1}-\delta)n})$ for some $\delta > {0}$	2015	https://epubs.siam.org/doi/10.1137/1.9781611973730.112, Corollary 4.2	link
Approximate Reach Centrality	if: to-time: $O(m^{2-\epsilon})$ then: from-time: $O*({2}^{({1}-\epsilon/{2})n})$	2015	https://epubs.siam.org/doi/10.1137/1.9781611973730.112, Theorem 4.4	link
#SSR	if: to-time: $O(m^{1-\epsilon})$ amrotized update and query times on sparse graphs, for any $\epsilon > {0}$, even after arbitrarily long polynomial time preprocessing then: SETH is false	2014	https://ieeexplore.ieee.org/abstract/document/6979028?casa_token=daaoBjrHUa4AAAAA:DCjk_WMWZ5Is6KvGpmS8a2bL9LskvV0P1zEG4U2u-Tm_C8sixu1w65OpTyjml1HEpaikXhtYsg	link
SC2	if: to-time: $O(m^{1-\epsilon})$ amrotized update and query times on sparse graphs, for any $\epsilon > {0}$, even after arbitrarily long polynomial time preprocessing then: SETH is false	2014	https://ieeexplore.ieee.org/abstract/document/6979028?casa_token=daaoBjrHUa4AAAAA:DCjk_WMWZ5Is6KvGpmS8a2bL9LskvV0P1zEG4U2u-Tm_C8sixu1w65OpTyjml1HEpaikXhtYsg	link
Dynamic MaxSCC	if: to-time: $O(m^{1-\epsilon})$ amrotized update and query times on sparse graphs, for any $\epsilon > {0}$, even after arbitrarily long polynomial time preprocessing then: SETH is false	2014	https://ieeexplore.ieee.org/abstract/document/6979028?casa_token=daaoBjrHUa4AAAAA:DCjk_WMWZ5Is6KvGpmS8a2bL9LskvV0P1zEG4U2u-Tm_C8sixu1w65OpTyjml1HEpaikXhtYsg	link
Dynamic Connected Subgraph	if: to-time: $O(m^{1-\epsilon})$ amrotized update and query times on sparse graphs, for any $\epsilon > {0}$, even after arbitrarily long polynomial time preprocessing then: SETH is false	2014	https://ieeexplore.ieee.org/abstract/document/6979028?casa_token=daaoBjrHUa4AAAAA:DCjk_WMWZ5Is6KvGpmS8a2bL9LskvV0P1zEG4U2u-Tm_C8sixu1w65OpTyjml1HEpaikXhtYsg	link
Dynamic 4/3-Diameter	if: to-time: $O(m^{2-\epsilon})$ amrotized update and query times, for any $\epsilon > {0}$, even after arbitrarily long polynomial time preprocessing then: SETH is false	2014	https://ieeexplore.ieee.org/abstract/document/6979028?casa_token=daaoBjrHUa4AAAAA:DCjk_WMWZ5Is6KvGpmS8a2bL9LskvV0P1zEG4U2u-Tm_C8sixu1w65OpTyjml1HEpaikXhtYsg	link
Dynamic ST-Reach	if: to-time: $O(m^{2-\epsilon})$ amrotized update and query times, for any $\epsilon > {0}$, even after arbitrarily long polynomial time preprocessing then: SETH is false	2014	https://ieeexplore.ieee.org/abstract/document/6979028?casa_token=daaoBjrHUa4AAAAA:DCjk_WMWZ5Is6KvGpmS8a2bL9LskvV0P1zEG4U2u-Tm_C8sixu1w65OpTyjml1HEpaikXhtYsg	link
dynamic st-Maximum Flow	assume: SETH then: there is no algorithm for solving incremental (or decremental) st-max-flow on a weighted and directed graph with $n$ nodes and $\tilde{O}(n)$ edges with amortized time $O(m^{1-\epsilon})$ per operation for any $\epsilon > {0}$	2016	https://arxiv.org/abs/1602.06705	link
sensitive incremental #SSR	assume: SETH then: let $\epsilon > {0}$, $t \in \mathbb{N}$, there exists no algorithm for target with preprocessing time $O(n^t)$, update time $u(n)$ and query time $q(n)$, such that $max\{u(n),q(n)\}=O(n^{1-\epsilon})$ with constant sensitivity $K(\epsilon,t)$	2017	https://arxiv.org/pdf/1703.01638.pdf	link
constant sensitivity (4/3)-approximate incremental diameter	assume: SETH then: let $\epsilon > {0}$, $t \in \mathbb{N}$, there exists no algorithm for target with preprocessing time $O(n^t)$, update time $u(n)$ and query time $q(n)$, such that $max\{u(n),q(n)\}=O(n^{1-\epsilon})$ with constant sensitivity $K(\epsilon,t)$	2017	https://arxiv.org/pdf/1703.01638.pdf	link
sensitive incremental ST-Reach	assume: SETH then: let $\epsilon > {0}$, $t \in \mathbb{N}$, there exists no algorithm for target with preprocessing time $O(n^t)$, update time $u(n)$ and query time $q(n)$, such that $max\{u(n),q(n)\}=O(n^{1-\epsilon})$ with constant sensitivity $K(\epsilon,t)$	2017	https://arxiv.org/pdf/1703.01638.pdf	link