# On theoretical aproaches for solving $\mathsf{SAT}$ in special cases

In what cases $$\mathsf{SAT}$$ can be solved in polynomial time?

I know two cases: $$2$$-$$\mathsf{SAT}$$ and Horn-$$\mathsf{SAT}$$.

Question 1: Is there a reference with algorithms for solving $$\mathsf{SAT}$$ effectively in some other cases?

I think that it is important to understand in what case $$\mathsf{SAT}$$ can be solved effectively. It can be related to the problem of understanding of effectivity of $$\mathsf{SAT}$$-solvers. And this is why I am surprised why there are small papers about this theme (it would be nice if I am wrong).

In fact there is a simple method for generating examples when $$\mathsf{SAT}$$ can be solved effectively: Consider some $$\mathsf{L}\in\mathsf{P}$$. For every $$x$$ there exists $$\mathsf{CNF}$$ $$\phi_x$$ such that $$x\in\mathsf{L}\iff\phi_x$$ is satisfiable. So, for $$\mathsf{CNF}$$ of kind $$\phi_x$$ there exists a polynomial algorithm for $$\mathsf{SAT}$$.

Example: Consider $$\mathsf{L}$$ to be $$2$$-$$\mathsf{COLORING}$$. This problem is reduced to $$2$$-$$\mathsf{SAT}$$ problem.

Question 2: Are there any other examples when a problem from $$\mathsf{P}$$ can be reduced to $$\mathsf{CNF}$$ of some adequate form (i.e. it is possible to analyse it and understand why it can be solved in polynomial time)?

• I am not sure if this answers your question, because I am not sure exactly what you are asking, but maybe at least it helps en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem Sep 23, 2019 at 3:42
• I think you'd need a better formulation of the problem. There's an infinite number of P classes. Consider for instance the class fo formulas with no negative literals, those can be solved in constant time (always satisfiable). BTW isn't 2-coloring 2SAT? Sep 23, 2019 at 14:25
• I agree with Mikolas that the formulation of the problem is not yet good enough. One thing that pops to my mind by reading your question is the problem of gate detection, a preprocessing technique of CNF formula when one tries to detect the encoding of constraints, e.g. finding that a bunch of clauses expresses a XOR constraint on a subset of variables.
– holf
Sep 23, 2019 at 18:09
• Also XOR-SAT (linear algebra over F2), RenamableHornSAT (reduces to HornSAT, but uses 2SAT to do the reduction :)), counting planar-3-NAE-SAT (using Valiant's holographic reductions. Curious if when you encode linear algebra over F_p into SAT whether you can tell just from the structure of the SAT instance that it's in P... Sep 26, 2019 at 22:38

Concerning Question 1, there have mainly been two lines of work to find tractable restrictions of SAT.

The first one that you are already familiar with is to restrict the types of the clauses that you are allowed to use. For example, in 2-SAT, you are only allowed to use size two clauses. In Horn-SAT, you only allow Horn clauses etc. The tractable restrictions for SAT have been completely classified by Schaefer in 1978  in his celebrated dichotomy Theorem. The result is a dichotomy in the sense that Schaefer showed that the restriction gives you either a problem in P or an NP-complete problem. It has later been generalized to the problem of counting the satisfying assignments  or to the problem of enumerating them .

Some of these restrictions indeed lead to better performances of SAT solvers. For example, on a 2-SAT instance, unit propagation will naturally solve the instance in polynomial time and one can observe a similar behavior for Horn clauses. However SAT solvers rarely try to detect if the input is of such a form as it would be too costly to scan all clauses (for hardcore SAT-solver people, linear time is already too slow ;)). So for example, affine formulas will often not be detected (CryptoMiniSat may be an exception here).

The second line of research is to look for tractable instances by trying to uncover some structure in the way the variables interact with the clauses. For example, given a CNF formula, you can look at its incidence graph: it is a bipartite graph whose vertices are the variables and the clauses of the formula and you have an edge between a clause $$C$$ and a variable $$x$$ if $$x$$ or $$\neg x$$ is in $$C$$. Now, if this graph is a tree, you can solve SAT in polynomial time by doing some dynamic programming on the tree.

Many results extend this observation and most of them are interested in the parametrized complexity of SAT. For example, a well-known parameter of graphs is the treewidth, an integer that intuitively measures how far a graph is from being a tree. Now, if the incidence graph from above has treewdith $$k$$, we know algorithms to solve SAT in time $$2^{O(k)}\mathsf{size}(F)$$, that is, a linear time algorithm if the treewidth is bounded. An early and good survey of these results have been written by Szeider in 2003 . The earliest result of this kind for SAT I am aware of is a paper by Dantsin  where he apparently shows the tractability of SAT on bounded branch width graphs (the paper is in Russian and I have never read it but I trust Alekhnovich and Razborov  which improved the result in 2002). Many things have been understood since, for more general parameters and for more general problems (#SAT for example). I am shamelessly citing my thesis here as it contains a whole chapter reviewing most recent improvements on the question since then .

The idea of restricting the structure of the input through some associated graph has however been transpiring in computer science in many other domains as early as the 80's. See for example the Yannakakis algorithm for conjunctive queries in databases .

Now these tractable instances of SAT do not explain the good performances of SAT-solvers at all. Most of the algorithms used to solve these instances are not directly related to the way SAT-solvers work. But for more complex problem such as #SAT, the links between the theoretical algorithms and the way solvers work in practice is much stronger.

Some work has been done to understand the performances of SAT solvers by analyzing the structure of the formula (by detecting communities for example) but I do not know the literature well enough and let someone more competent than me answer this. All I can say is that it is not really related to the fact that the input belongs to some tractable instance. What you need is good heuristics to quickly converge to one solution. When there is no solution, then proof complexity is also a way of understanding the performances of a SAT-solver as it constructs a refutation of the formula while solving it. Thus, if no small refutation exists, then you can derive a lower bound on the runtime of the solver. But again, this is not completely enough to explain the performances of the SAT solver.

Concerning Question 2, I am not aware of any problem that have been discovered to be in P by reducting to a tractable class of SAT as usually, it is easier to program an algorithm than to encode it into a restricted formula. Moreover one generally prefers direct algorithms because they give more insights on the problem. However, a recent paper by Lampis, Mengel and Mitsou  shows the tractability of many parametrized problems by reducing them to SAT with bounded treewidth (which is known to be tractable). In this case, it is indeed usually simpler to writer the reduction instead of redoing complex dynamic programming algorithms again.

# References

 Schaefer, Thomas J. (1978). "The Complexity of Satisfiability Problems". STOC 1978 https://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem

 Creignou, Nadia, and Miki Hermann. "Complexity of generalized satisfiability counting problems." Information and computation 125.1 (1996): 1-12.

 Creignou, Nadia, and J-J. Hébrard. "On generating all solutions of generalized satisfiability problems." RAIRO-Theoretical Informatics and Applications 31.6 (1997): 499-511.

 Szeider, Stefan. "On fixed-parameter tractable parameterizations of SAT." International Conference on Theory and Applications of Satisfiability Testing. Springer, Berlin, Heidelberg, 2003.

 E. Dantsin. Parameters defining the time of tautology recogni- tion by the splitting method. Semiotics and information science, 12:8–17, 1979.

 Alekhnovich, Michael, and Alexander A. Razborov. "Satisfiability, branch-width and Tseitin tautologies." The 43rd Annual IEEE Symposium on Foundations of Computer Science, 2002. Proceedings.. IEEE, 2002.

 Yannakakis, Mihalis. "Algorithms for acyclic database schemes." VLDB. Vol. 81. 1981.

 Capelli, Florent. Structural restriction of CNF-formulas: application to model counting and knowledge compilation, Thèse de Doctorat, Université Paris-Diderot, 2016.

 Lampis, Michael, Stefan Mengel, and Valia Mitsou. "QBF as an Alternative to Courcelle’s Theorem." International Conference on Theory and Applications of Satisfiability Testing. Springer, Cham, 2018.