wiki_research

commit a33a3e82a61b42f28dd4a0ab27a49484629e76cc
parent 3c9093866befb02f559941f91f6d0103ff868112
Author: Antoine Amarilli <a3nm@a3nm.net>
Date:   Mon, 15 Jun 2026 16:41:28 +0200

commit with codex

Diffstat:
dpll
 | 
6
+++++-
knowledge_compilation_classes
 | 
2
+-
knowledge_compilation_query
 | 
2
++
literal
 | 
2
++

4 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/dpll b/dpll
@@ -10,6 +10,10 @@ https://en.wikipedia.org/wiki/DPLL_algorithm
 - if there is a [literal_pure] aka one that occurs with only one polarity, insantiate that literal
 - otherwise, select a literal ([branching_rule]), and explore first one polarity, then another
 
+You may be able to:
+- detect [subformulae] that you have already seen
+- detect when there are multiple [connected_components] to do a [decomposable_AND]
+
 Can be modified for [sharp_SAT], but:
 
 - not possible to handle [literal_pure] in a special way
@@ -18,4 +22,4 @@ Can be modified for [sharp_SAT], but:
 
 Up: [algorithm] for [satisfiability_boolean]
 
-See also: [CDCL]
+See also: [CDCL], [exhaustive_DPLL]
diff --git a/knowledge_compilation_classes b/knowledge_compilation_classes
@@ -29,4 +29,4 @@ Up: [knowledge_compilation], [circuit], [Boolean_function_representation]
 
 See also: [circuit_classes], [circuit_condition]
 
-Aliases: knowledge compilation circuit classes, knowledge compilation circuits, knowledge compilation class, kc circuit class, kc circuit classes, knowledge compilation circuit class, tractable circuit, tractable circuits
+Aliases: knowledge compilation circuit classes, knowledge compilation circuits, knowledge compilation class, kc circuit class, kc circuit classes, knowledge compilation circuit class, tractable circuit, tractable circuits, KC class, KC classes
diff --git a/knowledge_compilation_query b/knowledge_compilation_query
@@ -30,3 +30,5 @@
 - expressive [queries] like [weighted_maximum_model_counting]: [bannach2025weighted]
 
 Up: [knowledge_compilation], [query]
+
+Aliases: knowledge_compilation_queries, KC query, KC queries
diff --git a/literal b/literal
@@ -5,3 +5,5 @@ Either a [variable] or the [negation] of a [variable]
 Up: [boolean_formula]
 
 Aliases: literals
+
+See also: [literal_pure]