What are those deterministic algorithms for k-SAT that are not derandomization of random algorithms like PPSZ and Schöning's local search?

Question

I am doing a survey on k-SAT where time complexity is in terms of n, i.e. the number of variables in a formula. As for the fast algorithms for k-SAT, we see biased-PPSZ, PPSZ, Schöning's local search, algorithms which combine PPSZ and Schöning's local search, algorithms which derandomize PPSZ or Schöning's local search.

There are many papers which are discussing improvement and property of PPSZ. However, where are other deterministic algorithms going? Is there no future for every deterministic algorithm which is not a derandomization of PPSZ or Schöning's local search or their improvement,combination?

There exists deterministic fast branching algorithms which are not derandomization from some randomized algorthms for k-SAT where time complexity is in terms of m and l, i.e. the number of clauses in a formula and the length of a formula. And there is a branching algorithm, and in the early papers which discuss k-SAT in terms of n, there is also algorithm using branching algorithm to obtain a speed which is from Burkhard Monien and Ewald Speckenmeyer. For 2-SAT, there is linear time deterministic algorithm based on strongly connected components of a contructed graph.

After Hertli reveals that unique-SAT bounds for PPSZ hold in general, work turns from derandomizing and improving Schöning's local search to derandomize PPSZ and improve that. Are there any possibilities for those deterministic algorithms without derandomization like some branching algorithms? What if some techniques like measure and conquer are contributed to k-SAT? No matter how, it must be admitted that PPSZ and Schöning's local search are both simple and efficient.

Papers I mention are as follows.

1. schöning, A Probabilistic Algorithm for k-SAT and Constraint Satisfaction k Problems
2. Evgeny Dantsin, Andreas Goerdt, Edward A Hirsch, Ravi Kannan, Jon Kleinberg, Christos Papadimitriou, Prabhakar Raghavan, and Uwe Sch¨oning. A deterministic (2-2/(k+1))n algorithm for k-sat based on local search. Theoretical Computer Science, 289(1):69–83, 2002.
3. S. Cliff Liu, Simpler Partial Derandomization of PPSZ for k-SAT
4. Daniel Rolf. Derandomization of PPSZ for unique- k-sat. In 8th International Conference on Theory and Applications ofSatisfiability Testing, SAT 2005, pages 216–225, 2005.
5. S. Cliff Liu, Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT∗
6. Robin A. Moser and Dominik Scheder, A full derandomization of schöning’s k-sat algorithm. In 43rd Annual ACMSymposium on Theory ofComputing, STOC 2011, pages 245–252, 2011.
7. Hertli, 3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General
8. Dominik Scheder and John P. Steinberger, PPSZ for General k-SAT – Making Hertli’s Analysis Simpler and 3-SAT Faster∗
9. Pavel Pudlák, Dominik Scheder, and Navid Talebanfard, Tighter Hard Instances for PPSZ
10. Burkhard Monien and Ewald Speckenmeyer. 1985. Solving satisfiability in less than 2n steps. Discrete Applied Mathematics 10, 3 (1985), 287–295.
11. Jianer Chen and Yang Liu, An Improved SAT Algorithm in Terms of Formula Length
12. Bengt ASPVALL, Michael F. PLASS and Robert Endre TARJAN, A LINEAR-TIME ALGORITHM FOR TESTING THE TRUTH OF CERTAIN QUANTIFIED BOOLEAN FORMULAS
13. Timon Hertli. 2014. Breaking the PPSZ Barrier for Unique 3-SAT. In Proc. of41st ICALP I. 600–611.
14. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. 1999. Satisfiability Coding Lemma. Chicago J. Theor. Comput. Sci. (1999).
15. Tong Qin and Osamu Watanabe. 2018. An Improvement of the Algorithm of Hertli for the Unique 3SAT Problem. In International Workshop on Algorithms and Computation. Springer, 93–105.
16. Thomas Hofmeister, Uwe Sch¨oning, Rainer Schuler, and Osamu Watanabe. A probabilistic 3sat algorithm further improved. In 19th Annual Symposium on Theoretical Aspects ofComputer Science, STACS 2002, pages 192–202. Springer, 2002.
17. Improving PPSZ for 3-SAT using Critical Variables

Answer 1

If I may interpret your question as a reference request: Donald Knuth recently finished the part of TAOCP that deals with satisfiability:

Donald E. Knuth, The Art of Computer Programming, Volume 4 Fascicle 6, Satisfiability (2015), xiii+310pp. ISBN 978-0-13-439760-3.

Although I did not work through it yet (no pun intended), it is well known that Don Knuth usually puts a clear emphasis on the structure of the different algorithmic approaches, and he gives a very detailed account on the history of ideas. My bet is that you'll find the answer to your question in the fascicle. (Maybe someone else who is more knowledgeable about SAT can give a less indirect answer 😉)

Answer 2

@Hermann Gruber Thank Hermann Gruber for providing extra materials so much.

The gap between SAT solvers for theory and for practice is large, and in some word, these two fields are nearly distinct.

For those SAT solvers for practice, there are an abundance of algorithms with benign performance on different types of instances.

Among them there are many algorithms, which meet the condition "not derandomization of random algorithms like PPSZ and Schöning's local search" and "deterministic algorithms".

Like:

1. Satisfiability by backtracking

2. Satisfiability by watching

3. Satisfiability by CDCL

4. Satisfiability by cyclic DPLL

5. Satisfiability by clause learning

6. Satisfiability by DPLL with lookahead

7. Survey propagation

8. lookahead for Satisfiability by DPLL

9. double lookahead for Satisfiability by DPLL

Such algorithms derive from different ideas. Generally speaking, they are based majorly on experiments rather than based majorly on theory, so if you want to promote algorithms like PPSZ and Schöning's local search by refering to these practical algorithms. It might be a bit challenging.

SAT solvers for theory progress slower than those for practice, there could be much work to do :) .