←2019-10-12 2019-10-13 2019-10-14→ ↑2019 ↑all
00:48:03 -!- oerjan has joined.
00:57:12 <esowiki> [[Keg]] https://esolangs.org/w/index.php?diff=66643&oldid=66634 * JonoCode9374 * (+25) /* Swap the words good and bad */
01:04:21 -!- imode has quit (Ping timeout: 268 seconds).
01:41:01 -!- imode has joined.
01:41:25 <oerjan> `addquote <kspalaiologos> I have made a chess engine in Malbolge <kspalaiologos> in theory it's decent <kspalaiologos> but it has two drawbacks <kspalaiologos> a) It requires 31 and a half gigabytes of memory <kspalaiologos> b) it's quicker to count atoms in universe than to run it
01:41:27 <HackEso> 1336) <kspalaiologos> I have made a chess engine in Malbolge <kspalaiologos> in theory it's decent <kspalaiologos> but it has two drawbacks <kspalaiologos> a) It requires 31 and a half gigabytes of memory <kspalaiologos> b) it's quicker to count atoms in universe than to run it
02:00:41 <imode> @message kspalaiologos care to share this mythical chess engine?
02:00:41 <lambdabot> Maybe you meant: messages messages-loud messages?
02:00:51 <imode> @tell kspalaiologos care to share this mythical chess engine?
02:00:51 <lambdabot> Consider it noted.
02:10:59 <oerjan> imode: it was linked in the logs
02:11:32 <zzo38> I read on Wikipedia about digital television captions, and they mention many things I have not seen in other TV sets
02:11:43 <oerjan> <kspalaiologos> https://github.com/KrzysztofSzewczyk/malbolge-chess
02:53:10 <esowiki> [[Cupid]] M https://esolangs.org/w/index.php?diff=66644&oldid=58294 * IFcoltransG * (+29) Added Turing Complete tag
02:53:49 <esowiki> [[Cupid]] M https://esolangs.org/w/index.php?diff=66645&oldid=66644 * IFcoltransG * (+0) Fixed capitalisation on Turing complete category
03:44:48 -!- Lord_of_Life_ has joined.
03:45:40 -!- Lord_of_Life has quit (Ping timeout: 264 seconds).
03:45:43 -!- atslash has quit (Ping timeout: 250 seconds).
03:46:13 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
03:47:04 -!- atslash has joined.
04:00:01 -!- Lord_of_Life has quit (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine).
04:02:34 -!- Lord_of_Life has joined.
04:26:00 -!- imode has quit (Ping timeout: 268 seconds).
05:09:42 <zzo38> 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.
05:12:33 <zzo38> 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).
05:16:08 <zzo38> 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?
07:26:52 -!- imode has joined.
07:46:39 -!- anima has joined.
07:51:58 -!- LKoen has joined.
08:25:48 -!- LKoen has quit (Remote host closed the connection).
08:28:16 -!- LKoen has joined.
08:33:02 -!- imode has quit (Quit: WeeChat 2.6).
08:33:07 <b_jonas> oh nice. Zach from SMBC advertises his book on http://phdcomics.com/comics/archive.php?comicid=2033
08:34:10 -!- Ancyleus has joined.
08:36:01 <esowiki> [[Special:Log/newusers]] create * YouTuringCompleteMe * New user account
08:43:27 -!- LKoen has quit (Remote host closed the connection).
08:44:37 -!- LKoen has joined.
08:47:22 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=66646&oldid=66607 * YouTuringCompleteMe * (+275) /* Introductions */
09:04:47 -!- oerjan has quit (Quit: Nite).
09:11:01 -!- arseniiv has joined.
09:31:46 -!- LKoen has quit (Remote host closed the connection).
09:37:29 -!- LKoen has joined.
09:41:22 <esowiki> [[Deadfish~]] M https://esolangs.org/w/index.php?diff=66647&oldid=38929 * A * (+124) /* Sample Program */
09:42:04 -!- LKoen has quit (Remote host closed the connection).
09:43:11 -!- LKoen has joined.
09:55:12 -!- LKoen has quit (Remote host closed the connection).
09:58:23 -!- arseniiv has quit (Ping timeout: 250 seconds).
10:12:52 <int-e> Hmm, somehow the styles of http://www.yihcomic.com/ and http://sssscomic.com/ are quite similar.
10:16:57 <shachaf> Today I tried to actually figure out the details of CDCL and other tricks a bit more.
10:18:31 <shachaf> 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.
10:19:10 <shachaf> Here's one thing that's not even related to CDCL:
10:20:00 <shachaf> When you need to decide on a variable and you add a literal p to your assumptions, what do you do?
10:20:43 <shachaf> In theory you want to "delete" every clause that contains p and every literal ¬p from all the other clauses.
10:21:00 <int-e> well you don't
10:21:10 <shachaf> The two-watched-literal trick lets you only worry about some clauses that contain ¬p, hopefully a small subset.
10:21:26 <shachaf> Do you need to worry about clauses that contain p at all or do you just ignore them?
10:21:37 -!- arseniiv has joined.
10:22:58 <int-e> 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.
10:23:59 <shachaf> But then when you backtrack you might add it to a watched literal list?
10:24:29 <int-e> but you don't touch the watched literal lists when you backtrack?
10:24:33 <int-e> or backjump
10:25:15 <shachaf> Right, that's what I thought. But then I don't understand your previous sentence.
10:25:36 <int-e> I believe you can just keep the clause on the list that you're processing
10:26:12 <int-e> uhm actually
10:26:18 <shachaf> So a large number of clauses is just irrelevant for you because you only ever find clauses through watch lists.
10:26:20 <int-e> sorry, I'm confused
10:29:06 <int-e> 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.
10:29:22 <int-e> (well, the trail has a negated l)
10:29:27 -!- LKoen has joined.
10:30:29 <int-e> 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)
10:31:05 <shachaf> 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?
10:31:16 <int-e> yes
10:31:42 <shachaf> 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.
10:31:46 <int-e> this is a kind of laziness
10:31:49 <shachaf> Though I'm not sure a thing like that would actually work.
10:32:07 <int-e> (but a good kind because many clauses that become true will never be touched at all)
10:32:47 <shachaf> 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?
10:33:37 <int-e> Hmm, maybe it's clever to move them to the literal that is true instead.
10:33:52 <shachaf> Oh, that makes sense.
10:34:07 <int-e> (provided the clause is not on that watch list already)
10:34:17 <shachaf> 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.
10:34:34 <b_jonas> what... are you writing SAT solvers?
10:34:42 <shachaf> Er, the last thing I said doesn't make sense.
10:35:17 <int-e> b_jonas: I've been resisting the temptation for a long time. I think I can maintain this state :) Not sure about shachaf.
10:36:20 <shachaf> Some of my questions are about the actual typical operations/memory layout/etc. used by reasonable SAT solvers.
10:36:45 -!- arseniiv_ has joined.
10:37:04 <shachaf> Others are about clause learning, which seems like one of the most complicated parts of many modern solvers.
10:37:04 <int-e> b_jonas: But I know enough about the basics (DPLL, CDCL, a bit about heuristics) to be harmful.
10:37:58 <int-e> I know a bit more about the verification side. (RUP, DRUP, RAT, DRAT)
10:38:02 -!- arseniiv has quit (Ping timeout: 240 seconds).
10:39:30 <shachaf> Oh, UNSAT verification?
10:39:41 <shachaf> I'd like to know about how that works.
10:41:30 <shachaf> I suspect understanding UNSAT certificates and understanding CDCL are pretty related?
10:41:48 <int-e> Actually, no.
10:42:00 -!- LKoen has quit (Remote host closed the connection).
10:42:09 -!- arseniiv_ has quit (Ping timeout: 250 seconds).
10:42:21 <shachaf> Oh, that's interesting.
10:43:21 <int-e> 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.
10:44:56 <int-e> The inference relies heavily on unit propagation though, so for efficiency, you end up with watched literals again.
10:46:39 <shachaf> Sure, atched literals is a great trick.
10:46:57 <shachaf> I should understand regular SAT solving first.
10:48:04 <int-e> https://www.researchgate.net/publication/333612067_Efficient_Verified_UNSAT_Certificate_Checking should be a good starting point (including references for DRAT and DRUP).
10:49:23 <b_jonas> shachaf: you should just wait for Knuth to write that part of volume 4.
10:49:40 <int-e> 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.
10:49:48 <int-e> (and potentially learning)
10:50:21 -!- LKoen has joined.
10:50:38 <int-e> DRUP adds deletion of clauses (for efficiency). RAT is a bit more complicated and motivated by simplification of clause sets rather than DPLL itself.
10:53:04 <shachaf> b_jonas: Fascicle 6? I have a copy right here.
10:53:34 <b_jonas> I have technically written a SAT solver once, but it's a rather trivially stupid one, it only works on very simple expressions
10:53:48 <shachaf> It doesn't talk about many of the things I want, though, I think.
10:53:53 <shachaf> I've only read part of it so far.
10:54:02 <b_jonas> shachaf: so does it not help about "typical operations/memory layout/etc."? I'd expect Knuth to talk about those
10:54:30 <shachaf> It certainly talks about those, for the algorithms it describes.
10:56:37 <b_jonas> hmm, https://www-cs-faculty.stanford.edu/~knuth/news.html has multiple news that I haven't seen
10:57:41 <shachaf> I'll look at it some more after these papers.
10:58:46 <b_jonas> pity one of the links is already broken
11:02:51 <shachaf> 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.
11:02:56 <shachaf> I guess I'll take a closer look.
11:05:47 <int-e> I see he gets up to RUP.
11:06:15 -!- anima has quit (Remote host closed the connection).
11:16:39 -!- anima has joined.
11:16:39 * int-e wonders how close the September 2015 pre-fascicle is to the printed fascicle...
11:23:53 -!- atslash has quit (Read error: Connection reset by peer).
11:24:56 -!- atslash has joined.
11:30:15 <jix> 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 :)
11:30:41 -!- Ancyleus has quit (Ping timeout: 250 seconds).
11:30:57 <b_jonas> idling... does that mean we should `welcome you?
11:31:17 <b_jonas> also, nice
11:31:31 <jix> that just means I was quite active here... I don't know 10, 15 years ago or so and never parted :)
11:31:57 <b_jonas> yeah, this channel has a long history.
11:32:22 <b_jonas> ``` q jix # the quote file doesn't know that you were active... not under this name at least
11:32:23 <HackEso> No output.
11:32:33 <jix> https://esolangs.org/wiki/Jannis_Harder << that's me
11:33:18 <int-e> 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.
11:33:38 <jix> int-e: yeah I skip the DRAT => GRAT part which is as expensive as solving in the first place
11:33:58 <int-e> (This is Lammich's pipeline... Heule et al. have a slightly different intermediate format ... I forgot the name.)
11:33:58 <jix> what I do is solving -> custom format -> LRAT (which is inspired by GRAT)
11:34:43 <jix> 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
11:35:04 <int-e> 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.)
11:35:43 <jix> I experimented with emitting LRAT directly, but the code to keep track of clause ids became very complicated and introduced memory overhead
11:36:12 <jix> so my next attempt just hashes clauses and resolves hash conflicts during conversion
11:37:12 <jix> int-e: ah maybe it was inspired by a predecessor of GRAT?
11:37:36 <int-e> Hrm, let me check.
11:39:34 <jix> 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
11:40:02 <int-e> 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.
11:40:35 <jix> ah, yeah, so I was thinking of GRIT when I read GRAT
11:41:41 <int-e> (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)
11:44:02 <int-e> "amost as fast as gratgen" - yeah I thought that gratgen looked very good, performance wise.
11:47:55 <jix> 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
11:49:56 <jix> I might need to implement that for a competitive solver, though, if I want to convince people of that
11:52:06 <int-e> jix: Hmm, how well does the unsatisfiable core computation work though?
11:52:52 <jix> 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
11:53:35 <jix> 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
11:54:23 <int-e> 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.
12:13:17 -!- atslash has quit (Ping timeout: 240 seconds).
12:13:38 -!- atslash has joined.
12:21:00 -!- Amiona has joined.
12:25:58 <Amiona> Chat 40+ -> https://soo.gd/room40plus
12:52:25 -!- Amiona has quit (Remote host closed the connection).
13:15:21 -!- Sigyn has quit (*.net *.split).
13:52:21 -!- Sigyn has joined.
13:52:21 -!- Sigyn has quit (Excess Flood).
13:56:37 -!- Sigyn has joined.
13:56:37 -!- Sigyn has quit (Excess Flood).
13:56:59 -!- Sigyn has joined.
13:56:59 -!- Sigyn has quit (Excess Flood).
14:01:48 -!- Sigyn has joined.
14:01:48 -!- Sigyn has quit (Excess Flood).
14:02:10 -!- Sigyn has joined.
14:02:12 -!- Sigyn has quit (Read error: Connection reset by peer).
14:04:25 -!- Sigyn has joined.
14:20:41 <esowiki> [[Deadfish~]] M https://esolangs.org/w/index.php?diff=66648&oldid=66647 * A * (+106) /* Implementation */
14:23:03 -!- arseniiv has joined.
14:29:22 <tswett[m]> When was the first emoji used in #esoteric? 🤔
14:31:51 <b_jonas> tswett[m]: probably before 2003
14:35:52 <tswett[m]> 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.
14:36:05 <tswett[m]> "Relatively recently" as in within the past 5 years.
14:43:12 <int-e> 'Originating on Japanese mobile phones in 1997, emoji became increasingly popular worldwide in the 2010s after being added to several mobile operating systems.'
14:43:19 <int-e> <3 wikipedia.
14:44:05 <int-e> '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)
14:45:31 <tswett[m]> Nyope. Looks like iOS got support for emoji in 2011, much longer ago than I thought.
14:48:00 <int-e> Unicode version 6.0, 2010, added those to Unicode.
14:48:02 <b_jonas> tswett[m]: when did it get support for animated emoji?
14:52:08 <b_jonas> soon we'll have animated emoji with sound and smell
14:52:43 <b_jonas> 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
14:53:32 <b_jonas> and a singing voice modifier that changes the default tenor voice to a bass
15:02:15 <pikhq> Pretty sure those, well, aren't really emoji.
15:02:29 <b_jonas> not yet
15:02:31 <pikhq> They're pictures being sent, not Unicode strings
15:02:45 <pikhq> (animoted emoji, I mean)
15:05:39 <int-e> I remember animated fonts on VGA...
15:11:00 <esowiki> [[User talk:Palaiologos]] N https://esolangs.org/w/index.php?oldid=66649 * Palaiologos * (+0) Created blank page
15:37:47 <tswett[m]> int-e: EGA was the first to support those, wasn't it?
15:38:33 <int-e> tswett[m]: I'd have to check. I've never had an EGA myself.
15:41:17 -!- clog has quit (Ping timeout: 240 seconds).
15:43:35 <int-e> tswett[m]: I still don't know, but at least it's very plausible that EGA supported this trick :)
15:45:11 <b_jonas> 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
15:46:51 -!- Lord_of_Life_ has joined.
15:47:17 -!- Lord_of_Life has quit (Ping timeout: 240 seconds).
15:49:43 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
15:53:55 -!- kspalaiologos has joined.
15:55:28 <int-e> . o O ( who doesn't like charred pizza )
15:58:20 <kspalaiologos> charred pizza is profanation of pizza
15:58:38 <kspalaiologos> once in my life I've been to Venice, there was a guy selling pizza slices
15:58:41 <kspalaiologos> one slice was arm-length
15:59:06 <kspalaiologos> the slice overall was very moist with a lot of olive oil
16:00:05 <b_jonas> luckily it's not pizza
16:00:14 <b_jonas> and not charred
16:01:32 <b_jonas> [ 16*12*0.0254
16:01:33 <j-bot> b_jonas: 4.8768
16:02:58 -!- imode has joined.
16:12:59 <tswett[m]> int-e: Well, EGA definitely supported (the appearance of) animated fonts.
16:13:07 <tswett[m]> Hecc, I should get an EGA.
16:13:40 <tswett[m]> Hook it up to my IBM PC.
16:13:45 <tswett[m]> But first I'll have to get an IBM PC.
16:14:03 <tswett[m]> One with an 8080 processor, I don't want none of this protected mode nonsense.
16:23:07 <imode> 8080's are pretty cheap, you could just build one.
16:25:01 <int-e> tswett[m]: don't you at least want a proper 16 bit data bus though?
16:25:37 -!- clog has joined.
16:25:39 <int-e> I mean, you already have 16 bit registers.
16:25:55 <tswett[m]> Hmmmm, perhaps.
16:39:29 <pikhq> tswett[m]: https://monotech.fwscart.com/NuXT_MicroATX_Turbo_XT_955MHz_832K_RAM_XTCF_SVGA_Floppy_Serial/p6083514_19777986.aspx ?
16:39:53 <pikhq> (not the literally ideal solution for all use cases of this sort of thing mind, but it is a very pleasant product)
16:40:50 <tswett[m]> pikhq: Ooh, sweet!
16:41:29 <pikhq> Right?
16:41:59 <pikhq> 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
16:46:32 <pikhq> On the other hand, while trickier to get _most_ of what makes that nice can be cobbled together with other off-the-shelf things.
16:47:19 <pikhq> (just less all-in-one)
17:01:59 <b_jonas> oh I see. the "955MHz" in the url was confusing. it's "9.55 MHz" rather than "955 MHz".
17:12:53 <tswett[m]> That's fast enough to run a stock exchange. :D
17:17:54 <tswett[m]> Damn it, now I'm all thinking about writing stock exchange software for an online game.
17:18:13 <tswett[m]> Psst, I'm writing an online game. Currently, you can log into the game, and see how much of various commodities everyone has.
17:18:42 <tswett[m]> Currently it is not possible to gain more commodities, or to do anything with the commodities you've got.
17:19:24 <b_jonas> 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.
17:19:36 <b_jonas> it's ridiculous
17:21:34 <tswett[m]> Yeah, high-frequency trading is a weird thing.
17:21:59 <b_jonas> I mean, I don't work in financial areas, and admittedly the areas where I work are crazy in other ways,
17:25:02 <tswett[m]> Theoretically, traders provide a valuable service.
17:25:37 <tswett[m]> I want to be able to buy and sell goods, services and capital at prices that reflect their fair market value.
17:26:14 <b_jonas> right, they provide the grease that reduces the friction of the market
17:26:25 <tswett[m]> So if someone puts effort into providing that for me, they deserve a bit of return for their effort.
17:26:42 <b_jonas> they do get their return in the form of money
17:27:01 <tswett[m]> Right
17:27:11 <b_jonas> `? tinfoil hat
17:27:12 <HackEso> tinfoil hat? ¯\(°​_o)/¯
17:27:47 <tswett[m]> 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."
17:29:04 <b_jonas> I'm not sure that's separable. they provide the valuable service by being good at poker.
17:30:28 <tswett[m]> Well, in actual poker, the good poker players aren't really providing a valuable service to the bad poker players.
17:31:01 <tswett[m]> 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.
17:31:40 <shachaf> Golly. Instead of pointless gambling, people should be able to bet on real things, and thus provide a valuable service to the world.
17:32:31 <b_jonas> as in on the stock market?
17:33:16 <shachaf> Well, stock betting is already mostly legal, and it's useful but it's not the only useful market.
17:33:50 <shachaf> I think mostly arbitrary prediction markets should be generally legal in the US, except one special one.
17:34:05 <b_jonas> or they pretend it's mostly legal, because if we could find out what specific illegal thing they do, the authorities would punish them
17:34:23 <shachaf> What do you mean?
17:34:50 <b_jonas> how about the intermediate stuff, betting on sports?
17:35:08 <shachaf> Sports betting seems pretty useless to me, but probably a bit better than casinos.
17:36:16 <b_jonas> 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
17:36:24 <b_jonas> I don't understand how it's so popular
17:36:44 <shachaf> It's kind of odd which things are legal to bet on in the US.
17:37:09 <shachaf> For example you can bet on the weather.
17:37:47 <FaeFly> what things aren't legal to bet on?
17:39:15 <shachaf> Arbitrary events.
17:39:26 <b_jonas> 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.
17:40:21 <b_jonas> 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?
17:40:25 <shachaf> Except for predictit.org and apparently something in Iowa, which are still not legal but allowed to run anyway?
17:40:45 <b_jonas> 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
17:40:48 <FaeFly> I guess the UK is more permitting than the US wrt betting on arbitrary events, then
17:40:53 <b_jonas> and it's even harder to enforce it
17:40:59 <shachaf> b_jonas: The answers to these questions are well-established for other trading, so it doesn't seem like a problem.
17:41:18 <shachaf> I mean, if you're betting secret and illegally it's hard to enforce, but the law is reasonably clear.
17:41:36 <shachaf> Yes, the UK is more permitting.
17:41:47 <shachaf> Except in the UK you have to use inscrutable words like "back" and "lay".
17:41:57 <b_jonas> right. and since games of chance are so severely regulated here, almost everyone who earns a signifiacnt amount do it illegally
17:42:04 <shachaf> 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.
17:42:52 <b_jonas> ah, jargon
17:43:14 <FaeFly> Usually the UK brokers let you bet on whether you think arsons will torch the Gävle straw goat or not
17:43:23 <FaeFly> (speaking of being able to bet on arbitrary events)
17:44:15 <b_jonas> FaeFly: they always do, the bet is only about when
17:44:27 <FaeFly> hehe
17:44:42 <shachaf> Anyway my point is just that actual markets are useful for the world, whereas casinos are not.
17:44:52 <b_jonas> oh right, as for goats
17:44:54 <FaeFly> (nah, there's been years when it hasn't been, but the majority of the time it seems to be)
17:45:17 <shachaf> 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.
17:45:17 <int-e> shachaf: I thought running a casino is great for making money?
17:45:37 <shachaf> Yes, casinos are useful for the owners and not anyone else.
17:45:59 <shachaf> Markets are useful for everyone.
17:46:05 <int-e> hah
17:46:10 <b_jonas> 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_.
17:46:19 <FaeFly> :D
17:46:31 <int-e> shachaf: grocery markets, maybe
17:46:41 <shachaf> Grocery futures! Good idea.
17:47:01 <shachaf> Exotic grocery futures options derivatives.
17:47:06 <int-e> Been done for cocoa...
17:47:18 <shachaf> Oh, another thing that's illegal in the US is onions future.
17:47:32 <shachaf> But that's an explicit exception for onion, most kinds of futures are legal.
17:47:51 <shachaf> for onions
17:48:05 <int-e> Well you learned the right lesson from the Tulip crisis.
17:48:17 <int-e> (Those are a kind of onion, right?)
17:48:17 <b_jonas> 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
17:48:28 <b_jonas> you can't compete with that
17:48:32 <tswett[m]> Yeah, ban bulb speculation!
17:49:31 <shachaf> I'd like onion futures to be legal. Maybe I can write my congresshumans.
17:50:45 <b_jonas> 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?
17:51:10 <shachaf> It's this law: https://en.wikipedia.org/wiki/Onion_Futures_Act
17:52:17 <shachaf> It was later amended to ban box office receipts futures (bets on how much money a movie will make).
17:52:48 <shachaf> I think the law is just bad. As far as I know onion farmers agree nowadays.
17:53:44 <int-e> 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.
17:53:55 <int-e> A ticking time bomb.
17:54:04 <int-e> (No, I'm not a big believer in capitalism. Why do you ask?)
17:54:48 <shachaf> Yes, I know that. That's why I'm taking the contrarian view point, obviously.
17:54:49 <int-e> (More to the point I believe that free markets have optimize the wrong objective function.)
17:55:01 <int-e> s/have//
17:55:08 <shachaf> Sure, I agree on that.
17:55:22 <shachaf> Well, I don't know what right and wrong objective functions you have in mind.
17:55:38 <shachaf> But I also don't know what's better. It's easy to name shortcomings in markets.
17:56:01 <esowiki> [[Photon]] https://esolangs.org/w/index.php?diff=66650&oldid=63463 * Sugarfi * (+0)
17:59:05 <b_jonas> 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
17:59:46 <b_jonas> 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
17:59:54 <int-e> 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.)
17:59:56 <shachaf> I mean, they *were* unfairly exploited by futures traders.
18:01:01 <int-e> In practice, timely regulation is probably the best to hope for.
18:01:16 <tswett[m]> 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.
18:01:23 <shachaf> int-e: OK, sure, it sounds like we agree on that.
18:01:43 <shachaf> A big point of the whole market thing is that incentives line up well.
18:01:59 <int-e> Regulation is also the key to internalizing external costs, especially from the future.
18:02:02 <shachaf> And you certainly want regulation rather than "free markets" which can easily be pathological.
18:02:17 <shachaf> Right, and you want to internalize externalities.
18:02:50 <int-e> 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.
18:04:09 <int-e> Of course it's all embedded in a prisoner's dilemma between countries because for most things we have a global market.
18:06:03 <int-e> (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.)
18:07:16 <int-e> Cornering markets, as nasty as that is... seems minor in comparison.
18:08:28 <shachaf> Limiting climate change is good but a particular government can add regulation for externalities however market-oriented it is.
18:08:39 <shachaf> And the inter-government issues are no different.
18:14:35 <b_jonas> this channel is weird. SAT solvers in the morning, free market in the evening
18:15:26 <int-e> we've also seen ootsology, meditation, and actual spam
18:15:57 <shachaf> 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.
18:17:23 <b_jonas> `8-ball should futures be illegal?
18:17:24 <HackEso> Better not tell you now.
18:17:44 <b_jonas> fungot, what restrictions do you recommend to put on the free market?
18:17:44 <fungot> 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
18:17:54 <b_jonas> um
18:18:44 <int-e> 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...)
18:19:39 <shachaf> Hmm, I think futures are useful for reducing uncertainty and transferring risk from people who have it to people who want it.
18:20:15 <int-e> that's the trouble, isn't it
18:20:32 <int-e> hedging risks is great, speculation is bad, and there's no discernable differencw
18:20:35 <int-e> e
18:21:03 <shachaf> Why is speculation bad?
18:21:21 <shachaf> (Speculation can also be done without futures, of course.)
18:21:24 <int-e> it's bad when combined with bankruptcy
18:21:47 <int-e> Because then you're in an ugly external cost scenario.
18:22:07 * int-e shrugs.
18:22:31 <arseniiv> oh at first I thought about futures like promises
18:22:51 <int-e> Yes. I promise to buy ... shares at price ... in the future.
18:22:52 <int-e> :P
18:22:52 <shachaf> That's arguable, but often it's addressed anyway.
18:22:55 <arseniiv> now I see this is economical stuff I don’t know anything about
18:23:15 <shachaf> I think speculation clearly has a useful function too.
18:23:41 <b_jonas> and that's still greasing the market?
18:23:45 <arseniiv> though I don’t really distingwish promises and futures too, I hadn’t read anything comprehensive to date about them all
18:23:47 <shachaf> 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.
18:24:10 <b_jonas> right, greasing the market, even though wheat in particular isn't greasy
18:24:20 <shachaf> I get paid for it because the people who need it are willing to pay because it's so useful to them.
18:24:27 <shachaf> That seems cleary useful.
18:24:58 <int-e> shachaf: presumably you've also paid for storage. except... nowadays... that's not so clear at all
18:25:10 <arseniiv> . o O ( my market is all floury on the floor, who did it )
18:25:24 <shachaf> Nowadays you might've paid someone else for storage, sure.
18:26:31 <b_jonas> presumably if the grain travels time then someone payed for its storage somehow
18:26:39 <b_jonas> because no free launch
18:26:50 <shachaf> Right.
18:27:21 <int-e> or maybe there is no grain
18:28:18 <b_jonas> 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??
18:28:33 <int-e> it's futures -> short-selling -> cornering markets -> disaster. :P
18:29:18 <arseniiv> 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
18:29:44 <shachaf> 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.
18:30:08 <b_jonas> 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
18:30:21 <int-e> shachaf: because "everyone" is concentrated in the top 1%.
18:30:40 <shachaf> I don't think that's true.
18:31:08 <int-e> I think it's born out by the capital distribution and its changed distribution over time.
18:31:17 <shachaf> 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.
18:31:52 <arseniiv> (^cont.) (representing them the usual way gives something paranormal but why the reverse works is not automatically clear)
18:32:06 <int-e> but wouldn't they be better off if they had sufficient money floating to hedge those risks themselves...
18:32:09 <shachaf> 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.
18:32:16 <shachaf> Why?
18:32:34 <shachaf> I buy insurance rather than hedging tail risks myself.
18:33:13 <shachaf> I think in some cases insurance makes sense and in some cases it's ridiculous, but the concept surely makes sense.
18:33:39 <b_jonas> shachaf: right, that's more than half the point of insurance
18:33:52 <shachaf> (Ridiculous: US health insurance.)
18:33:54 <int-e> So you should cover normal fluctuations using your own capital and tail risks by a proper insurance?
18:34:11 <b_jonas> shachaf: oh yeah, that one is weird
18:34:13 <int-e> I don't see where you need futures in this picture.
18:34:42 <shachaf> You should be able to transfer whatever risks you want to people who want to buy them.
18:35:09 <b_jonas> or hmm
18:36:26 <shachaf> 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).
18:36:35 <b_jonas> 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
18:37:09 <b_jonas> `? trigak
18:37:10 <HackEso> trigak? ¯\(°​_o)/¯
18:37:54 <b_jonas> `? serini
18:37:56 <HackEso> serini? ¯\(°​_o)/¯
18:38:08 <b_jonas> what look, trigak and serini look just the same according to the wisdome
20:09:40 -!- kspalaiologos has quit (Quit: Leaving).
20:14:10 <shachaf> I often hear backjumping described as a big improvement, but is it actually that important?
20:14:43 <shachaf> 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.
20:40:30 <shachaf> b_jonas: https://twitter.com/ioccc/status/1183476350847336453
20:41:19 <b_jonas> ooh, this will be interesting
20:41:27 <b_jonas> shachaf: ioccc? let me see
20:42:02 <int-e> 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.
20:42:41 <int-e> shachaf: It's not an unconditional win, but heuristically you want to do as much unit propagation as possible before making a decision.
20:42:48 <shachaf> b_jonas: It's only a pre-update.
20:44:09 <int-e> shachaf: You can think of it as a partial restart, maybe?
20:44:25 <b_jonas> majority opposition win in Bp
20:45:13 <shachaf> 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?
20:45:14 -!- LKoen has quit (Read error: Connection reset by peer).
20:45:44 <int-e> shachaf: well, sooner or later...
20:46:17 <int-e> shachaf: actually, no, it's incomparable
20:46:35 <b_jonas> shachaf: I know it's not the final results yet, but it won't change significantly at this point
20:46:48 <int-e> 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.
20:47:41 <int-e> shachaf: I'm pretty sure this is one of those ideas that are completely unclear in theory but work out well in practice.
20:48:04 <int-e> Aka a heuristic ;)
20:49:23 <b_jonas> shachaf: yes, that's probably not worth an ioccclist trigger
20:49:26 <b_jonas> `? ioccclist
20:49:27 <HackEso> 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
20:49:39 <int-e> shachaf: oh what do you mean by "unwind"... only backtracking or backjumping really unwinds anything; everything else expands the trail.
20:49:40 <b_jonas> it doesn't even appear on the news page
20:52:01 <j4cbo> hey SDR nerds, can anyone identify this encoding scheme?
20:52:09 <j4cbo> https://usercontent.irccloud-cdn.com/file/o3noKYIX/Screenshot%202019-10-13%2014.51.44.png
20:52:13 <j4cbo> https://usercontent.irccloud-cdn.com/file/G4qGBD9F/Screenshot%202019-10-13%2014.50.47.png
20:52:53 <j4cbo> 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
20:53:36 <j4cbo> so a transmission is variable length depending on how many 0s or 1s there are?
20:54:00 <b_jonas> j4cbo: that could happen, there's at least one encoding scheme that is variable length like that
20:54:16 <b_jonas> of course there could be a layer over it that changes what comes out as zeroes and ones
20:54:24 <j4cbo> https://usercontent.irccloud-cdn.com/file/qoPjGUGh/Screenshot%202019-10-13%2014.53.51.png
20:54:39 <b_jonas> j4cbo: but isn't it also possible that you have too few samples and sometimes the high can be 2 long too?
20:54:59 <j4cbo> that is possible
20:55:18 <j4cbo> i'm trying to reverse-engineer my cheap-ass wirelessly controlled christmas lights
20:55:53 <j4cbo> 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
20:55:56 <b_jonas> see https://en.wikipedia.org/wiki/1-Wire which is variable length like that
20:56:05 <b_jonas> but with different timing
20:56:12 <j4cbo> then it's OOK over 433mhz
20:56:28 <j4cbo> i'm kind of hoping the receive device supports discrete on and off commands
20:56:30 <b_jonas> do you always get the same sample from the same button?
20:57:07 <j4cbo> yep
20:57:14 <b_jonas> well that's promising
20:57:23 <j4cbo> it just plays over and over again while the button is held down
20:57:45 <b_jonas> send it lots of random nonsense quickly and hope that does something?
20:58:01 <zzo38> Could you implement on/off by the power connection instead if needed?
20:58:43 <j4cbo> totally, but that requires extra hardware :P
20:58:55 <b_jonas> j4cbo: these only have, like, 17 bits of info at most, so try all 2**17 combinations
20:59:12 <b_jonas> some of them will probably be ignored
20:59:48 <j4cbo> yeah, i need to rig up some code to send those words out from my own hardware next
21:00:08 <b_jonas> are these sent by radio or by infrared?
21:00:18 <j4cbo> radio, 433mhz OOK
21:01:23 <b_jonas> hmm, that might be harder
21:02:13 <j4cbo> i have a spare rileylink
21:11:43 <shachaf> 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.
21:12:09 <shachaf> By unwinding I mean regular backtracking, i.e. only subtracting 1 from the level.
21:22:12 <int-e> shachaf: Right. Then I think I've understood correctly... and perhaps answered your question as well.
21:30:40 <shachaf> int-e: Back at computer.
21:31:34 <b_jonas> strangely, the word "confusil" doesn't appear in quotes or wisdom ... yet
21:31:45 <shachaf> int-e: Whether you backtrack or backjump to a point earlier in the trail, you should have the same state, shouldn't you?
21:32:43 <int-e> shachaf: No, because the backtracking will leave an additional literal on the trail.
21:32:51 <shachaf> I mean the same trail state. Your learned clauses might be different.
21:33:01 <b_jonas> sorry I don't make more constructive conversation, but SAT solvers really isn't a topic I feel interested about
21:33:04 <int-e> shachaf: before unit propragation with the learned clause kicks in.
21:33:40 <shachaf> Wait, backtracking only deletes everything past some point in the trail, doesn't it?
21:34:16 <shachaf> So at the time you unwind to any past level k, you've deleted everything past k in the trail.
21:34:19 <int-e> shachaf: backtracking takes deletes the trail up to the last decision, and places the negated decision literal on the trail
21:34:48 <shachaf> When you say "that point" what do you mean?
21:35:11 <shachaf> I feel like I should just draw a diagram and the confusilation would be resolved in eight seconds.
21:35:30 <int-e> shachaf: "that point" meaning the position of the decision literal that backjumping would replace on the trail.
21:37:04 <shachaf> 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.
21:37:38 -!- arseniiv has quit (Ping timeout: 240 seconds).
21:37:39 <shachaf> You reach a contradiction and you add a clause, which would let you backjump to replace e. Right?
21:37:40 <int-e> 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.
21:37:47 <int-e> shachaf: ^d marks decisions.
21:38:12 <shachaf> Aha.
21:38:20 <shachaf> Now I see what you mean. Thanks.
21:40:48 <shachaf> So one of the important things about CDCL is that the only thing the learned clauses are any use for is unit propagation. Right?
21:41:09 <shachaf> 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.
21:41:18 <int-e> . o O ( just like any other clauses )
21:41:47 <shachaf> No, the original clauses are useful for specifying your problems.
21:41:58 <shachaf> The new clauses are redundant and only useful if they make unit propagation happen.
21:42:12 <shachaf> I'm just saying something very obvious here.
21:42:14 <int-e> Right.
21:42:26 <int-e> Actually there's a point here.
21:42:50 <int-e> SAT solvers also prune the clause database (they forget clauses), and that's only allowed for clauses that are redundant.
21:43:09 <int-e> Which means that in most cases, they will only forget learned clauses.
21:43:12 <shachaf> Do they even forget original problem clauses?
21:43:49 <int-e> There are simplification procedures (I know nothing about them really except that they exist) which can also identify redundant clauses.
21:43:56 <shachaf> I thought the main reason to forget clauses was to save memory, and otherwise having a bunch of clauses doesn't hurt.
21:44:00 <shachaf> But, sure, simplification makes sense.
21:44:11 <int-e> Or potentially rewrite clauses (add some clauses that make other clauses redundant while maintaining satisfiability)
21:45:23 <shachaf> 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?
21:46:06 <int-e> You mean wrt the current trail?
21:46:10 <shachaf> 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).
21:46:28 <shachaf> But your learned clauses have to be globally true so you can't really talk about subproblems like that.
21:46:52 <int-e> If you ever want to go back on that assumption and keep the learned clauses valid... yeah you'll need full clauses.
21:47:01 <int-e> So in particular that's true for everything on the trail.
21:47:47 <shachaf> 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.
21:48:34 <shachaf> 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.
21:49:14 <int-e> Also learning is completely optional... a SAT solver can just refuse to learn clauses above a certain size.
21:49:36 <shachaf> Right. Without learning a CDCL solver is still correct, which is good.
21:50:12 <shachaf> Maybe you can just use big clauses for backjumping without learning them? Not sure how useful that would be.
21:50:21 <int-e> Actually it's kind of awful too... you have so many degrees of freedom for heuristics...
21:51:18 <int-e> Which literal to decide on, what to learn, what to forget, when to restart...
21:51:44 <shachaf> Restarting seems like a surprising strategy to me. Especially a solver (BerkMin) that restarts every 550 conflicts?!
21:52:00 <shachaf> Do restarting solvers have any guarantee of termination?
21:52:24 <int-e> They are supposed to do some sort of (exponential?) backoff...
21:53:00 <int-e> But this interacts in interesting ways with learning.
21:53:30 <int-e> If you learn all backjump clauses and never forget then even if you restart after every conflict you'll eventually solve the problem.
21:54:01 <shachaf> Oh, because everything slowly becomes forced by UP.
21:54:12 <int-e> (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)
21:59:38 <int-e> 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.
22:00:53 <int-e> I suppose this is especially important for satisfiable problems.
22:09:15 <shachaf> Why is unit propagation the only thing used for assigning values to variables, other than decisions?
22:13:53 <int-e> because it's fast?
22:14:57 <int-e> And I guess the attitude is that all other inferences can be learned as clauses.
22:19:39 <int-e> 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.
22:21:51 <int-e> If you're facing a decision like... "would you rather do X or 1k unit propagations"
22:22:23 <int-e> it's easy to imagine that X probably won't pay off :)
22:49:11 <j4cbo> boo, i need an SDR
23:03:15 -!- xkapastel has joined.
23:41:35 -!- Hooloovo0 has quit (Ping timeout: 265 seconds).
←2019-10-12 2019-10-13 2019-10-14→ ↑2019 ↑all