0
$\begingroup$

Can any SAT problem be converted into one with only affine formulas?

Handbook of Satisfiability p. 672:

Affine formulas. A linear equation over the two-element field is an expression of the form $x_1 ⊕ … ⊕ x_k = δ$ where $⊕$ denotes the sum modulo $2$ and $δ$ stands for $0$ or $1$. Such an equation can be expressed as a CNF formula consisting of $2k−1$ clauses of length $k$. An affine formula is a conjunction of linear equations over the two-element field [$\mathbf{Z}_2=\langle Bool , +, ∧, 0, 1\rangle$]. Using Gaussian elimination, we can test satisfiability of affine formulas in polynomial time.

In other words: Can any SAT problem be converted to a system of linear equations over $\mathbf{Z}_2$?

Improve this question
$\endgroup$
6
  • $\begingroup$ Please edit your question to define what you mean by "converted". What relationship do you require between the original SAT problem and the system of linear equations? Equisatisfiable? Equivalent? Do you require conversion to be implemented by a polynomial-time algorithm or is exponential-time fine? $\endgroup$
    – D.W. ♦
    Commented Sep 12, 2023 at 1:16
  • $\begingroup$ No, not every SAT can. Equations in product-of-XORs form can, though. Most problems cannot be turned into product-of-XORs. For example, Bitcoin mining can't. If it could be, they wouldn't have used that algorithm. I mention Bitcoin mining because if you can efficiently solve SAT you can make yourself a billionaire. $\endgroup$
    – Criticizing Israel not allowed
    Commented Sep 12, 2023 at 8:23
  • $\begingroup$ @user253751 Thank you. Perhaps you could turn your comment into a full answer. $\endgroup$
    – Geremia
    Commented Sep 12, 2023 at 23:05
  • $\begingroup$ @D.W. Equivalent. And I'm not concerned with the runtime of the transformation algorithm. $\endgroup$
    – Geremia
    Commented Sep 12, 2023 at 23:10
  • $\begingroup$ Please edit your question to state that in the question. Please don't put clarifications in the comments. Make sure the question is clear and reads well for someone who encounters the question for the first time. We don't want people to have to read the comments to understand what is being asked. Thank you. $\endgroup$
    – D.W. ♦
    Commented Sep 15, 2023 at 0:34

2 Answers 2

Reset to default
3
$\begingroup$

Equivalence: Not every SAT instance can be expressed as a system of linear equations. For instance, $x_1 \lor x_2$ cannot be expressed as a system of linear equations.

(Why not? Systems of linear equations have the following property: if $x_1,x_2$ is a solution to the system, and $y_1,y_2$ is a solution, and $z_1,z_2$ is a solution, then $x_1 \oplus y_1 \oplus z_1,x_1 \oplus y_2 \oplus z_2$ is also a solution. Yet it is easy to verify that True,False is a solution to the SAT instance $x_1 \lor x_2$, and False,True is a solution, and True,True is a solution; yet the xor of these three solutions is False,False, which is not a solution. Therefore, the satisfying assignments to $x_1 \oplus x_2$ cannot be represented as a solution to a system of linear equations.)

(See also https://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem, https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#XOR-satisfiability.)

Equisatisfiability: Every SAT instance is either satisfiable or not satisfiable, i.e., is equisatisfiable to either True or False. Both of those can be expressed as systems of linear equations. However, figuring out which one is correct is not believed to be possible in polynomial time (specifically, not unless P=NP).

Improve this answer
$\endgroup$
2
  • $\begingroup$ Please explain why "$x_1 \lor x_2$ cannot be expressed as a system of linear equations". Thanks. $\endgroup$
    – Geremia
    Commented Sep 14, 2023 at 0:42
  • $\begingroup$ @Geremia, I've revised my answer with an explanation. $\endgroup$
    – D.W. ♦
    Commented Sep 14, 2023 at 5:25
0
$\begingroup$

No, unless P=NP.

Cook-Levin showed SAT is an NP-complete problem. Solving a system of linear equations is a polynomial time problem. Also, Schaefer's Dichotomy Theorem says that SAT problems can divided into P or NP-complete classes.

cf. Introduction to Mathematics of Satisfiability

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.