The New Sudoku Players' Forum

[ag24ag24]

To your other point: I have not mplemented a solver based on TLC, largely because the use of three premises rather than two would make it very much slower. However, I agree with you that TLC-resisting puzzles should be the focus for understanding the power of ATLC, so I may try to do a TLC-based solver.

[ag24ag24]

I would say that the question of whether any sukaku resists ATLC is more nteresting than the question of whether anything resists TLC but yields to ATLC, but I agree that they are both interesting!

I have never previously edited a post, but I'll try to do as you ask.

[ag24ag24]

Posts edited, result as hoped! Many thanks.

[denis_berthier]

a new (or so I believe!) resolution theory that seems to be extremely powerful, deriving full solutions - purely stepwise, i.e. in T&E(0) - for many (looks like most; conceivably all...) puzzles that are in ph_2010

A puzzle is in T&E(0) iff it can be solved in BRT (the universal Basic Resolution Theory) - i.e. by Singles + elimination by direct contradiction with decided values.
All the puzzles in ph_2010 are in T&E(2) [except one erroneously present in the collection].
So, you probably want to rephrase this sentence?
.

[denis_berthier]

The one thing that I realise may be unorthodox is that resolution rules can derive new assertions, whereas in all the RTs I've seen discussed here (and elsewhere) they always derive eliminations in one step.

Not exactly. The expression "resolution rule" was introduced in [HLS 2007] with precise meaning. It allows the assertion of a candidate. There are typical and classical rules that assert a candidate: Singles, UR1, basic tridagon...

You are using the same expression "resolution rule" in a more general meaning, where you can assert a disjunction of candidates. This allows a higher degree of complexity - and the computational problems that go with it. This can also be viewed as allowing OR branching - a restricted form of T&E. This should a priori allow you to go beyond T&E(1).
In my approach, OR-branching is allowed for exotic patterns (tridagon, impossible patter, deadly patterns...) in rules that introduce ORk-relations and used in ORk-chains, but all this is intended for use in only very specific situations.
.

[ag24ag24]

I of course defer to your statement of the terminology - but I had understood the definition of "T&E" to be with respect to a given resolution theory. In other words, that when (for example) we say "T&E(2)" we are abbreviating "T&E(Singles,2)", but that there can equally be "T%E(Basics,2)" and so on. But regardless, I hope my meaning is clear - there is no trial-and-error in the algorithm that I've been using to solve puzzles with the ATLC resolution theory.

[denis_berthier]

NEW RESOLUTION THEORY. My new RT uses not only links and truths but also a third type of assertion, which I will call an arrow. An arrow is a truth contingent on another truth
[...]
Arrows may sound innocent enough at first: seemingly they are just merges of two steps in a standard AIC (a link followed by a truth). However, in their full generality they turn out to be far more powerful than that.

Arrows amount to introducing one more level of T&E.
.

[denis_berthier]

I of course defer to your statement of the terminology - but I had understood the definition of "T&E" to be with respect to a given resolution theory. In other words, that when (for example) we say "T&E(2)" we are abbreviating "T&E(Singles,2)", but that there can equally be "T%E(Basics,2)" and so on. But regardless, I hope my meaning is clear - there is no trial-and-error in the algorithm that I've been using to solve puzzles with the ATLC resolution theory.

Did you mean T&E(your RT, 0) ?
If so, you'd better give a name to your RT and write it that way.
.

[marek stefanik]

ATLC can indeed solve any sudoku (or sukaku).
I will provide a short outline of a proof, based on the implicational completeness of Resolution.

Let S be a set of clauses. For every non-tautological clause C that is logically implied by S there is clause D, derivable by resolution from S, such that D subsumes C.

You can represent each candidate as a variable.
I will define a restricted Resolution (RR for short) which uses just 3 types of clauses:
clauses with no negation (truths),
clauses with one negation (arrows),
clauses consisting of two negated variables (without any non-negated ones; links).
The sudoku axioms are truths and links.

Non-restricted Resolution can solve any sudoku, since it is implicationally complete.
I will show that RR can also solve any sudoku.

Def: A truth T represents a clause C iff each candidate in T appears non-negated in C or is directly linked to a negated candidate in C.

We can construct a solution by RR from a solution by Resolution as follows:

We first convert links to truths:
We resolve each link ¬c1 ∨ ¬c2 with a truth including c1 but not c2, then we resolve the resolvent and a truth containing c2 but not c1.
The final result is a truth representing the initial link.
For example, from the link ¬1r1c1 ∨ ¬1r1c2 we may first obtain the arrow 2r1c1 ∨ ... ∨ 9r1c1 ∨ ¬1r1c2 and then the truth 2r1c1 ∨ ... ∨ 9r1c1 ∨ 1r2c2 ∨ ... ∨ 1r9c2.
At this stage we have a truth representing each axiom.

Whenever Resolution resolves two clauses C1 and C2 by cancelling out the candidate c, which WLOG appears negated in C1 and non-negated in C2, we find truths T1 and T2 representing C1 and C2 respectively.
If T1 contains no candidate c' linked to c, each candidate of T1 appears in C1\{c} or is linked to a negated candidate in C1\{c}, therefore also in the resolvent, so T1 represents the resolvent.
If T2 does not contain c, T2 represents the resolvent.
Otherwise we iteratively resolve T1 with each link ¬c ∨ ¬c', s.t. T contains c'. We then resolve with T2 and the final result represents the resolvent obtained by Resolution.
In all clauses created in this process, c is the only candidate which appears negated.
For example, when Resolution resolves clauses 1r1c1 ∨ ¬2r2c2 and 2r2c2 ∨ 3r3c3 ∨ 4r4c4 and we have truths 1r1c1 ∨ 2r1c2 ∨ 4r2c2 and 2r2c2 ∨ 3r3c3 representing them, we obtain
1r1c1 ∨ ¬2r2c2 ∨ 4r2c2, then 1r1c1 ∨ ¬2r2c2, and finally 1r1c1 ∨ 3r3c3, which indeed represents 1r1c1 ∨ 3r3c3 ∨ 4r4c4.

Whenever Resolution derives the elimination ¬c, we derive it by iteratively resolving the corresponding truth with links ¬c ∨ ¬c', s.t. T contains c'.
For example, when Resolution derives ¬2r2c2 and we have the truth 2r1c1 ∨ 2r2c8 ∨ 4r2c2 representing it, we obtain ¬2r2c2 ∨ 2r2c8 ∨ 4r2c2, then ¬2r2c2 ∨ 4r2c2, and finally ¬2r2c2.

All of this can be simulated in ATLC using the rules LTA, ATT, and ALA.

I wouldn't be surprised if TLC can also solve any sudoku.
Maybe the rules TLTT and LTLL are a sufficient replacement for arrows, but I won't try to prove it.

Marek

[ag24ag24]

Did you mean T&E(your RT, 0) ?
If so, you'd better give a name to your RT and write it that way.
.

Yes, I meant T&E(ATLC,0) since I have given the name "ATLC" to my RT.

[ag24ag24]

Thank you Marek! I think I understand your argument, but I'm missing one part - you seem to be starting from the claim that non-restricted Resolution achieves its implicational completeness via only two rules, namely (1) resolving C1 and C2 by cancelling out a candidate that they share (negated in exactly one of them), and (2) deriving the elimination of a candidate. I can see how you model those two rules in your RR, and I think I can see how to model your RR with my ATLC, but I don't see why those two rules can necessarily deliver implicational completeness.

[ag24ag24]

Arrows amount to introducing one more level of T&E.

Can you please elaborate? Are you saying that puzzles in T&E(Singles,3) should then not be in T&E(ATLC,0) ?

[denis_berthier]

Arrows amount to introducing one more level of T&E.

Can you please elaborate? Are you saying that puzzles in T&E(Singles,3) should then not be in T&E(ATLC,0) ?

On the contrary. Arrows allow to make deductions conditional on their premises (which is 1 level of T&E if there's only one premise).
I can't give much detail. I haven't had time to read the details of your rules (and BTW, your example is eligible).
.

[denis_berthier]

Did you mean T&E(your RT, 0) ?
If so, you'd better give a name to your RT and write it that way.

Yes, I meant T&E(ATLC,0) since I have given the name "ATLC" to my RT.

But then you must write T&E(ATLC, 0) or simply ATLC. Otherwise, you're introducing much confusion as soon as the 1st post of the topic.
.

[marek stefanik]

Regarding the implicational completeness of Resolution, I sadly cannot be of much help.
Even the course in computational logic which I took last year didn't go over the proof, not even for refutation-completeness.
My only advice is to look at the article I linked. I think its reference 7 should have the answers (and is publicly available). I will probably check it out myself soon.

One nitpicky note:
Resolution only uses the rule (1) you mentioned.
Rule (2) is just a way how we can interpret its results: if it derives the clause c, we can set the candidate c, if the clause ¬c, we can eliminate it.
I mentioned the elimination only because I had to specifically construct it in RR from a truth representing it (which is not the case for assertions, as long as the puzzle has a solution).

Of course, neither RR nor ATLC are implicationally complete as they cannot represent clauses with more than 2 negations, but the sudoku axioms allow for a work-around.

Marek