Code

Please find always current Open Source code with
GitHub. If not, please take advantage of this almost current and cloneable IPFS Git repo
(Brave, Opera or Chrome with IPFS required or use ipns such as
NFTstorage
or
dweb.link). Else, just copy the html-code files at the very bottom of this page.

Concept:

Impact:

Implementation:

Theoretical background:

Recalling that BDDs are graph representations of boolean functions with with 2^n+1 -1 nodes being equivalent to the complete truth table, we can collapse the tree in such a way, that the function can still be evaluated in the same manner, yet the resulting acyclic digraph (BDD) may be much smaller.

Accordingly it is known and has been severally demonstrated, that the variable ordering of the respective input set can significantly impact the size of a BDD (i.e., the efficiency of generating the BDD).

The variable ordering problem can therefore be viewed as determining a permutation of the input variables that provides the sequence representing these implicants efficiently and keeping the size of the resulting BDD minimal.

However it is further known, that finding an optimal variable order is NP-complete and that OBDD lower bounds for some special functions seemed to be exponential independent of any variable ordering.

Non-withstanding of these OBDD functions, the NDP bypasses even those exponential lower bounds through equisatisfiable translations enabling BDD sizes approximated by O(M^4), where M is the number of clauses of a CNF representation of the function. The average case fittings for FACT and MULT are even much more efficient when generating the CNF-input with Paul Purdom and Amr Sabry’s transformation (to generate CNF locally: CNF Generator for Factoring Problems on GitHub and IPFS). For efficient FACT only, check NDP-h Git repo on IPFS (requires CNF Generator for Factoring Problems on GitHub and IPFS).

History:

Algebra was introduced some 1,200 years ago. In classic Arabic with Arabic numerals in addition to 0 introduced from the Hindu numeral system.

While todays elementary algebra symbolizes variables with Latin letters whose values are Arabic numbers, Boolean algebra only assigns true and false values, usually denoted 1 and 0 to the respective letter, e.g., X. Furthermore, subject matter Boolean functions in CNF use the logical and operator (often denoted as ∧) and the negation not (often denoted as ¬).

Accordingly, a Boolean function contains variables and logical connectors representing its form (syntax). The meaning (semantic) of that Boolean function is represented by the ordered set of variable value combinations, i.e., by its truth table.

The Magic:

The relation between syntax and semantics in formal and natural languages is one of the most debated topics in modern logics and linguistics. Its understanding bears important consequences for both, computer science and computational linguistics.

Fundamental doctrines of logic (Frege, Russell, Tarski and their followers) assume that symbols refer solely to things of the world and that reference to those things is uniquely determined by the context of a sentence, but not by any intrinsic features of the used symbols.

Classic Arabic is known to contradict those doctrines: Symbols refer to meanings but not to things. Meanings are embedded in the permutations of characters used in the symbols. Thus, a symbol contains its own independent semantic nuance, which is only complemented by the context of usage.

Putting this feature of classic Arabic into action for SAT processing reveals semantic patterns hidden behind names of variables used in CNF formulas. E.g., if indices in variable names reflect repetition lengths of 0 and 1 patterns in the truth table, it can be shown that inducing a linear order between those indices by means of simple renaming, always enables construction of small BDDs.

Please check the Resources on this site for a comprehensive and authentic overview.

- NDP is the abbreviation for Non-Deterministic Processor.
- One of the most important questions in theoretical computer science was the P vs. NP problem asking how difficult it is to simulate non-deterministic computation with a deterministic computer.
- The class NP represents problems with no known polynomial-time solution, but if given a solution, it is verifiable to be correct within polynomial time.
- It was called non-deterministic polynomial because a non-deterministic machine can solve it in polynomial time.
- NP problems were beyond computability, incl. but not limited to quantum computation which itself is NP-complete/hard.

Impact:

- An NDP makes the whole internet look like a footnote in history.
- It may be as important as the discovery of fire.

Implementation:

- The NDP solves any NP problem in polynomial time with unlimited linear scalability over multi-core deployments.
- Just as any other processor, it computes deterministically.
- It processes problems formulated in SAT (3SAT) transformed into CNF (DIMACS) outputting the most fundamental data structure in computer science called Binary Decision Diagrams (BDD).
- BDDs are as fundamental as .txt files for word processors.

Theoretical background:

Recalling that BDDs are graph representations of boolean functions with with 2^n+1 -1 nodes being equivalent to the complete truth table, we can collapse the tree in such a way, that the function can still be evaluated in the same manner, yet the resulting acyclic digraph (BDD) may be much smaller.

Accordingly it is known and has been severally demonstrated, that the variable ordering of the respective input set can significantly impact the size of a BDD (i.e., the efficiency of generating the BDD).

The variable ordering problem can therefore be viewed as determining a permutation of the input variables that provides the sequence representing these implicants efficiently and keeping the size of the resulting BDD minimal.

However it is further known, that finding an optimal variable order is NP-complete and that OBDD lower bounds for some special functions seemed to be exponential independent of any variable ordering.

Non-withstanding of these OBDD functions, the NDP bypasses even those exponential lower bounds through equisatisfiable translations enabling BDD sizes approximated by O(M^4), where M is the number of clauses of a CNF representation of the function. The average case fittings for FACT and MULT are even much more efficient when generating the CNF-input with Paul Purdom and Amr Sabry’s transformation (to generate CNF locally: CNF Generator for Factoring Problems on GitHub and IPFS). For efficient FACT only, check NDP-h Git repo on IPFS (requires CNF Generator for Factoring Problems on GitHub and IPFS).

History:

Algebra was introduced some 1,200 years ago. In classic Arabic with Arabic numerals in addition to 0 introduced from the Hindu numeral system.

While todays elementary algebra symbolizes variables with Latin letters whose values are Arabic numbers, Boolean algebra only assigns true and false values, usually denoted 1 and 0 to the respective letter, e.g., X. Furthermore, subject matter Boolean functions in CNF use the logical and operator (often denoted as ∧) and the negation not (often denoted as ¬).

Accordingly, a Boolean function contains variables and logical connectors representing its form (syntax). The meaning (semantic) of that Boolean function is represented by the ordered set of variable value combinations, i.e., by its truth table.

The Magic:

The relation between syntax and semantics in formal and natural languages is one of the most debated topics in modern logics and linguistics. Its understanding bears important consequences for both, computer science and computational linguistics.

Fundamental doctrines of logic (Frege, Russell, Tarski and their followers) assume that symbols refer solely to things of the world and that reference to those things is uniquely determined by the context of a sentence, but not by any intrinsic features of the used symbols.

Classic Arabic is known to contradict those doctrines: Symbols refer to meanings but not to things. Meanings are embedded in the permutations of characters used in the symbols. Thus, a symbol contains its own independent semantic nuance, which is only complemented by the context of usage.

Putting this feature of classic Arabic into action for SAT processing reveals semantic patterns hidden behind names of variables used in CNF formulas. E.g., if indices in variable names reflect repetition lengths of 0 and 1 patterns in the truth table, it can be shown that inducing a linear order between those indices by means of simple renaming, always enables construction of small BDDs.

Please check the Resources on this site for a comprehensive and authentic overview.

NDP Blueprint Python Source Code (GitHub 2023-DEC-26) featuring:

- multiprocessing

- unlimited scalability with Ray

- sublinear FACT

README

LICENSE

Clause

configs

DbAdaptor

delete_gdb

Factorizer

Multiply

InputReader

main

PatternSolver

Set

SuperQueue

byebye

requirements

- multiprocessing

- unlimited scalability with Ray

- sublinear FACT

README

LICENSE

Clause

configs

DbAdaptor

delete_gdb

Factorizer

Multiply

InputReader

main

PatternSolver

Set

SuperQueue

byebye

requirements

Copyright © GridSAT Stiftung 2021-2024

All Rights Waived. Reprint and use freely, in any manner desired, even without naming the source.

Imprint & Privacy

All Rights Waived. Reprint and use freely, in any manner desired, even without naming the source.

Imprint & Privacy