Conjunctive Normal Form SAT (Boolean Satisfiability)
Jump to navigation
Jump to search
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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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.ezproxy.canberra.edu.au/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 |