< 1570927683 555539 :oerjan!oerjan@sprocket.nvg.ntnu.no JOIN :#esoteric > 1570928232 555769 PRIVMSG #esoteric :14[[07Keg14]]4 10 02https://esolangs.org/w/index.php?diff=66643&oldid=66634 5* 03JonoCode9374 5* (+25) 10/* Swap the words good and bad */ < 1570928661 765186 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 268 seconds < 1570930861 716789 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1570930885 521354 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :`addquote I have made a chess engine in Malbolge in theory it's decent but it has two drawbacks a) It requires 31 and a half gigabytes of memory b) it's quicker to count atoms in universe than to run it < 1570930887 203064 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :1336) I have made a chess engine in Malbolge in theory it's decent but it has two drawbacks a) It requires 31 and a half gigabytes of memory b) it's quicker to count atoms in universe than to run it < 1570932041 42102 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :@message kspalaiologos care to share this mythical chess engine? < 1570932041 121670 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :Maybe you meant: messages messages-loud messages? < 1570932051 787127 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :@tell kspalaiologos care to share this mythical chess engine? < 1570932051 829022 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :Consider it noted. < 1570932659 897381 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :imode: it was linked in the logs < 1570932692 970027 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :I read on Wikipedia about digital television captions, and they mention many things I have not seen in other TV sets < 1570932703 999649 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric : https://github.com/KrzysztofSzewczyk/malbolge-chess > 1570935190 477372 PRIVMSG #esoteric :14[[07Cupid14]]4 M10 02https://esolangs.org/w/index.php?diff=66644&oldid=58294 5* 03IFcoltransG 5* (+29) 10Added Turing Complete tag > 1570935229 652219 PRIVMSG #esoteric :14[[07Cupid14]]4 M10 02https://esolangs.org/w/index.php?diff=66645&oldid=66644 5* 03IFcoltransG 5* (+0) 10Fixed capitalisation on Turing complete category < 1570938288 430801 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1570938340 66547 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 264 seconds < 1570938343 599760 :atslash!~atslash@static.231.107.9.5.clients.your-server.de QUIT :Ping timeout: 250 seconds < 1570938373 276668 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1570938424 899680 :atslash!~atslash@46.188.0.82 JOIN :#esoteric < 1570939201 502484 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine < 1570939354 63064 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1570940760 787592 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 268 seconds < 1570943382 34252 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :I have been writing how I thought should be designed a television set. The digital caption setting menu includes service number 1-63, user override on/off, tag mask, enable flashing, maximum number of windows, font priority (user or broadcast), special effects on/off, auto switching services. < 1570943553 900457 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :The analog caption setting menu includes service selection (CC1-CC4 and TEXT1-TEXT4), user override on/off, allow/disallow white background, minimum roll-up, enable flashing, enable buffering, alarm on/off, character set (EIA-608 or ASCII). < 1570943768 899905 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Common caption setting menu can include: caption on mute, caption relative to either the picture or the screen, style submenu, status menu (can be used for debugging), caption recording. And then, there is also the caption scrollback feature, to review earlier captions. Do you think it is good enough? < 1570951612 871209 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1570952799 22340 :anima!~androirc@2a04:cec0:1005:7a6c:0:14:fc00:7a01 JOIN :#esoteric < 1570953118 583205 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1570955148 706965 :LKoen!~LKoen@81.255.219.130 QUIT :Remote host closed the connection < 1570955296 109861 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric < 1570955582 884125 :imode!~linear@unaffiliated/imode QUIT :Quit: WeeChat 2.6 < 1570955587 219822 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :oh nice. Zach from SMBC advertises his book on http://phdcomics.com/comics/archive.php?comicid=2033 < 1570955650 979203 :Ancyleus!~Ancyleus@47.149.105.11 JOIN :#esoteric > 1570955761 234204 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03YouTuringCompleteMe 5* 10New user account < 1570956207 674778 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr QUIT :Remote host closed the connection < 1570956277 513645 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric > 1570956442 837786 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=66646&oldid=66607 5* 03YouTuringCompleteMe 5* (+275) 10/* Introductions */ < 1570957487 571245 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Nite < 1570957861 593866 :arseniiv!~arseniiv@95.105.12.59.dynamic.ufanet.ru JOIN :#esoteric < 1570959106 698201 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr QUIT :Remote host closed the connection < 1570959449 732377 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric > 1570959682 454528 PRIVMSG #esoteric :14[[07Deadfish~14]]4 M10 02https://esolangs.org/w/index.php?diff=66647&oldid=38929 5* 03A 5* (+124) 10/* Sample Program */ < 1570959724 753174 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr QUIT :Remote host closed the connection < 1570959791 814953 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric < 1570960512 7361 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr QUIT :Remote host closed the connection < 1570960703 593989 :arseniiv!~arseniiv@95.105.12.59.dynamic.ufanet.ru QUIT :Ping timeout: 250 seconds < 1570961572 323155 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hmm, somehow the styles of http://www.yihcomic.com/ and http://sssscomic.com/ are quite similar. < 1570961817 658623 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Today I tried to actually figure out the details of CDCL and other tricks a bit more. < 1570961911 987130 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I feel like there are some basic things I'm confused about. I should probably implement the parts I understand to see if I become unconfused. < 1570961950 938998 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Here's one thing that's not even related to CDCL: < 1570962000 318685 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :When you need to decide on a variable and you add a literal p to your assumptions, what do you do? < 1570962043 877476 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :In theory you want to "delete" every clause that contains p and every literal ¬p from all the other clauses. < 1570962060 147017 :int-e!~noone@int-e.eu PRIVMSG #esoteric :well you don't < 1570962070 612830 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :The two-watched-literal trick lets you only worry about some clauses that contain ¬p, hopefully a small subset. < 1570962086 511467 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Do you need to worry about clauses that contain p at all or do you just ignore them? < 1570962097 912511 :arseniiv!~arseniiv@94.41.23.234.dynamic.ufanet.ru JOIN :#esoteric < 1570962178 501103 :int-e!~noone@int-e.eu PRIVMSG #esoteric :when processiong a clause you don't put it on another watched literal list if its next literal is already true, so this is part of the watched literal logic. < 1570962239 73423 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But then when you backtrack you might add it to a watched literal list? < 1570962269 700933 :int-e!~noone@int-e.eu PRIVMSG #esoteric :but you don't touch the watched literal lists when you backtrack? < 1570962273 849714 :int-e!~noone@int-e.eu PRIVMSG #esoteric :or backjump < 1570962315 830009 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Right, that's what I thought. But then I don't understand your previous sentence. < 1570962336 920162 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I believe you can just keep the clause on the list that you're processing < 1570962372 181153 :int-e!~noone@int-e.eu PRIVMSG #esoteric :uhm actually < 1570962378 137773 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So a large number of clauses is just irrelevant for you because you only ever find clauses through watch lists. < 1570962380 248498 :int-e!~noone@int-e.eu PRIVMSG #esoteric :sorry, I'm confused < 1570962546 443920 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But I think I got it right nevertheless. So... you go through the watch list of a literal l. If you encounter a clause that is already true in the current partial assignment (while looking for another literal that's currently unassigned), then you can keep the clause on the watch list for l, because whatever made the clause true is earlier on the trail than l. < 1570962562 165374 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(well, the trail has a negated l) < 1570962567 426017 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric < 1570962629 344552 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Meaning once the clause evaluation becomes unknown again, l will not be assigned, reestablishing the watched literal invariant (any clause with unknown truth value is on two watched literal lists) < 1570962665 401417 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :OK, so the only way a bunch satisfied clauses hurt you is that a watch list might contain them and you might need to sift through them? < 1570962676 433621 :int-e!~noone@int-e.eu PRIVMSG #esoteric :yes < 1570962702 293085 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :And you might e.g. move them to the end of a watch list and possibly be able to stop looking through a watch list early. < 1570962706 708861 :int-e!~noone@int-e.eu PRIVMSG #esoteric :this is a kind of laziness < 1570962709 761561 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Though I'm not sure a thing like that would actually work. < 1570962727 575825 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(but a good kind because many clauses that become true will never be touched at all) < 1570962767 307293 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm, but the ones that become true and are watched will just be inspected over and over because the watched literal will never move, unless you do something extra? < 1570962817 166414 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hmm, maybe it's clever to move them to the literal that is true instead. < 1570962832 407637 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, that makes sense. < 1570962847 777342 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(provided the clause is not on that watch list already) < 1570962857 717429 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :You can even locate the true literal that's furthest away in the stack, so hopefully you don't see it for a long time. < 1570962874 116104 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :what... are you writing SAT solvers? < 1570962882 932754 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Er, the last thing I said doesn't make sense. < 1570962917 411591 :int-e!~noone@int-e.eu PRIVMSG #esoteric :b_jonas: I've been resisting the temptation for a long time. I think I can maintain this state :) Not sure about shachaf. < 1570962980 80482 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Some of my questions are about the actual typical operations/memory layout/etc. used by reasonable SAT solvers. < 1570963005 595747 :arseniiv_!~arseniiv@136.169.230.185 JOIN :#esoteric < 1570963024 20500 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Others are about clause learning, which seems like one of the most complicated parts of many modern solvers. < 1570963024 376697 :int-e!~noone@int-e.eu PRIVMSG #esoteric :b_jonas: But I know enough about the basics (DPLL, CDCL, a bit about heuristics) to be harmful. < 1570963078 627700 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I know a bit more about the verification side. (RUP, DRUP, RAT, DRAT) < 1570963082 870177 :arseniiv!~arseniiv@94.41.23.234.dynamic.ufanet.ru QUIT :Ping timeout: 240 seconds < 1570963170 961356 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, UNSAT verification? < 1570963181 781 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I'd like to know about how that works. < 1570963290 72691 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I suspect understanding UNSAT certificates and understanding CDCL are pretty related? < 1570963308 512199 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Actually, no. < 1570963320 354814 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr QUIT :Remote host closed the connection < 1570963329 594844 :arseniiv_!~arseniiv@136.169.230.185 QUIT :Ping timeout: 250 seconds < 1570963341 302167 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, that's interesting. < 1570963401 969259 :int-e!~noone@int-e.eu PRIVMSG #esoteric :At least on a high level, certification works by maintaining a set of clauses (initially those of the problem) and adding and removing clauses with inferences that maintain satisficability. The last step derives the empty clause. < 1570963496 717744 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The inference relies heavily on unit propagation though, so for efficiency, you end up with watched literals again. < 1570963599 683768 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Sure, atched literals is a great trick. < 1570963617 272493 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I should understand regular SAT solving first. < 1570963684 418112 :int-e!~noone@int-e.eu PRIVMSG #esoteric :https://www.researchgate.net/publication/333612067_Efficient_Verified_UNSAT_Certificate_Checking should be a good starting point (including references for DRAT and DRUP). < 1570963763 469351 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: you should just wait for Knuth to write that part of volume 4. < 1570963780 817585 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The idea for RUP is that every backjump clause can be derived by "reverse unit propagation" -- assert the negation of the literals of the derived clause, and do unit propagation; if that results in a conflict, then the clause can be added without affecting satisfiability. So all a SAT solver has to do to produce a certificate is to record the backjump clauses which it's computing anyway. < 1570963788 761775 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(and potentially learning) < 1570963821 494034 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1570963838 249884 :int-e!~noone@int-e.eu PRIVMSG #esoteric :DRUP adds deletion of clauses (for efficiency). RAT is a bit more complicated and motivated by simplification of clause sets rather than DPLL itself. < 1570963984 846673 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :b_jonas: Fascicle 6? I have a copy right here. < 1570964014 898580 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :I have technically written a SAT solver once, but it's a rather trivially stupid one, it only works on very simple expressions < 1570964028 996948 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It doesn't talk about many of the things I want, though, I think. < 1570964033 880662 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I've only read part of it so far. < 1570964042 937747 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: so does it not help about "typical operations/memory layout/etc."? I'd expect Knuth to talk about those < 1570964070 635160 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It certainly talks about those, for the algorithms it describes. < 1570964197 775368 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :hmm, https://www-cs-faculty.stanford.edu/~knuth/news.html has multiple news that I haven't seen < 1570964261 661758 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I'll look at it some more after these papers. < 1570964326 731755 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :pity one of the links is already broken < 1570964571 444248 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :OK, it looks like the part of fascicle 6 two pages after where I left my bookmark in it a while ago is on the same topics I was reading papers on today. < 1570964576 318758 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I guess I'll take a closer look. < 1570964747 236256 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I see he gets up to RUP. < 1570964775 519350 :anima!~androirc@2a04:cec0:1005:7a6c:0:14:fc00:7a01 QUIT :Remote host closed the connection < 1570965399 31707 :anima!~androirc@2a04:cec0:1005:7a6c:0:14:fc00:7a01 JOIN :#esoteric < 1570965399 110104 :int-e!~noone@int-e.eu PRIVMSG #esoteric :
ACTION wonders how close the September 2015 pre-fascicle is to the printed fascicle...
< 1570965833 796399 :atslash!~atslash@46.188.0.82 QUIT :Read error: Connection reset by peer < 1570965896 558337 :atslash!~atslash@46.188.0.82 JOIN :#esoteric < 1570966215 338911 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :shachaf: int-e: While I've been just idling here for years, I just noticed discussion about SAT solving... I've written a CDCL SAT solver and UNSAT certificate checker https://github.com/jix/varisat (not using DRAT though, I'm using a different proof format that records unit propagations during solving and thus can be checked much faster)... feel free to ask me any questions about SAT solving :) < 1570966241 597384 :Ancyleus!~Ancyleus@47.149.105.11 QUIT :Ping timeout: 250 seconds < 1570966257 253925 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :idling... does that mean we should `welcome you? < 1570966277 116149 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :also, nice < 1570966291 55346 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :that just means I was quite active here... I don't know 10, 15 years ago or so and never parted :) < 1570966317 149774 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :yeah, this channel has a long history. < 1570966342 886904 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :``` q jix # the quote file doesn't know that you were active... not under this name at least < 1570966343 737102 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :No output. < 1570966353 77719 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :https://esolangs.org/wiki/Jannis_Harder << that's me < 1570966398 256298 :int-e!~noone@int-e.eu PRIVMSG #esoteric :jix: It's funny that you mention recording unit propagations... because the GRAT format does that as well, making for a three stage verification pipeline: simplifier+SAT-solver => DRAT => GRAT (fewer clauses, more information) => verifier. < 1570966418 367041 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :int-e: yeah I skip the DRAT => GRAT part which is as expensive as solving in the first place < 1570966438 126316 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(This is Lammich's pipeline... Heule et al. have a slightly different intermediate format ... I forgot the name.) < 1570966438 960517 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :what I do is solving -> custom format -> LRAT (which is inspired by GRAT) < 1570966483 611403 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :total time is cut roughly in half, but my solver isn't as good as others on many problems, so it's not that practical yet < 1570966504 20072 :int-e!~noone@int-e.eu PRIVMSG #esoteric :jix: It's funny though that the overhead of storing and reading additional information like that pays off. (Ah, LRAT. I think that was it. If so, it's a concurrent development to GRAT.) < 1570966543 601979 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :I experimented with emitting LRAT directly, but the code to keep track of clause ids became very complicated and introduced memory overhead < 1570966572 396491 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :so my next attempt just hashes clauses and resolves hash conflicts during conversion < 1570966632 727722 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :int-e: ah maybe it was inspired by a predecessor of GRAT? < 1570966656 31941 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hrm, let me check. < 1570966774 417395 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :there also is a newer DRAT proof checker, https://github.com/krobelus/rate that can emit LRAT and GRAT that is supposedly faster than drat-trim, but I haven't really benchmarked it yet < 1570966802 61039 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So... There's DRUP and DRAT as the foundation. There's a format called GRIT that records unit propagation steps. This is a precursor to both LRAT and GRAT, which do the same thing for RAT steps as well. < 1570966835 511602 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :ah, yeah, so I was thinking of GRIT when I read GRAT < 1570966901 853273 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(LRAT and GRAT were developed independently for certified DRAT checking, both published at CADE 2017; LRAT is Cruz-Filipe, Heule, Hunt, Kaufmann, Schneider-Kamp; GRAT is Lammich) < 1570967042 515175 :int-e!~noone@int-e.eu PRIVMSG #esoteric :"amost as fast as gratgen" - yeah I thought that gratgen looked very good, performance wise. < 1570967275 673174 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :in any case I think emitting an LRAT/GRAT like proof directly from the solver is quite a bit faster than conversion from DRAT, the biggest downside is that it is quite a bit larger than a DRAT proof, but if you're not interested in storing the proof you could run the verifying concurrently to avoid that < 1570967396 904541 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :I might need to implement that for a competitive solver, though, if I want to convince people of that < 1570967526 28272 :int-e!~noone@int-e.eu PRIVMSG #esoteric :jix: Hmm, how well does the unsatisfiable core computation work though? < 1570967572 552986 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :int-e: haven't checked that yet, it's possible, but it'll probably generate larger cores because there is no core-first propagation or anything like that < 1570967615 319855 :jix!~jix@209.250.235.106 PRIVMSG #esoteric :if you use iterative solving to minimize the unsat core (like Heule did for the chromatic number of the plane problem), you can iterate faster, so it'd be interesting to compare it in that setting < 1570967663 931606 :int-e!~noone@int-e.eu PRIVMSG #esoteric :jix: Yeah I'm basically asking a research question... the answer can't be determined without trying, I think. I certainly don't have the intuition for it. < 1570968797 95553 :atslash!~atslash@46.188.0.82 QUIT :Ping timeout: 240 seconds < 1570968818 373475 :atslash!~atslash@static.231.107.9.5.clients.your-server.de JOIN :#esoteric < 1570969260 943140 :Amiona!5a8d8d14@m90-141-141-20.cust.tele2.se JOIN :#esoteric < 1570969558 66676 :Amiona!5a8d8d14@m90-141-141-20.cust.tele2.se PRIVMSG #esoteric : Chat 40+ -> https://soo.gd/room40plus < 1570971145 963932 :Amiona!5a8d8d14@m90-141-141-20.cust.tele2.se QUIT :Remote host closed the connection < 1570972521 773806 :Sigyn!sigyn@freenode/utility-bot/sigyn QUIT :*.net *.split < 1570974741 590975 :Sigyn!sigyn@freenode/utility-bot/sigyn JOIN :#esoteric < 1570974741 738005 :Sigyn!sigyn@freenode/utility-bot/sigyn QUIT :Excess Flood < 1570974997 601846 :Sigyn!sigyn@freenode/utility-bot/sigyn JOIN :#esoteric < 1570974997 681820 :Sigyn!sigyn@freenode/utility-bot/sigyn QUIT :Excess Flood < 1570975019 595331 :Sigyn!sigyn@freenode/utility-bot/sigyn JOIN :#esoteric < 1570975019 631545 :Sigyn!sigyn@freenode/utility-bot/sigyn QUIT :Excess Flood < 1570975308 565364 :Sigyn!sigyn@freenode/utility-bot/sigyn JOIN :#esoteric < 1570975308 641655 :Sigyn!sigyn@freenode/utility-bot/sigyn QUIT :Excess Flood < 1570975330 566929 :Sigyn!sigyn@freenode/utility-bot/sigyn JOIN :#esoteric < 1570975332 200730 :Sigyn!sigyn@freenode/utility-bot/sigyn QUIT :Read error: Connection reset by peer < 1570975465 626564 :Sigyn!sigyn@freenode/utility-bot/sigyn JOIN :#esoteric > 1570976441 214532 PRIVMSG #esoteric :14[[07Deadfish~14]]4 M10 02https://esolangs.org/w/index.php?diff=66648&oldid=66647 5* 03A 5* (+106) 10/* Implementation */ < 1570976583 868239 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru JOIN :#esoteric < 1570976962 627313 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :When was the first emoji used in #esoteric? 🤔 < 1570977111 716225 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :tswett[m]: probably before 2003 < 1570977352 996251 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :When did emoji become "a thing," anyway? I seem to remember it was relatively recently that they were implemented on iOS and Android and subsequently (pretty much immediately) became popular in the US. < 1570977365 744038 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :"Relatively recently" as in within the past 5 years. < 1570977792 304752 :int-e!~noone@int-e.eu PRIVMSG #esoteric :'Originating on Japanese mobile phones in 1997, emoji became increasingly popular worldwide in the 2010s after being added to several mobile operating systems.' < 1570977799 973974 :int-e!~noone@int-e.eu PRIVMSG #esoteric :<3 wikipedia. < 1570977845 384 :int-e!~noone@int-e.eu PRIVMSG #esoteric :'The first ASCII emoticons, :-) and :-(, were written by Scott Fahlman in 1982, but emoticons actually originated on the PLATO IV computer system in 1972.' (ditto) < 1570977931 423140 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Nyope. Looks like iOS got support for emoji in 2011, much longer ago than I thought. < 1570978080 347036 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Unicode version 6.0, 2010, added those to Unicode. < 1570978082 493944 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :tswett[m]: when did it get support for animated emoji? < 1570978328 965950 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :soon we'll have animated emoji with sound and smell < 1570978363 134330 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :and modifiers for whether the man blowing a raspberry emoji or the crying face emoji are supposed to be rendered with sound on or muted < 1570978412 200138 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :and a singing voice modifier that changes the default tenor voice to a bass < 1570978935 799791 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :Pretty sure those, well, aren't really emoji. < 1570978949 883588 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :not yet < 1570978951 532750 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :They're pictures being sent, not Unicode strings < 1570978965 188964 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :(animoted emoji, I mean) < 1570979139 806817 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I remember animated fonts on VGA... > 1570979460 907681 PRIVMSG #esoteric :14[[07User talk:Palaiologos14]]4 N10 02https://esolangs.org/w/index.php?oldid=66649 5* 03Palaiologos 5* (+0) 10Created blank page < 1570981067 547172 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :int-e: EGA was the first to support those, wasn't it? < 1570981113 841592 :int-e!~noone@int-e.eu PRIVMSG #esoteric :tswett[m]: I'd have to check. I've never had an EGA myself. < 1570981277 94618 :clog!~nef@bespin.org QUIT :Ping timeout: 240 seconds < 1570981415 407762 :int-e!~noone@int-e.eu PRIVMSG #esoteric :tswett[m]: I still don't know, but at least it's very plausible that EGA supported this trick :) < 1570981511 83156 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :darn it! the windows were open so the beeping sounded like it was coming from the outside. it took me two minutes to realize that it was my own oven alarm < 1570981611 437565 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1570981637 35735 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 240 seconds < 1570981783 664035 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1570982035 786108 :kspalaiologos!~kspalaiol@176.221.122.71 JOIN :#esoteric < 1570982128 617800 :int-e!~noone@int-e.eu PRIVMSG #esoteric :. o O ( who doesn't like charred pizza ) < 1570982300 700535 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :charred pizza is profanation of pizza < 1570982318 417368 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :once in my life I've been to Venice, there was a guy selling pizza slices < 1570982321 800801 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :one slice was arm-length < 1570982346 781252 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :the slice overall was very moist with a lot of olive oil < 1570982405 637129 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :luckily it's not pizza < 1570982414 509667 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :and not charred < 1570982492 256903 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :[ 16*12*0.0254 < 1570982493 5251 :j-bot!eldis4@firefly.nu PRIVMSG #esoteric :b_jonas: 4.8768 < 1570982578 937942 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1570983179 313030 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :int-e: Well, EGA definitely supported (the appearance of) animated fonts. < 1570983187 122076 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Hecc, I should get an EGA. < 1570983220 815202 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Hook it up to my IBM PC. < 1570983225 696055 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :But first I'll have to get an IBM PC. < 1570983243 962639 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :One with an 8080 processor, I don't want none of this protected mode nonsense. < 1570983787 58256 :imode!~linear@unaffiliated/imode PRIVMSG #esoteric :8080's are pretty cheap, you could just build one. < 1570983901 599202 :int-e!~noone@int-e.eu PRIVMSG #esoteric :tswett[m]: don't you at least want a proper 16 bit data bus though? < 1570983937 740500 :clog!~nef@bespin.org JOIN :#esoteric < 1570983939 84182 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I mean, you already have 16 bit registers. < 1570983955 916263 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Hmmmm, perhaps. < 1570984769 339405 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :tswett[m]: https://monotech.fwscart.com/NuXT_MicroATX_Turbo_XT_955MHz_832K_RAM_XTCF_SVGA_Floppy_Serial/p6083514_19777986.aspx ? < 1570984793 204806 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :(not the literally ideal solution for all use cases of this sort of thing mind, but it is a very pleasant product) < 1570984850 615854 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :pikhq: Ooh, sweet! < 1570984889 192556 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :Right? < 1570984919 390301 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :I imagine stock is never gonna be _super_ common, cause it's very much a cottage-industry thing _and_ some of the components are new-old-stock, but < 1570985192 186698 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :On the other hand, while trickier to get _most_ of what makes that nice can be cobbled together with other off-the-shelf things. < 1570985239 198339 :pikhq!uid394595@gateway/web/irccloud.com/x-putygvflmnyxxsta PRIVMSG #esoteric :(just less all-in-one) < 1570986119 7904 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric : oh I see. the "955MHz" in the url was confusing. it's "9.55 MHz" rather than "955 MHz". < 1570986773 38784 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :That's fast enough to run a stock exchange. :D < 1570987074 887579 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Damn it, now I'm all thinking about writing stock exchange software for an online game. < 1570987093 405019 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Psst, I'm writing an online game. Currently, you can log into the game, and see how much of various commodities everyone has. < 1570987122 807863 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Currently it is not possible to gain more commodities, or to do anything with the commodities you've got. < 1570987164 31944 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :nothing is fast enough to run a stock exchange. those people are crazy, they put computers in the middle of the Atlantic just so they can speculate a few milliseconds earlier when their choice depends on information from both European and American stock exchanges. < 1570987176 723561 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :it's ridiculous < 1570987294 238701 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Yeah, high-frequency trading is a weird thing. < 1570987319 432758 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :I mean, I don't work in financial areas, and admittedly the areas where I work are crazy in other ways, < 1570987502 761050 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Theoretically, traders provide a valuable service. < 1570987537 200008 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :I want to be able to buy and sell goods, services and capital at prices that reflect their fair market value. < 1570987574 481418 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :right, they provide the grease that reduces the friction of the market < 1570987585 798015 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :So if someone puts effort into providing that for me, they deserve a bit of return for their effort. < 1570987602 770736 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :they do get their return in the form of money < 1570987621 557409 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Right < 1570987631 667599 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :`? tinfoil hat < 1570987632 774120 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :tinfoil hat? ¯\(°​_o)/¯ < 1570987667 331277 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :But there's presumably a point where it stops being "they get money in exchange for providing a valuable service" and starts being "they get money for being better at poker than everyone else." < 1570987744 862433 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :I'm not sure that's separable. they provide the valuable service by being good at poker. < 1570987828 204043 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Well, in actual poker, the good poker players aren't really providing a valuable service to the bad poker players. < 1570987861 922119 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Just like if I go into a casino and count cards, the casino pays me money, but it's not because I'm providing a valuable service to the casino. < 1570987900 794570 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Golly. Instead of pointless gambling, people should be able to bet on real things, and thus provide a valuable service to the world. < 1570987951 838803 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :as in on the stock market? < 1570987996 219194 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Well, stock betting is already mostly legal, and it's useful but it's not the only useful market. < 1570988030 138134 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I think mostly arbitrary prediction markets should be generally legal in the US, except one special one. < 1570988045 369189 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :or they pretend it's mostly legal, because if we could find out what specific illegal thing they do, the authorities would punish them < 1570988063 613870 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What do you mean? < 1570988090 233916 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :how about the intermediate stuff, betting on sports? < 1570988108 284295 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Sports betting seems pretty useless to me, but probably a bit better than casinos. < 1570988176 61360 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :sports betting seems pretty popular here, among people who I think don't have any comparative advantage in the bets, so it's just a game of chance, paying for the thrill or something < 1570988184 405445 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :I don't understand how it's so popular < 1570988204 969099 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It's kind of odd which things are legal to bet on in the US. < 1570988229 543888 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :For example you can bet on the weather. < 1570988267 316526 :FaeFly!znc@freenode/staff/firefly PRIVMSG #esoteric :what things aren't legal to bet on? < 1570988355 905392 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Arbitrary events. < 1570988366 764325 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :the tricky part of the legal rules (IANAL) is not just what you can bet on, but how you pay income tax after them. it's pretty clear that if you win all your bets, then all that you gain on them is your income. < 1570988421 749201 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :but if you win one bet and lose another bet, then is it a transaction as a whole and your income is the difference, or is the winning bet your income and the losing bets your spending so your income is what you win on the former? < 1570988425 714955 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Except for predictit.org and apparently something in Iowa, which are still not legal but allowed to run anyway? < 1570988445 382924 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :there are some rules on that, but of course there are so many, often illegal, new forms of betting, that they can't cover it all < 1570988448 499931 :FaeFly!znc@freenode/staff/firefly PRIVMSG #esoteric :I guess the UK is more permitting than the US wrt betting on arbitrary events, then < 1570988453 647589 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :and it's even harder to enforce it < 1570988459 186389 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :b_jonas: The answers to these questions are well-established for other trading, so it doesn't seem like a problem. < 1570988478 351658 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I mean, if you're betting secret and illegally it's hard to enforce, but the law is reasonably clear. < 1570988496 920622 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Yes, the UK is more permitting. < 1570988507 957160 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Except in the UK you have to use inscrutable words like "back" and "lay". < 1570988517 248488 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :right. and since games of chance are so severely regulated here, almost everyone who earns a signifiacnt amount do it illegally < 1570988524 785655 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Once in a while I figure out what they mean but the next time I want to look at a market I've forgotten again. < 1570988572 562041 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :ah, jargon < 1570988594 134089 :FaeFly!znc@freenode/staff/firefly PRIVMSG #esoteric :Usually the UK brokers let you bet on whether you think arsons will torch the Gävle straw goat or not < 1570988603 55554 :FaeFly!znc@freenode/staff/firefly PRIVMSG #esoteric :(speaking of being able to bet on arbitrary events) < 1570988655 551541 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :FaeFly: they always do, the bet is only about when < 1570988667 482645 :FaeFly!znc@freenode/staff/firefly PRIVMSG #esoteric :hehe < 1570988682 81090 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Anyway my point is just that actual markets are useful for the world, whereas casinos are not. < 1570988692 46419 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :oh right, as for goats < 1570988694 902284 :FaeFly!znc@freenode/staff/firefly PRIVMSG #esoteric :(nah, there's been years when it hasn't been, but the majority of the time it seems to be) < 1570988717 148628 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So if people are going to get the gambling thrill anyway, better for them to lose money on actual markets, to incentivize counterparties to do research or something. < 1570988717 228331 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: I thought running a casino is great for making money? < 1570988737 968602 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Yes, casinos are useful for the owners and not anyone else. < 1570988759 964377 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Markets are useful for everyone. < 1570988765 2274 :int-e!~noone@int-e.eu PRIVMSG #esoteric :hah < 1570988770 26010 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :you know how Gävle has goats, and Budapest used to have these painted cows at one point? on my vacation, I found that Dortmund had painted _winged_ _rhinoceroses_. < 1570988779 718117 :FaeFly!znc@freenode/staff/firefly PRIVMSG #esoteric ::D < 1570988791 952418 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: grocery markets, maybe < 1570988801 543026 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Grocery futures! Good idea. < 1570988821 610036 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Exotic grocery futures options derivatives. < 1570988826 171805 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Been done for cocoa... < 1570988838 606044 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, another thing that's illegal in the US is onions future. < 1570988852 666118 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But that's an explicit exception for onion, most kinds of futures are legal. < 1570988871 432340 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :for onions < 1570988885 111159 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Well you learned the right lesson from the Tulip crisis. < 1570988897 141975 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Those are a kind of onion, right?) < 1570988897 325850 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :int-e: nah, they don't really work. the agriculture guys figured out that they don't have to pay for insurance, they just tell the government every year that this year has been the worst weather ever since their life and there's no way they could have been prepared for it and the government has got to pay them subsidy to help them < 1570988908 530037 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :you can't compete with that < 1570988912 636315 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :Yeah, ban bulb speculation! < 1570988971 51737 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I'd like onion futures to be legal. Maybe I can write my congresshumans. < 1570989045 985897 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: is this like those rules that get compiled to stupid law compilations on the internet, like laws about not being allowed to park an elephant close to a school or something? < 1570989070 860049 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It's this law: https://en.wikipedia.org/wiki/Onion_Futures_Act < 1570989137 680701 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It was later amended to ban box office receipts futures (bets on how much money a movie will make). < 1570989168 487043 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I think the law is just bad. As far as I know onion farmers agree nowadays. < 1570989224 513456 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: It's certainly a ridiculous piece of legislation. I'm all for such a ban but limiting it to onions is ridiculous and short-sighted. < 1570989235 95746 :int-e!~noone@int-e.eu PRIVMSG #esoteric :A ticking time bomb. < 1570989244 484896 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(No, I'm not a big believer in capitalism. Why do you ask?) < 1570989288 832486 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Yes, I know that. That's why I'm taking the contrarian view point, obviously. < 1570989289 788173 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(More to the point I believe that free markets have optimize the wrong objective function.) < 1570989301 888425 :int-e!~noone@int-e.eu PRIVMSG #esoteric :s/have// < 1570989308 779585 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Sure, I agree on that. < 1570989322 319936 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Well, I don't know what right and wrong objective functions you have in mind. < 1570989338 101343 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But I also don't know what's better. It's easy to name shortcomings in markets. > 1570989361 768890 PRIVMSG #esoteric :14[[07Photon14]]4 10 02https://esolangs.org/w/index.php?diff=66650&oldid=63463 5* 03Sugarfi 5* (+0) 10 < 1570989545 901119 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: that looks crazy, and I think it's an example of exactly what I said above, that agriculture people can put on a great innocent small child face with the puppy eyes and tell the congress that they're being unfairly exploited by the evil stock trade people, and then the congress does anything they ask for < 1570989586 45337 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :and if they don't, then the agriculture people pour milk and throw watermelons at them, and the politicians get afraid that their beautifully tailored suits will get spoiled, and so they give in < 1570989594 380816 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I don't have a feasible, stable solution either. (For example, socialism is a great idea, but putting it into practice is really hard... you're likely to end up with corruption everywhere, and quite possibly an unmotivated workforce.) < 1570989596 348276 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I mean, they *were* unfairly exploited by futures traders. < 1570989661 151447 :int-e!~noone@int-e.eu PRIVMSG #esoteric :In practice, timely regulation is probably the best to hope for. < 1570989676 408656 :tswett[m]!tswettmatr@gateway/shell/matrix.org/x-pgmmudzojockohut PRIVMSG #esoteric :The free market is great as long as the market value of every person's labor exceeds the market value of the goods and services necessary for that person's well-being. < 1570989683 954842 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: OK, sure, it sounds like we agree on that. < 1570989703 344760 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :A big point of the whole market thing is that incentives line up well. < 1570989719 32710 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Regulation is also the key to internalizing external costs, especially from the future. < 1570989722 666080 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :And you certainly want regulation rather than "free markets" which can easily be pathological. < 1570989737 760193 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Right, and you want to internalize externalities. < 1570989770 444936 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Basically, since we don't know anything better than the free market model that is also stable in the medium and perhaps even long term, we have to resort to tweaking the cost function. < 1570989849 568452 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Of course it's all embedded in a prisoner's dilemma between countries because for most things we have a global market. < 1570989963 979919 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(The background problem I'm considering is limiting climate change. It's one of the truly big challenges where in theory, it should be in everybody's interest to work really hard towards a solution, including accepting lowered standards of living for the few for the benefit of the many and future generations. In practice... I don't see any of that happening fast enough to matter.) < 1570990036 929175 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Cornering markets, as nasty as that is... seems minor in comparison. < 1570990108 345006 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Limiting climate change is good but a particular government can add regulation for externalities however market-oriented it is. < 1570990119 513410 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :And the inter-government issues are no different. < 1570990475 412870 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :this channel is weird. SAT solvers in the morning, free market in the evening < 1570990526 696906 :int-e!~noone@int-e.eu PRIVMSG #esoteric :we've also seen ootsology, meditation, and actual spam < 1570990557 891879 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: Anyway, I don't think we disagree on any of the facts, so I think it's odd that you end up thinking futures should be illegal and I don't. < 1570990643 507164 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :`8-ball should futures be illegal? < 1570990644 170139 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :Better not tell you now. < 1570990664 98124 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :fungot, what restrictions do you recommend to put on the free market? < 1570990664 438539 :fungot!~fungot@unaffiliated/fizzie/bot/fungot PRIVMSG #esoteric :b_jonas: designing an os -and- playing tabletop.... i'm kinda thinking specifically of http and other stateless protocols... and dynamic ip addresses. but i can't < 1570990674 823978 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :um < 1570990724 390005 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: If you put it like that I'm not sure about whether they should be illegal. I don't think they are useful, and I dislike some of the consequences (cornering markets is most attractive in the presence of futures, isn't it...) < 1570990779 66611 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm, I think futures are useful for reducing uncertainty and transferring risk from people who have it to people who want it. < 1570990815 808508 :int-e!~noone@int-e.eu PRIVMSG #esoteric :that's the trouble, isn't it < 1570990832 337797 :int-e!~noone@int-e.eu PRIVMSG #esoteric :hedging risks is great, speculation is bad, and there's no discernable differencw < 1570990835 290522 :int-e!~noone@int-e.eu PRIVMSG #esoteric :e < 1570990863 932243 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Why is speculation bad? < 1570990881 891032 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :(Speculation can also be done without futures, of course.) < 1570990884 556974 :int-e!~noone@int-e.eu PRIVMSG #esoteric :it's bad when combined with bankruptcy < 1570990907 850117 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Because then you're in an ugly external cost scenario. < 1570990927 16921 :int-e!~noone@int-e.eu PRIVMSG #esoteric :
ACTION shrugs.
< 1570990951 3612 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru PRIVMSG #esoteric :oh at first I thought about futures like promises < 1570990971 273955 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Yes. I promise to buy ... shares at price ... in the future. < 1570990972 472853 :int-e!~noone@int-e.eu PRIVMSG #esoteric ::P < 1570990972 856406 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :That's arguable, but often it's addressed anyway. < 1570990975 27087 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru PRIVMSG #esoteric :now I see this is economical stuff I don’t know anything about < 1570990995 179622 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I think speculation clearly has a useful function too. < 1570991021 932797 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :and that's still greasing the market? < 1570991025 301025 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru PRIVMSG #esoteric :though I don’t really distingwish promises and futures too, I hadn’t read anything comprehensive to date about them all < 1570991027 356985 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :If I buy wheat when it's cheap (low demand) and sell it when it's expensive (high demand), I've transferred wheat from people who don't need it to people who do. < 1570991050 173162 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :right, greasing the market, even though wheat in particular isn't greasy < 1570991060 112014 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I get paid for it because the people who need it are willing to pay because it's so useful to them. < 1570991067 94414 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :That seems cleary useful. < 1570991098 663715 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: presumably you've also paid for storage. except... nowadays... that's not so clear at all < 1570991110 386390 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru PRIVMSG #esoteric :. o O ( my market is all floury on the floor, who did it ) < 1570991124 63993 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Nowadays you might've paid someone else for storage, sure. < 1570991191 412726 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :presumably if the grain travels time then someone payed for its storage somehow < 1570991199 657583 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :because no free launch < 1570991210 427483 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Right. < 1570991241 469866 :int-e!~noone@int-e.eu PRIVMSG #esoteric :or maybe there is no grain < 1570991298 133544 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :you mean it got to the future the old style way, by having planted seeds a few months before you need it, and then harvesting at the right time, so it doesn't need to be stored?? < 1570991313 50214 :int-e!~noone@int-e.eu PRIVMSG #esoteric :it's futures -> short-selling -> cornering markets -> disaster. :P < 1570991358 228309 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru PRIVMSG #esoteric :BTW I watched those slides on GA and I wonder how can it be explained transparently than in PGA, you represent points by (n−1)-vectors, lines by (n−2)-vectors and so on and hyperplanes by 1-vectors, all in reverse to the way they’re represented in usual projective space context < 1570991384 680758 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I feel like you're focusing on a few extremely bad failure cases -- which are generally illegal anyway -- and not on the constant benefits everyone gets. < 1570991408 969413 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :it's not a _disaster_, it's just another stupid zillion dollars lots of government subsidies, because the agriculture sector knows that puppy eyes are cheaper than taking any risk or behaving like they're part of a world economy where maybe it's not worth for them to grow watermelons at all because shipping them all the way from brazil is cheaper < 1570991421 843464 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: because "everyone" is concentrated in the top 1%. < 1570991440 157091 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I don't think that's true. < 1570991468 776581 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I think it's born out by the capital distribution and its changed distribution over time. < 1570991477 967286 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Wheat farmers get the benefits of wheat futures, because they can reliably know what prices they'll sell their wheat at before it's grown, so they can plan better. < 1570991512 863971 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru PRIVMSG #esoteric :(^cont.) (representing them the usual way gives something paranormal but why the reverse works is not automatically clear) < 1570991526 332352 :int-e!~noone@int-e.eu PRIVMSG #esoteric :but wouldn't they be better off if they had sufficient money floating to hedge those risks themselves... < 1570991529 833882 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Sure, I think there are clearly problems causing wealth to be concentrated among a small number of people to a ridiculous degree. But I don't think derivatives are the cause. < 1570991536 697629 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Why? < 1570991554 722151 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I buy insurance rather than hedging tail risks myself. < 1570991593 669329 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I think in some cases insurance makes sense and in some cases it's ridiculous, but the concept surely makes sense. < 1570991619 359971 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: right, that's more than half the point of insurance < 1570991632 643538 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :(Ridiculous: US health insurance.) < 1570991634 405121 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So you should cover normal fluctuations using your own capital and tail risks by a proper insurance? < 1570991651 432204 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: oh yeah, that one is weird < 1570991653 267269 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I don't see where you need futures in this picture. < 1570991682 320208 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :You should be able to transfer whatever risks you want to people who want to buy them. < 1570991709 627445 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :or hmm < 1570991786 938090 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :No one is forcing wheat farmers to use futures. If they want to hedge tail risks only they can do that too (and people also trade wheat options, but I imagined you'd have even more of an objection to those). < 1570991795 357521 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :well, there's also cases when the government mandates you to buy insurance, most importantly (a) when you're driving motor vehilcles, you must buy insurance to pay to the people you kill by accident, and (b) if you run a travel agency, you must buy insurance to transport the travelers back home < 1570991829 477902 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :`? trigak < 1570991830 560487 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :trigak? ¯\(°​_o)/¯ < 1570991874 951458 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :`? serini < 1570991876 52512 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :serini? ¯\(°​_o)/¯ < 1570991888 56894 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :what look, trigak and serini look just the same according to the wisdome < 1570997380 751704 :kspalaiologos!~kspalaiol@176.221.122.71 QUIT :Quit: Leaving < 1570997650 815242 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I often hear backjumping described as a big improvement, but is it actually that important? < 1570997683 275518 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :With your learned clause, even if you didn't backjump but only went up one level, the new clause would give you a conflict via unit propagation anyway, right? So you wouldn't end up making any new decisions. < 1570999230 876230 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :b_jonas: https://twitter.com/ioccc/status/1183476350847336453 < 1570999279 453800 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :ooh, this will be interesting < 1570999287 767466 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: ioccc? let me see < 1570999322 640919 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: The point of backjumping is that you undo decisions that were made after a point where the newly learned clause could be used for unit propagation. < 1570999361 661347 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: It's not an unconditional win, but heuristically you want to do as much unit propagation as possible before making a decision. < 1570999368 830269 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :b_jonas: It's only a pre-update. < 1570999449 488299 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: You can think of it as a partial restart, maybe? < 1570999465 149249 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :majority opposition win in Bp < 1570999513 945400 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: I mean, clearly backjumping is good, but if you didn't do it, unit propagation alone (and no decisions) would unwind you to the same point. Right? < 1570999514 914213 :LKoen!~LKoen@81.255.219.130 QUIT :Read error: Connection reset by peer < 1570999544 595854 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: well, sooner or later... < 1570999577 676882 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: actually, no, it's incomparable < 1570999595 745271 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: I know it's not the final results yet, but it won't change significantly at this point < 1570999608 397469 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: if ordinary backtracking returns to that point, the negated literal corresponding to that decision will end up on the trail, then the backjump literal. < 1570999661 663855 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: I'm pretty sure this is one of those ideas that are completely unclear in theory but work out well in practice. < 1570999684 315535 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Aka a heuristic ;) < 1570999763 287584 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :shachaf: yes, that's probably not worth an ioccclist trigger < 1570999766 272075 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :`? ioccclist < 1570999767 330933 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :ioccclist is update notification for when a new year of the International Obfuscated C Code Contest is announced, or the winners for a year is announced, or the source codes of winners are released. http://www.ioccc.org/#news < 1570999779 30440 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: oh what do you mean by "unwind"... only backtracking or backjumping really unwinds anything; everything else expands the trail. < 1570999780 767637 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :it doesn't even appear on the news page < 1570999921 290741 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :hey SDR nerds, can anyone identify this encoding scheme? < 1570999929 478582 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :https://usercontent.irccloud-cdn.com/file/o3noKYIX/Screenshot%202019-10-13%2014.51.44.png < 1570999933 425727 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :https://usercontent.irccloud-cdn.com/file/G4qGBD9F/Screenshot%202019-10-13%2014.50.47.png < 1570999973 565882 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :it's not manchester... the thing i noticed is each high is only ever 1 symbol length but the low intervals are either 1 or 2 < 1571000016 360902 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :so a transmission is variable length depending on how many 0s or 1s there are? < 1571000040 528761 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :j4cbo: that could happen, there's at least one encoding scheme that is variable length like that < 1571000056 169319 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :of course there could be a layer over it that changes what comes out as zeroes and ones < 1571000064 297170 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :https://usercontent.irccloud-cdn.com/file/qoPjGUGh/Screenshot%202019-10-13%2014.53.51.png < 1571000079 546175 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :j4cbo: but isn't it also possible that you have too few samples and sometimes the high can be 2 long too? < 1571000099 298031 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :that is possible < 1571000118 432666 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :i'm trying to reverse-engineer my cheap-ass wirelessly controlled christmas lights < 1571000153 167091 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :i have a remote control dongle with three buttons (toggle power, change pattern, and 'sync' which restarts the current pattern) so... those are the only three samples i'm gonna get :P < 1571000156 700859 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :see https://en.wikipedia.org/wiki/1-Wire which is variable length like that < 1571000165 45310 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :but with different timing < 1571000172 173029 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :then it's OOK over 433mhz < 1571000188 148769 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :i'm kind of hoping the receive device supports discrete on and off commands < 1571000190 917109 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :do you always get the same sample from the same button? < 1571000227 630443 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :yep < 1571000234 413333 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :well that's promising < 1571000243 355561 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :it just plays over and over again while the button is held down < 1571000265 168166 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :send it lots of random nonsense quickly and hope that does something? < 1571000281 34233 :zzo38!~zzo38@24-207-15-213.eastlink.ca PRIVMSG #esoteric :Could you implement on/off by the power connection instead if needed? < 1571000323 80976 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :totally, but that requires extra hardware :P < 1571000335 403600 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :j4cbo: these only have, like, 17 bits of info at most, so try all 2**17 combinations < 1571000352 483514 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :some of them will probably be ignored < 1571000388 363448 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :yeah, i need to rig up some code to send those words out from my own hardware next < 1571000408 781009 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :are these sent by radio or by infrared? < 1571000418 950882 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :radio, 433mhz OOK < 1571000483 903526 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :hmm, that might be harder < 1571000533 661043 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :i have a spare rileylink < 1571001103 969932 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: I think I'm confusil about something but I don't want to type it on my phone so I'll try to say more later. < 1571001129 984749 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :By unwinding I mean regular backtracking, i.e. only subtracting 1 from the level. < 1571001732 208848 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: Right. Then I think I've understood correctly... and perhaps answered your question as well. < 1571002240 689493 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: Back at computer. < 1571002294 323231 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :strangely, the word "confusil" doesn't appear in quotes or wisdom ... yet < 1571002305 732497 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :int-e: Whether you backtrack or backjump to a point earlier in the trail, you should have the same state, shouldn't you? < 1571002363 686267 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: No, because the backtracking will leave an additional literal on the trail. < 1571002371 607683 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I mean the same trail state. Your learned clauses might be different. < 1571002381 577989 :b_jonas!~x@catv-176-63-24-44.catv.broadband.hu PRIVMSG #esoteric :sorry I don't make more constructive conversation, but SAT solvers really isn't a topic I feel interested about < 1571002384 647010 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: before unit propragation with the learned clause kicks in. < 1571002420 362543 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Wait, backtracking only deletes everything past some point in the trail, doesn't it? < 1571002456 79838 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So at the time you unwind to any past level k, you've deleted everything past k in the trail. < 1571002459 86767 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: backtracking takes deletes the trail up to the last decision, and places the negated decision literal on the trail < 1571002488 331580 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :When you say "that point" what do you mean? < 1571002511 943042 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I feel like I should just draw a diagram and the confusilation would be resolved in eight seconds. < 1571002530 395067 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: "that point" meaning the position of the decision literal that backjumping would replace on the trail. < 1571002624 651197 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Say you have a,b!,c,d,e!,f,g!,h,i on the trail, where the !ed literals are decisions and the rest are a result of unit propagation. < 1571002658 956302 :arseniiv!~arseniiv@95.105.7.27.dynamic.ufanet.ru QUIT :Ping timeout: 240 seconds < 1571002659 830607 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :You reach a contradiction and you add a clause, which would let you backjump to replace e. Right? < 1571002660 344652 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: if you have 1 2^d 3 4 5^d 6 7, a conflict, with learned clause -1,-7... then backjumping results in 1 -7 as the new trail, whereas if you continue the search until 2^d is removed by backtracking, you'll end up with 1 -2, and then unit propagation will add -7. < 1571002667 704582 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: ^d marks decisions. < 1571002692 44338 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Aha. < 1571002700 499831 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Now I see what you mean. Thanks. < 1571002848 118695 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So one of the important things about CDCL is that the only thing the learned clauses are any use for is unit propagation. Right? < 1571002869 593869 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :So you want them to be as small as possible if you can manage it, or otherwise as relevant as possible within your assumptions. Or something like that. < 1571002878 15304 :int-e!~noone@int-e.eu PRIVMSG #esoteric :. o O ( just like any other clauses ) < 1571002907 321447 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :No, the original clauses are useful for specifying your problems. < 1571002918 601722 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :The new clauses are redundant and only useful if they make unit propagation happen. < 1571002932 470231 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I'm just saying something very obvious here. < 1571002934 991685 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Right. < 1571002946 220761 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Actually there's a point here. < 1571002970 457405 :int-e!~noone@int-e.eu PRIVMSG #esoteric :SAT solvers also prune the clause database (they forget clauses), and that's only allowed for clauses that are redundant. < 1571002989 715804 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Which means that in most cases, they will only forget learned clauses. < 1571002992 744195 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Do they even forget original problem clauses? < 1571003029 84970 :int-e!~noone@int-e.eu PRIVMSG #esoteric :There are simplification procedures (I know nothing about them really except that they exist) which can also identify redundant clauses. < 1571003036 580688 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I thought the main reason to forget clauses was to save memory, and otherwise having a bunch of clauses doesn't hurt. < 1571003040 959849 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But, sure, simplification makes sense. < 1571003051 963362 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Or potentially rewrite clauses (add some clauses that make other clauses redundant while maintaining satisfiability) < 1571003123 744555 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :One of the slightly odd things about CDCL is that you have to use full clauses, rather than the reduced clauses you get after assuming some literals. Right? < 1571003166 296240 :int-e!~noone@int-e.eu PRIVMSG #esoteric :You mean wrt the current trail? < 1571003170 178596 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I mean, if you have the clause (a | b | c), and you assume ¬b, you sometimes think of it as solving the subproblem where you have the clause (a | c). < 1571003188 539722 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But your learned clauses have to be globally true so you can't really talk about subproblems like that. < 1571003212 559107 :int-e!~noone@int-e.eu PRIVMSG #esoteric :If you ever want to go back on that assumption and keep the learned clauses valid... yeah you'll need full clauses. < 1571003221 973356 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So in particular that's true for everything on the trail. < 1571003267 123634 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But I think that's not so bad because even if you learn a big clause, while you're in the same region (sharing most of the trail) it'll still be locally pretty small and so useful for unit propagation. < 1571003314 66027 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :When your trail looks very different after a while, the big clause might be less useful, and you might be more inclined to forget it. < 1571003354 645456 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Also learning is completely optional... a SAT solver can just refuse to learn clauses above a certain size. < 1571003376 10901 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Right. Without learning a CDCL solver is still correct, which is good. < 1571003412 627478 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Maybe you can just use big clauses for backjumping without learning them? Not sure how useful that would be. < 1571003421 90054 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Actually it's kind of awful too... you have so many degrees of freedom for heuristics... < 1571003478 2243 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Which literal to decide on, what to learn, what to forget, when to restart... < 1571003504 521305 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Restarting seems like a surprising strategy to me. Especially a solver (BerkMin) that restarts every 550 conflicts?! < 1571003520 438590 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Do restarting solvers have any guarantee of termination? < 1571003544 500887 :int-e!~noone@int-e.eu PRIVMSG #esoteric :They are supposed to do some sort of (exponential?) backoff... < 1571003580 844505 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But this interacts in interesting ways with learning. < 1571003610 616066 :int-e!~noone@int-e.eu PRIVMSG #esoteric :If you learn all backjump clauses and never forget then even if you restart after every conflict you'll eventually solve the problem. < 1571003641 532962 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, because everything slowly becomes forced by UP. < 1571003652 703252 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(this is degenerate... you'd have a conflict, analyse it to find the backjump clause, learn that clause, but never actually backjump because you're restarting anyway) < 1571003978 487040 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The other intuitive reason for restarts is that initially the variable selection heuristic has no information at all... with a restart, even early decision levels can benefit from the variable selection heuristic. < 1571004053 623203 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I suppose this is especially important for satisfiable problems. < 1571004555 82069 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Why is unit propagation the only thing used for assigning values to variables, other than decisions? < 1571004833 587484 :int-e!~noone@int-e.eu PRIVMSG #esoteric :because it's fast? < 1571004897 225401 :int-e!~noone@int-e.eu PRIVMSG #esoteric :And I guess the attitude is that all other inferences can be learned as clauses. < 1571005179 37253 :int-e!~noone@int-e.eu PRIVMSG #esoteric :IIRC the original DPLL had a "pure literal" rule... if a literal only occurs positively in the current set of clauses (those that are not already true) then one can assert that literal to be true. Nobody implements this as part of the propagation rules. < 1571005311 186827 :int-e!~noone@int-e.eu PRIVMSG #esoteric :If you're facing a decision like... "would you rather do X or 1k unit propagations" < 1571005343 791049 :int-e!~noone@int-e.eu PRIVMSG #esoteric :it's easy to imagine that X probably won't pay off :) < 1571006951 33224 :j4cbo!sid186930@gateway/web/irccloud.com/x-rhlvmgrmtzwmpdca PRIVMSG #esoteric :boo, i need an SDR < 1571007795 598434 :xkapastel!uid17782@gateway/web/irccloud.com/x-wpmssffdsnzgzmsg JOIN :#esoteric < 1571010095 431361 :Hooloovo0!Hooloovoo@sorunome.de QUIT :Ping timeout: 265 seconds