January 22, 2011 at 14:56Discussion of the operation of the Romanov algorithm using an example
In continuation of yesterday's discussion .
The last time we stopped at explaining how the unification and filtering algorithms work on a specific example. The example itself was built in a special way to test certain properties of the algorithms.
For further discussion, I wrote a small unit test that operates with the formula from the example. The unit test is needed to skip the step of the Romanov algorithm, where the initial formula is decomposed into a set of CTFs. Instead, decomposition is proposed initially by the author of the question.
Unit test and detailed log of the application I posted here:
gist.github.com/791064
If possible, I suggest referring there by line numbers (it’s not very convenient there that you cannot give a direct link to the line number, you have to look for it manually; if someone offers a more convenient service, I will transfer the log there).
As you can see from the log of work, the test ends with the situation when at the next step of constructing the hyperstructure the base graph turned out to be an empty set, which according to the algorithm means that the formula is not feasible (item 2b at the bottom of page 11 in the text of the article ).
In order not to rewrite the article here again, I propose in the discussion to ask questions that require additional clarification.
The last time we stopped at explaining how the unification and filtering algorithms work on a specific example. The example itself was built in a special way to test certain properties of the algorithms.
For further discussion, I wrote a small unit test that operates with the formula from the example. The unit test is needed to skip the step of the Romanov algorithm, where the initial formula is decomposed into a set of CTFs. Instead, decomposition is proposed initially by the author of the question.
Unit test and detailed log of the application I posted here:
gist.github.com/791064
If possible, I suggest referring there by line numbers (it’s not very convenient there that you cannot give a direct link to the line number, you have to look for it manually; if someone offers a more convenient service, I will transfer the log there).
As you can see from the log of work, the test ends with the situation when at the next step of constructing the hyperstructure the base graph turned out to be an empty set, which according to the algorithm means that the formula is not feasible (item 2b at the bottom of page 11 in the text of the article ).
In order not to rewrite the article here again, I propose in the discussion to ask questions that require additional clarification.