Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: comp.lang.prolog
Subject: Re: The road to Artificial Intelligence
Date: Sat, 16 Mar 2024 14:13:50 +0100
Message-ID: <ut45uc$1efp6$1@solani.org>
References: <b406aa35-c39b-46f3-862f-1cc4b75143ae@googlegroups.com>
 <338dc0fb-4a93-405f-99da-7799d25ddc91n@googlegroups.com>
 <url15e$m5i4$3@solani.org> <ut45h5$1efic$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 16 Mar 2024 13:13:48 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1523494"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.18.1
Cancel-Lock: sha1:yDX/FW2qrvwQ+pB9nrx5YCQsvrw=
X-User-ID: eJwFwQkBACAIBLBKIN8ZBxD6R3AzcfYOdXO1taWnWbmqaEeO3UAQxliLr0+5LPg0qPPZpCD0kdRZGRAHfVTPFTM=
In-Reply-To: <ut45h5$1efic$1@solani.org>
Bytes: 2526
Lines: 50


Or a more striking example, Peter Norvig's impossible
Sudoku, which he claims took him 1439 seconds
to show that it is unsolvable:

/* Peter Norvig */
problem(9, [[_,_,_,_,_,5,_,8,_],
             [_,_,_,6,_,1,_,4,3],
             [_,_,_,_,_,_,_,_,_],
             [_,1,_,5,_,_,_,_,_],
             [_,_,_,1,_,6,_,_,_],
             [3,_,_,_,_,_,_,_,5],
             [5,3,_,_,_,_,_,6,1],
             [_,_,_,_,_,_,_,_,4],
             [_,_,_,_,_,_,_,_,_]]).

https://norvig.com/sudoku.html

whereby SWI-Prolog with all_distinct/1 does
it in a blink, even without labeling:

?- problem(9, M), time(sudoku(M)).
% 316,054 inferences, 0.016 CPU in 0.020 seconds
  (80% CPU, 20227456 Lips)
false.

Pretty cool!

Mild Shock schrieb:
> I didn't make all my homework yet.
> For example just fiddling around with CLP(FD), I get:
> 
> ?- maplist(in, Vs, [1\/3..4, 1..2\/4, 1..2\/4,
>            1..3, 1..3, 1..6]), all_distinct(Vs).
> false.
> 
> Does Scryer Prolog CLP(Z) have some explanator for that?
> What is exactly the conflict that it fails?
> 
> Mild Shock schrieb:
>>
>> Terence Tao, "Machine Assisted Proof"
>> https://www.youtube.com/watch?v=AayZuuDDKP0
>>
>> Mostowski Collapse schrieb:
>>> Don't buy your Pearls in Honk Kong. They are all fake.
>>>
>>> So what do you prefer, this Haskell monster:
>>> https://www.cs.nott.ac.uk/~pszgmh/countdown.pdf
>