From 9d0a2ae355e23f0d0312b12339d669b3dd4853ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Jul 2025 17:40:43 -0700 Subject: [PATCH] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index df7107c3d..88b521e96 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -17,35 +17,38 @@ and possibly * Lookahead solvers: * lookahead in the smt directory performs a simplistic lookahead search using unit propagation. - * lookahead in the sat directory uses custom lookahead solver. - They both proxy on a cost model where the most useful variable to branch on is the one that _minimizes_ the set of new clauses maximally + * lookahead in the sat directory uses custom lookahead solver based on MARCH. March is described in Handbook of SAT and Knuth volumne 4. + * They both proxy on a cost model where the most useful variable to branch on is the one that _minimizes_ the set of new clauses maximally through unit propagation. In other words, if a literal _p_ is set to true, and _p_ occurs in clause $\neg p \vee q \vee r$, then it results in reducing the clause from size 3 to 2 (because $\neg p$ will be false after propagating _p_). + * Selected references: SAT handbook, Knuth Volumne 4, Marijn's March solver on github, [implementation of march in z3](https://github.com/Z3Prover/z3/blob/master/src/sat/sat_lookahead.cpp) * VSIDS: * As referenced in Matteo and Antti's solvers. * Variable activity is a proxy for how useful it is to case split on a variable during search. Variables with a higher VSIDS are split first. * VSIDS is updated dynamically during search. It was introduced in the paper with Moscovitz, Malik, et al in early 2000s. A good overview is in Armin's tutorial slides (also in my overview of SMT). * VSIDS does not keep track of variable phases (if the variable was set to true or false). + * Selected refernces [DAC 2001](https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf) and [Biere Tutorial](https://alexeyignatiev.github.io/ssa-school-2019/slides/ab-satsmtar19-slides.pdf) * Proof prefix: * Collect the literals that occur in learned clauses. Count their occurrences based on polarity. This gets tracked in a weighted score. * The weight function can be formulated to take into account clause sizes. * The score assignment may also decay similar to VSIDS. * We could also use a doubly linked list for literals used in conflicts and keep reinsert literals into the list when they are used. This would be a "Variable move to front" (VMTF) variant. + * Selected references: [Battleman et al](https://www.cs.cmu.edu/~mheule/publications/proofix-SAT25.pdf) * From local search: * Note also that local search solvers can be used to assign variable branch priorities. * We are not going to directly run a local search solver in the mix up front, but let us consider this heuristic for completeness. * The heuristic is documented in Biere and Cai's journal paper on integrating local search for CDCL. * Roughly, it considers clauses that move from the UNSAT set to the SAT set of clauses. It then keeps track of the literals involved. + * Selected references: [Cai et al](https://www.jair.org/index.php/jair/article/download/13666/26833/) * Assignment trails: * We could also consider the assignments to variables during search. * Variables that are always assigned to the same truth value could be considered to be safe to assign that truth value. * The cubes resulting from such variables might be a direction towards finding satisfying solutions. + * Selected references: [Alex and Vadim](https://link.springer.com/chapter/10.1007/978-3-319-94144-8_7) and most recently [Robin et al](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9). ## Algorithms - - This section considers various possible algorithms. In the following, $F$ refers to the original goal, $T$ is the number of CPU cores or CPU threads.