commit cbe5b838222ac1c938673aa3cc4ffe9f56418ef1
parent c9d2397ef33b6a1dc0a4c9de441b79069b6f8e7f
Author: Antoine Amarilli <a3nm@a3nm.net>
Date: Mon, 15 Jun 2026 15:47:40 +0200
commit with codex
Diffstat:
6 files changed, 33 insertions(+), 5 deletions(-)
diff --git a/circuit_equivalence b/circuit_equivalence
@@ -7,3 +7,5 @@ The [computational_problem] of deciding, given two [Boolean_circuits], whether t
Up: [Boolean_function_equivalence], [circuit]
Aliases: circuit equivalence problem
+
+See also: [circuit_implication]
diff --git a/enumeration_circuit b/enumeration_circuit
@@ -13,3 +13,5 @@ Harder than [satisfiability_boolean] so [np_hard] on general [boolean_circuit]
Up: [enumeration] on [boolean_circuit]
See also: [enumeration_via_circuit]
+
+Aliases: enumerating satisfying assignments
diff --git a/falsifying_valuation b/falsifying_valuation
@@ -4,6 +4,6 @@ A [Boolean_valuation] such that a [Boolean_function] [evaluates] to [false]
Up: [Boolean_valuation]
-See also: [satisfiability_boolean], [satisfying_valuation]
+See also: [satisfiability_boolean], [satisfying_valuation], [falsifiability]
Aliases: falsifying valuations, falsifying assignment, falsifying assignments
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
+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
diff --git a/knowledge_compilation_query b/knowledge_compilation_query
@@ -1,8 +1,32 @@
# Knowledge compilation query
-- [satisfiability]
-- [sharp_satisfiability]
+- [satisfiability]: does there exist a [satisfying_assignment]
+- [falsifiability]: does there exist a [falsifying_assignment]
+ - or is the formula a [tautology]
+- [sharp_satisfiability]: count the number of [satisfying_assignments]
+
+- [weighted_satisfiability]
+- [weighted_model_counting]
+
+- [enumerating_satisfying_assignments]
+
+- [uniform_sampling] of [satisfying_assignment]
+
+- [most_probable_explanation], connection to [smallest_witness]
+ - and likewise for the negation, connection to [query_resilience]
+
+- find an [implicant]
+- [shortest_implicant]
+
+- [clause_entailment], see if a clause is entailed
+
+- [maj_sat], [gt_maj_sat]
+
- [max_sat]
+
+- test [circuit_equivalence]
+- test [circuit_implication] aka "sentential entailment"
+
- expressive [queries] like [weighted_maximum_model_counting]: [bannach2025weighted]
Up: [knowledge_compilation], [query]
diff --git a/satisfiability b/satisfiability
@@ -10,7 +10,7 @@ The *satisfiability problem* is a [decision_problem] in [logic]: given a [logica
Tools: [sat_solver]
-See also: [strong_exponential_time_hypothesis], [satisfiability_boolean], [tautology], [automaton_emptiness], [satisfiability_modulo_theory], [equisatisfiability], [enumeration_valuations], [satisfiability_finite]
+See also: [strong_exponential_time_hypothesis], [satisfiability_boolean], [tautology], [automaton_emptiness], [satisfiability_modulo_theory], [equisatisfiability], [enumeration_valuations], [satisfiability_finite], [falsifiability]
Up: [computational_problem]
