Skip to main content
deleted 4 characters in body
Source Link
orlp
  • 13.9k
  • 1
  • 26
  • 41

Suppose that you have a CNF formula $x$ with input size $n$, and that you can solve $\text{SAT}$ in $O(n^c)$ time for some constant $c$.

We construct a new formula $y$. For each clause $l_i$ in $x$, with variablesterms $v_{i,k}$, add a new variable $t_i$ and the CNF clauses $\bigwedge_i(\neg t_i \vee l_i)$ and $ \bigwedge_{i,k} (t_i \vee \neg v_{i,k})$.

Now this formula is only satisfiable if $t_i$ is assigned a truth value equal to $l_i$, and our input size is bounded by linear function of the original size. We then add a "at least $k$ out of $n$" constraint to this formula on the $t$ variables. This also adds a polynomial number of clauses. Now the formula is only satisfiable if at least $k$ clauses of the original formula are satisfiable.

Now we can simply solve $\log_2(n)$ instances of the above formula, doing a binary search with $k$ to find the maximal number of clauses that are satisfiable simultaneously.

Suppose that you have a CNF formula $x$ with input size $n$, and that you can solve $\text{SAT}$ in $O(n^c)$ time for some constant $c$.

We construct a new formula $y$. For each clause $l_i$ in $x$, with variables $v_{i,k}$, add a new variable $t_i$ and the CNF clauses $\bigwedge_i(\neg t_i \vee l_i)$ and $ \bigwedge_{i,k} (t_i \vee \neg v_{i,k})$.

Now this formula is only satisfiable if $t_i$ is assigned a truth value equal to $l_i$, and our input size is bounded by linear function of the original size. We then add a "at least $k$ out of $n$" constraint to this formula on the $t$ variables. This also adds a polynomial number of clauses. Now the formula is only satisfiable if at least $k$ clauses of the original formula are satisfiable.

Now we can simply solve $\log_2(n)$ instances of the above formula, doing a binary search with $k$ to find the maximal number of clauses that are satisfiable simultaneously.

Suppose that you have a CNF formula $x$ with input size $n$, and that you can solve $\text{SAT}$ in $O(n^c)$ time for some constant $c$.

We construct a new formula $y$. For each clause $l_i$ in $x$, with terms $v_{i,k}$, add a new variable $t_i$ and the CNF clauses $\bigwedge_i(\neg t_i \vee l_i)$ and $ \bigwedge_{i,k} (t_i \vee \neg v_{i,k})$.

Now this formula is only satisfiable if $t_i$ is assigned a truth value equal to $l_i$, and our input size is bounded by linear function of the original size. We then add a "at least $k$ out of $n$" constraint to this formula on the $t$ variables. This also adds a polynomial number of clauses. Now the formula is only satisfiable if at least $k$ clauses of the original formula are satisfiable.

Now we can simply solve $\log_2(n)$ instances of the above formula, doing a binary search with $k$ to find the maximal number of clauses that are satisfiable simultaneously.

Source Link
orlp
  • 13.9k
  • 1
  • 26
  • 41

Suppose that you have a CNF formula $x$ with input size $n$, and that you can solve $\text{SAT}$ in $O(n^c)$ time for some constant $c$.

We construct a new formula $y$. For each clause $l_i$ in $x$, with variables $v_{i,k}$, add a new variable $t_i$ and the CNF clauses $\bigwedge_i(\neg t_i \vee l_i)$ and $ \bigwedge_{i,k} (t_i \vee \neg v_{i,k})$.

Now this formula is only satisfiable if $t_i$ is assigned a truth value equal to $l_i$, and our input size is bounded by linear function of the original size. We then add a "at least $k$ out of $n$" constraint to this formula on the $t$ variables. This also adds a polynomial number of clauses. Now the formula is only satisfiable if at least $k$ clauses of the original formula are satisfiable.

Now we can simply solve $\log_2(n)$ instances of the above formula, doing a binary search with $k$ to find the maximal number of clauses that are satisfiable simultaneously.