Conjunctive Normal Form SAT (Boolean Satisfiability)

From Algorithm Wiki
Revision as of 07:53, 10 April 2023 by Admin (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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
Retrieved from "https://algorithm-wiki-csail-mit-edu.ezproxy.canberra.edu.au/w/index.php?title=Conjunctive_Normal_Form_SAT&oldid=46873"