00:04:36 -!- Soni has quit (Ping timeout: 264 seconds).
00:12:36 <int-e> ... savannah.gnu.org just went down?
00:13:52 <shachaf> b_jonas: I bought some fascicles.
00:15:08 <int-e> I read some of the pre-fascicles. Not sure yet about buying the book... if anything it'll be a christmas thing I guess.
00:15:34 <int-e> I'm definitely not in a hurry
00:16:01 <int-e> hmm... apart from kissat, what other sat solver should I throw at this
00:17:18 <int-e> I wish http://satcompetition.org/ would list winners for 2019-2021 as well.
00:17:49 <int-e> At... I guess something that qualifies as a "hard combinatorial problem" (cf. https://research.ibm.com/haifa/ponderthis/challenges/October2022.html )
00:19:58 <shachaf> From what I remember of the SAT solver competition results, vbs was a very good solver.
00:20:31 <shachaf> (Sorry, I don't know which solvers are state-of-the-art these days.)
00:21:00 <int-e> (Or the individual competition pages. Sure, the information is there somewhere... result CSVs for the tracks, huge submissions tarballs, proceedings... but they're not accessible)
00:22:01 <int-e> Hmm. This maybe? https://github.com/simewu/top-SAT-solvers-2021
00:25:31 <int-e> (not the github link; the reference to VBS)
00:30:34 <int-e> TIL what vivification is in SAT solving
00:30:57 <int-e> shachaf: It's okay, I just took way longer to realize than I like.
00:31:36 <int-e> Nah you had reason to believe that I should know that acronym.
00:32:14 <int-e> And I have encountered it before.
00:32:35 <shachaf> Hmm, I don't know what vivification is.
00:33:55 <int-e> It's for removal of redundant literals from clauses... https://home.mis.u-picardie.fr/~cli/clauseVivificationPublishedVersion.pdf is what I looked at.
00:36:35 <int-e> The other thing I'm wondering is whether there's anything bad about using a sorting network for encoding a cardinality constraint "at least n out of 148".
00:38:36 <shachaf> When is a literal redundant?
00:39:13 <shachaf> I guess their answer is "when the clause without that literal is implied by the other clauses".
00:39:20 <int-e> shachaf: The criterion they use is that l is redundant in l v C if asserting ~C and unit propagation lead to a conflict.
00:39:45 <b_jonas> I think for just getting 108 on the ponder this you don't need a SAT solver
00:40:40 <shachaf> That seems kind of expensive to check!
00:40:41 <int-e> b_jonas: Yeah, and not for 110 either.
00:40:44 <shachaf> I guess that's the point of this paper.
00:43:45 <shachaf> The thing I said is too general, of course. For example the empty clause is implied by any UNSAT instance.
00:44:17 <shachaf> And also by "other clauses" I meant "all clauses".
00:44:19 <int-e> "Unfortunately, it is not easy to make clause vivification effective because of its high cost."
00:44:36 <shachaf> But if you restrict it to unit propagation -- which still seems hard? -- don't you lose a lot of the benefits?
00:45:41 <int-e> Well, as they also point out in that paper, identifying redundant literals is still NP-hard.
00:46:10 <shachaf> Right, for example for the reason I said, I imagine.
00:46:51 <int-e> While the approximation is polynomial (and mostly linear), and furthermore based on something SAT solvers already do very efficiently.
00:47:18 <int-e> Well, the DPLL/CDCL ones anyway.
00:48:12 <shachaf> Don't you still need to pick which literal to check? I guess that's bounded by your instance size.
00:48:15 <int-e> (Somehow the "DPLL" acronym has disappeared. Or maybe that's just an Armin Biere thing?)
00:48:39 <int-e> shachaf: It's also bounded by the clause size.
00:48:55 <shachaf> I mean, if you check all your clauses.
00:50:10 <shachaf> I can probably excuse people for it being ancient history when no one knew how to do algorithms yet, but it seems a little odd that DPLL is even a named algorithm.
00:50:38 <shachaf> I guess people also don't do pure literal elimination, so really no one does DPLL.
00:50:38 <int-e> And they actually restrict it further (relying on ordering the clause's literals) so that only one trail (alternating between asserting a negated literal and unit propagation) is created, rather than a (at least partially) new trail for each literal.
00:51:25 <shachaf> I should read this in more detail probably.
00:51:38 <shachaf> Also I should get back to SAT solvers! I had a great time working on my CDCL solver.
00:52:00 <shachaf> I still need to add a better variable ordering heuristic. I think that's the biggest impact thing I can do.
00:52:24 <shachaf> Some people do VSIDS but I hear rumors about move-to-front being good.
00:52:32 <shachaf> Or also more complicated things.
00:52:48 <int-e> Hmm. I don't know whether people do this as an in-processing technique, but one thing you can do to eliminate a variable is to resolve each pair (x v C, -x v D) in the clause set. The pure literal rule is a special case of that.
00:53:23 <shachaf> That's the original DP algorithm, right?
00:54:02 <shachaf> This thing: https://en.wikipedia.org/wiki/Davis%E2%80%93Putnam_algorithm
00:54:19 <shachaf> Hmm, I guess it has a bunch of other steps.
00:54:29 <shachaf> «Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm.»
00:55:50 <int-e> Yeah, it's the DP procedure there.
00:56:07 -!- Lord_of_Life has quit (Ping timeout: 246 seconds).
00:56:26 <shachaf> I falsely remembered it as the only thing that algorithm did.
00:56:32 <shachaf> Now it seems a lot more reasonable.
00:57:20 <shachaf> I didn't think of pure literal elimination as a special case of that, that's funny.
00:57:23 -!- Lord_of_Life has joined.
00:58:06 <int-e> Oh it's not quite correct.
00:58:47 <int-e> Nah, it's correct after all.
00:59:05 <int-e> I'm just confusing myself with second thoughts.
00:59:12 <shachaf> Right, you resolve and then remove all the clauses containing the original literal.
00:59:17 <shachaf> So if there are no negations you just remove all of them.
00:59:23 <shachaf> I also confused myself for a bit about it.
01:00:48 <shachaf> I have something like a topological sort of a partial order, but with the property that there are a bunch of extra constraints of the form "if a < b, then c < d, e < f, etc."
01:01:07 <shachaf> Is there a nice representation of this sort of thing? It seems like it'd get very busy visually, drawing all the hypothetical edges.
01:01:42 <int-e> so... putting b before a may be advantageous?
01:02:20 <shachaf> It's not really that I want to find an "optimal" order.
01:02:25 <shachaf> I just want to explore all the possible orders.
01:03:06 <shachaf> Specifically this is about CPU memory ordering. The nodes in this graph are things like "store x is visible at thread t".
01:03:25 <shachaf> A directed graph isn't flexible enough for the kinds of constraints you'd want to express.
01:03:48 <shachaf> I *think* maybe constraints of the form I gave might be enough.
01:04:26 <int-e> fancy. you have a digraph on the edges of a digraph
01:05:12 <int-e> (if you split "if a < b, then c < d, e < f, etc." into "if a < b, then c < d", "if a < b, then e < f", etc.
01:05:43 <shachaf> I see, where the 2-cell structure here is "this edge exists implies that this edge exists".
01:06:55 <shachaf> That's an interesting way to look at it.
01:09:24 <int-e> b_jonas: anyway, regarding needing a SAT solver... I got 120 edges basically on pen&paper.
01:09:41 <int-e> b_jonas: but I'm trying to narrow the gap between the lower and upper bounds that I have.
01:10:30 <int-e> b_jonas: partly because the problem *originally* asked for an optimal solution.
01:10:45 <zzo38> I do not have any of the TAOCP although I have borrowed the first few temporarily from the inter library loan. I think I might be interested to read, though.
01:11:23 <shachaf> It's kind of weird to think of it the way you said because the 1-cell edges might not actually exist, right?
01:11:29 <shachaf> Or am I missing a nice way to make that work?
01:16:13 <int-e> I guess you kind of need two forms, T ==> a < b (or just a < b) for unconditional orderings, and then the interesting a < b ==> c < d.
01:17:00 <int-e> (you can play tricks like a < b ==> P and b < a ==> P exploiting that you're looking for total orders, but that doesn't seem helpful)
01:17:26 <int-e> I'm trying to convince myself that this is NP-hard.
01:23:01 <int-e> Ah. Yes, it is. You can use a < b for a literal (and b < a for its negation), and then, to encode A | B | C, pick fresh auxiliary variables u,v,w, and encode !A => u < v, !B => v < w, !C => w < u, thereby reducing from 3-SAT.
01:24:30 <int-e> (transitivity is a bunch of 3-clauses)
01:26:21 <int-e> b_jonas: Oh well I submitted https://savannah.gnu.org/support/index.php?110743
01:29:29 <shachaf> What's the thing that's NP-hard? Finding out whether a topological order exists at all?
01:30:06 <shachaf> Hmm, I guess my statement is too general, because they certainly always exist in my case.
01:34:18 <int-e> It probably doesn't matter for enumeration (unless the set of valid orderings gets very sparse relative to the n! possible ones)
01:37:08 <int-e> NP-hard: Enumeration is, since it has to solve the existence problem to produce the first candidate.
01:38:13 <shachaf> Certainly enumeration is NP-hard if existence is.
01:38:22 <int-e> shachaf: in your application, do you ever have both a < b and b < a?
01:39:23 <int-e> (from the description I'd rather suspect that all pairs a < b are picked from a preexisting partial order)
01:40:51 <int-e> (but I'm not sure)
01:41:21 <int-e> however... I'll try to catch some sleep
01:44:12 <shachaf> Very often the constraints are of the form: "if a_0 < b_0, then a_1 < b_1, a_2 < b_2" and "if b_0 < a_0, then b_1 < a_1, b_2 < a_2"
01:45:02 <shachaf> Actually the constraint here is that there's a global order on {a, b, c} such that each cluster {a_i, b_i, c_i} is in the same order.
01:45:09 <shachaf> (This isn't the only kind of constraint but it's an important one.)
01:46:36 <int-e> Though "if a < b then c < d" and "if d < c then b < a" are equivalent.
01:47:30 <shachaf> So one thing I was imagining was a GUI for exploring simple graphs, where you click on one node at a time to create a particular total order.
01:47:57 <shachaf> But something for enumerating all possible orders would also be useful.
02:12:18 <b_jonas> zzo38: you can buy them as e-books now
02:13:24 <b_jonas> int-e: a bug report for bash. I see.
02:16:55 -!- razetime has joined.
02:37:30 -!- earend1 has joined.
03:13:31 <zzo38> I would prefer a printed copy, though
03:36:12 -!- Soni has joined.
03:42:24 <b_jonas> zzo38: you can order those too
03:43:36 <b_jonas> they're somewhat more expensive though
03:47:42 <zzo38> How much expensive?
03:58:06 <b_jonas> zzo38: https://www.informit.com/promotions/art-of-computer-programming-books-and-ebooks-140521
03:59:11 <b_jonas> hard to tell because the shipping costs aren't obvious if you're outside the US
04:00:15 -!- razetime has quit (Ping timeout: 250 seconds).
04:35:41 -!- razetime has joined.
04:49:31 -!- sprock has quit (Remote host closed the connection).
04:54:50 -!- sprock has joined.
05:00:38 <zzo38> I am in Canada, which is near United States.
05:02:49 <zzo38> Scryfall bulk files has a Oracle bulk file, which seems good to me, but last time, I had problems with it. For example, I should not want any cards that do not have Oracle text (somehow, there are some, even though there should not be), and do not want anything about versions of cards but only the Oracle and legality, that is in common of all versions.
05:03:13 <zzo38> Now that there is lights too, I should think that the lights should be given as an array of array of numbers, but it does not do that.
05:06:17 <zzo38> Is there a better one available?
05:13:03 -!- earend1 has quit (*.net *.split).
05:13:04 -!- pikhq has quit (*.net *.split).
05:13:05 -!- imode has quit (*.net *.split).
05:13:05 -!- MizMahem has quit (*.net *.split).
05:13:05 -!- integral has quit (*.net *.split).
05:13:05 -!- Argorok has quit (*.net *.split).
05:13:18 -!- imode has joined.
05:13:28 -!- Argorok has joined.
05:13:52 -!- earend1 has joined.
05:14:14 -!- MizMahem has joined.
05:14:20 -!- earend1 has changed hostmask to uid568065@user/utoneq.
05:14:29 -!- integral has joined.
05:14:30 -!- pikhq has joined.
05:14:32 -!- MizMahem has changed hostmask to sid296354@user/mizmahem.
05:14:37 -!- integral has changed hostmask to sid296274@user/integral.
05:14:39 -!- pikhq has changed hostmask to sid394595@user/pikhq.
06:27:16 -!- Sgeo has quit (Read error: Connection reset by peer).
07:51:54 -!- tromp has joined.
08:01:36 -!- razetime has quit (Ping timeout: 264 seconds).
08:26:38 -!- razetime has joined.
09:05:19 -!- razetime has quit (Ping timeout: 250 seconds).
09:05:48 -!- razetime has joined.
09:14:22 -!- __monty__ has joined.
10:01:12 -!- laerling has changed hostmask to ~laerling@user/laerling.
10:05:54 -!- razetime has quit (Ping timeout: 248 seconds).
10:08:49 <esolangs> [[!lyriclydemoteestablishcommunism!]] https://esolangs.org/w/index.php?diff=103997&oldid=99916 * HungKhanh0106 * (+76) /* Implementation */
10:09:14 <esolangs> [[!lyriclydemoteestablishcommunism!]] https://esolangs.org/w/index.php?diff=103998&oldid=103997 * HungKhanh0106 * (+4) /* Implementation */
10:27:04 -!- razetime has joined.
11:22:39 -!- Noisytoot has quit (Quit: ZNC 1.8.2 - https://znc.in).
11:26:50 -!- Noisytoot has joined.
12:21:23 -!- Noisytoot has quit (Ping timeout: 248 seconds).
12:26:10 -!- Noisytoot has joined.
12:35:45 -!- Noisytoot has quit (Ping timeout: 268 seconds).
12:48:55 -!- Noisytoot has joined.
12:57:49 -!- Noisytoot has quit (Ping timeout: 246 seconds).
13:07:36 -!- Noisytoot has joined.
13:21:27 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
13:36:01 -!- tromp has joined.
13:40:29 -!- shikhin has changed nick to handy.
13:40:38 -!- Sgeo has joined.
13:40:52 -!- handy has changed nick to shikhin.
15:44:01 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
16:06:40 -!- tromp has joined.
16:23:36 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
16:33:58 -!- tromp has joined.
16:47:23 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
17:05:19 -!- Noisytoot has quit (Ping timeout: 252 seconds).
17:07:32 -!- Noisytoot has joined.
17:13:15 -!- FreeFull has joined.
17:13:23 -!- Noisytoot has quit (Remote host closed the connection).
17:16:39 -!- Noisytoot has joined.
18:14:07 -!- tromp has joined.
18:16:15 -!- razetime has quit (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.).
19:06:56 <zzo38> How does name stickers working in Magic: the Gathering if applied to an object that has no name or that has multiple names?
19:54:27 <esolangs> [[Tinytalk]] M https://esolangs.org/w/index.php?diff=103999&oldid=103996 * Rdococ * (+50) /* Sets */
21:02:51 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
21:04:47 <esolangs> [[Tinytalk]] M https://esolangs.org/w/index.php?diff=104000&oldid=103999 * Rdococ * (-25) /* Implementations */
22:19:14 -!- __monty__ has quit (Quit: leaving).
23:07:50 -!- fungot has quit (Ping timeout: 268 seconds).
23:38:53 <esolangs> [[Special:Log/newusers]] create * Lien889 * New user account
23:50:09 -!- FreeFull has quit.