Reference Implementation of Polynomial Algorithm for 3-SAT Problem
|
This is result of our joint research togerher with professor Romanov (VlGU, Vladimir).The project is reference implementation of algorithm introduced in Romanov’s article Non-orthodox combinatorial models based on discordant structures published on arXiv.org. This paper introduces a novel method for compact representation of sets of n-dimensional binary sequences in a form of compact triplets structures (CTS), supposing both logic and arithmetic interpretations of data. Suitable illustration of CTS application is the unique graph-combinatorial model for the classic intractable 3-Satisfiability problem and a polynomial algorithm for the model synthesis. The method used for Boolean formulas analysis and classification by means of the model is defined as a bijective mapping principle for sets of components of discordant structures to a basic set. The statistic computer-aided experiment showed efficiency of the algorithm in a large scale of problem dimension parameters, including those that make enumeration procedures of no use. The formulated principle expands resources of constructive approach to investigation of intractable problems. Our implementation is published it as open source (LGPLv3) on github. Currently this implementation is in public beta and may have bugs. Go grab it, test it and submit issues if you find them. Any feedback is appreciated. Links |
