Development of the Concept of Non-Orthodox Combinatorial Models Based on Discordant Structures for 3-SAT Problem Resolvation

Dear Fellow Researchers,

Would you kindly pay attention to the article “Discordant Compact Logic-Arithmetic Structures in Discrete Optimization Problems” by the author V. F. Romanov published on arXiv.org: http://arxiv.org/abs/1309.6078.

The previous paper of the author introduced the model for effective resolvability of 3-SAT problem based on unique special purpose components: structures of compact triplets and systems of hyperstructures. A concealed shortcoming of the filtration procedure for the complicated hyperstructures didn’t allow considering the model as irreproachable for the totality of input formulas.

The novel model uses, however, the merits of the structures of compact triplets (CTS) and, moreover, their outcome: the structures of compact couples (CCS); the system of CCS forms foundation of the new method and algorithm for 3-SAT problem resolving.

The problem is reduced to elementary detection of n-tuples of zeros in the discordant CCS system, prepared for this purpose by means of a special transformation. The formula is synthesized, being on the structure a variation of 2-CNF, associated with the calculation procedure realizing adaptation of the polynomial algorithm of constraints distribution (well-known in the optimization theory) to the efficient resolving of Boolean formula coded by means of discordant compact structures.

As a whole the described algorithmic model of 3-SAT problem representation and solution belongs to the class of polynomial models. No use of heuristic modes and complicated systems of hyperstructures radically distinguish the given model from earlier workings out of the author.

Your opinion and suggestions concerning my work would be of great value for me.

Yours faithfully, the author Vladimir Romanov

Advertisements
This entry was posted in Uncategorized. Bookmark the permalink.

10 Responses to Development of the Concept of Non-Orthodox Combinatorial Models Based on Discordant Structures for 3-SAT Problem Resolvation

  1. Vor says:

    Do you have a working code that can be used to test a (very) hard SAT instance?

    • dmitrygusev says:

      No, at the moment we don’t even have a reference implementation to test any instances.

      By hard you mean a huge instance?

      As a previous version, new algorithm doesn’t make any assumptions on instance structure, so it should work the same for all (easy and hard) instances. It also much lighter by the means of required computations and memory consumption, so it should be possible to create implementations that are able to solve bigger instances than previous algorithm.

      • J says:

        When can we expect a reference implementation to be available?

      • dmitrygusev says:

        I can’t give you an exact estimates, because I’m working on this in my spare time, which I don’t have a lot this time.

        Current implementation should be much simpler than previous: there is no more hyperstructures and concordant shifts, etc. So if someone else wants to try his skills and implement this — you’re welcome, I will try to answer any questions with the help of Vladimir Romanov.

        Meanwhile you can watch this repo on github: https://github.com/anjlab/sat3. If new implementation will appear from me — it will be there. Of course, I will also write a post here when it will be ready.

  2. Vor says:

    I just gave a look at the paper: the transformation from F to CTF is not clear (to me). What does it mean to “group the lines of F with identical numbers of three non-empty columns”? I can figure out what are the source lines of the CT formula F1 (they are the rows of F with three consecutive non empty columns), but where do the the lines of of the CT formula F2 come from ? Furthermore the “putting three non-empty columns …” is not clear. Perhaps you should formally define the two steps, and expand the example describing the two steps applied to F in detail.

    • dmitrygusev says:

      Rows for F2 also taken from F, but the permutation of variables changed for F2.

      You can look at the previous reference implementation, F => CTF set completely implemented there. Try running any example using this solver, and examine debug output.

  3. Tesseractic says:

    It’s been over a year now and there’s no sign of a reference implementation over on GitHub; has this new(er) algorithm been implemented by the author, or does this algorithm only exist on paper and in V.F. Romanov’s mind? I’m finding the paper’s description of the algorithm difficult to follow.

    Dmitry: have you made any progress on a reference implementation?

    • Tesseractic says:

      Also, is the paper’s description of the algorithm completely sufficient, or does it require, for instance, knowledge of ‘constraints distribution’?

      Is there an alternative reference for ‘constraints distribution’, preferably on the net?

    • dmitrygusev says:

      Tesseractic:

      There’s no reference implementation (yet?), at least not the one I know of. I also don’t know if professor Romanov has any implementation available. I suggest you to contact him directly at romvf@mail.ru.

      I haven’t made any progress on new implementation, and I won’t have any time soon to work on it.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s