wiki_research

commit 040c2c73d995590bd477fd306451fbc68318fcb8
parent 87d23aa9ae8429b084b090c6393b0dc8ccc349de
Author: Antoine Amarilli <a3nm@a3nm.net>
Date:   Mon,  6 Jan 2025 23:59:57 +0100

Merge branch 'master' of a3nm.net:git/wiki_research

Diffstat:
boolean_circuit
 | 
2
++
circuit
 | 
2
++
circuit_equivalence
 | 
5
+++++
cnf_variable_convex
 | 
9
+++++++++
conjunctive_normal_form
 | 
2
++
convexity
 | 
8
++++++++
ddnnf
 | 
2
++
equisatisfiability
 | 
2
++
equivalence
 | 
8
++------
equivalence_problem
 | 
11
+++++++++++
mathematics
 | 
1
+
ramsey_theorem
 | 
4
+++-
tseytin_transformation
 | 
7
+++++++

13 files changed, 56 insertions(+), 7 deletions(-)
diff --git a/boolean_circuit b/boolean_circuit
@@ -10,3 +10,5 @@ Similar: https://en.wikipedia.org/wiki/Propositional_directed_acyclic_graph
 Up: [circuit]
 
 See also: [boolean_formula], [knowledge_compilation_classes]
+
+Aliases: Boolean circuits
diff --git a/circuit b/circuit
@@ -51,3 +51,5 @@
 Up: [theoretical_computer_science]
 
 See also: [sum_product_network]
+
+Aliases: circuits
diff --git a/circuit_equivalence b/circuit_equivalence
@@ -0,0 +1,5 @@
+# Circuit equivalence
+
+[Computational_problem] of deciding, given two [Boolean_circuits], whether they represent the same [Boolean_function]
+
+Up: [equivalence], [circuit]
diff --git a/cnf_variable_convex b/cnf_variable_convex
@@ -0,0 +1,9 @@
+# Cnf variable convex
+
+defined in [bova2017compiling]
+
+Up: [conjunctive_normal_form]
+
+Aliases: variable convex CNF, variable convex formula
+
+See also: [convexity]
diff --git a/conjunctive_normal_form b/conjunctive_normal_form
@@ -2,11 +2,13 @@
 
 A [boolean_formula] which is a [conjunction] of [clauses]
 
+Types:
 - [monotone_cnf]
 - [2cnf]
   - [monotone2cnf]
 - [3cnf]
 - [kcnf]
+- [cnf_variable_convex]
 
 lower bound on size of CNF relative to [disjunctive_normal_form]
 
diff --git a/convexity b/convexity
@@ -0,0 +1,8 @@
+# Convexity
+
+- [convex_function]
+- [convex_set]
+- [convex_hull]
+- [cnf_variable_convex]
+
+Up: [mathematics]
diff --git a/ddnnf b/ddnnf
@@ -2,6 +2,8 @@
 
 [deterministic] [decomposable] [nnf]
 
+testing [circuit_equivalence] of d-DNNFs is in [coRP]: [darwiche2002testing]
+
 Up: [knowledge_compilation_classes], [dd]
 
 See also: [dnnf], [decision_dnnf], [uobdd]
diff --git a/equisatisfiability b/equisatisfiability
@@ -7,3 +7,5 @@ Two [logic_formulas] f and f' are equisatisfiable if f being satisfiable is [equ
 Up: [satisfiability]
 
 Aliases: equisatisfiable
+
+See also: [equivalence_problem]
diff --git a/equivalence b/equivalence
@@ -1,15 +1,11 @@
 # Equivalence
 
-As [computational_problem]:
-
-- [language_equivalence]
-- [query_equivalence]
-- [automaton_equivalence]
-- [regular_expression_equivalence]
+As [computational_problem]: [equivalence_problem]
 
 Other:
 
 - [equivalence_relation]
+- [equivalence_operator] in [propositional_logic]
 
 Up: [mathematics]
 
diff --git a/equivalence_problem b/equivalence_problem
@@ -0,0 +1,11 @@
+# Equivalence problem
+
+- [language_equivalence]
+- [query_equivalence]
+- [automaton_equivalence]
+- [regular_expression_equivalence]
+- [circuit_equivalence]
+
+Up: [computational_problem], [equivalence]
+
+See also: [equisatisfiability]
diff --git a/mathematics b/mathematics
@@ -46,6 +46,7 @@
 - [infinite]
 - [cardinal]
 - [fourier_transform]
+- [convexity]
 - [equality]
 - [inequality_mathematics]
 - [disequality]
diff --git a/ramsey_theorem b/ramsey_theorem
@@ -10,6 +10,8 @@ Generalizations:
 - [hypergraphs]
   - https://en.wikipedia.org/wiki/Ramsey%27s_theorem#Hypergraphs
 
-Can also be useful in [formal_language_theory]
+Can also be useful in [formal_language_theory]: [ramsey_formal_languages]
 
 Up: [mathematics]
+
+Aliases: Ramsey's theorem
diff --git a/tseytin_transformation b/tseytin_transformation
@@ -0,0 +1,7 @@
+# Tseytin transformation
+
+https://en.wikipedia.org/wiki/Tseytin_transformation
+
+Transform a [Boolean_circuit] into [equisatisfiable] [CNF], by adding some additional [variables]
+
+Up: [circuit]