i understand that you don’t distribute kernel images signed by microsoft for your own distro (https://www.tuxedocomputers.com/en/TUXEDO-OS_1.tuxedo – “Secure Boot must be disabled in your computer’s UEFI firmware”), but i’m planning to sign my own kernel images anyway and get rid of the microsoft PK/KEK entirely
this works nicely on my ibp 14 v4 (apparently it doesn’t have anything onboard that needs a microsoft KEK to initialize properly with uefi), but that’s a clevo motherboard, not a uniwill one. does the ibp 14 gen8 firmware has anything signed with microsoft’s keys that would break if i removed the keys?
@juliank the tricky thing is what would happen if you backtrack and the clauses that were in conflict get removed (if you remove versions of packages you decide not necessarily to install on backtracking).
in this case the conflict cause would become useful once you decide to install the same package at some other branch of the search when the variables and clauses get added back again. until then, some variables would be “dangling” (appear in the lemma, but not in the problem proper)
but i guess this is not actually a problem if variables can be uniquely identified (so it is apparent when they are re-added to the problem) and you never branch on “dangling” variables
SAT solvers are weird, man
@juliank ah, materializing further clauses sound reasonable, especially if solutions have a fairly regular structure. i guess your alternative would be to pull in clauses for all transitive dependencies, which sounds a lot more painful
a tricky thing is how to represent useful lemmas (CDCL-style) when some variables from the learned clause might not even be in the original problem (pulled in by a transitive dependency in your case).
the very least, i’m having a lot of trouble with that on the first-order model generator that we’re working on (i can’t even pull in all clauses eagerly in the beginning, because i don’t know the model size in advance and a FOL quantifier could match any model element)
2**32 levels of backtracking.
holy (super) cow! is that a state space of
A->B|...|Z looks suspiciously like a dual-Horn clause
!A | B | ... | Z (although I don’t know what to make of
A->!B, other than just
!A | !B). but it’s defnitely no accident that your algorithm is pretty much DPLL, given that your input is already basically in CNF
maybe this is a good time for CDCL?
btw (commenting here because i’m not logging into my reddit account any time soon after the API debacle), it seems like the issue you linked in https://old.reddit.com/r/tuxedocomputers/comments/14noz4v/infinity_book_pro_14_gen8_cannot_find_disable/jqqd2nv/ is not publicly accessible. i assume this should land in the next firmware update anyways?
Happy Enshittification Day! 💥
July 1, 2023: Reddit cuts off API access, Twitter requires login, Youtube may ban ad-blockers, Meta & Google block news in Canada...
A half-year since Cory Doctorow's seminal thesis on #enshittification, how corporate platforms die (https://pluralistic.net/2023/01/21/potemkin-ai/#hey-guys), and every corporate site seems hell bend on its own destruction.
Celebrate #EnshittificationDay by going to [instance address]/about, find the donations link, and make your contribution to open social media!
this doesn’t support adding V0 streams for songs i bought, but i don’t really need that. all songs i bought are downloaded in flac anyways. however, listening to 128k previews before i buy stuff bandcamp friday come is comfy
second student so far in the exam i’m correcting who claims that graph isomorphism is NP-complete
either they know something i don’t or they prepared for the exam… poorly
@Techmeme company named after fruit allegedly more strongly represented by a depiction of fruit than the actual fruit – truly a hyperreal nightmare
bandcamp won their union! bandcamp won their union!!
i'm so fucking happy for them, and also for the possible knock-on effects of some of epic game's holdings unionizing
once more for the backrow hecklers
nvidia _choose_ to not support the wayland stack. or well more generally, the new linux kms+egl gpu stack, since there's a lot other cool things you can built on top of it that aren't wayland
nvidia _choose_ to implement crypto locked down fw in a way that blocks open drivers (even apple got this right!). and no one else can fix it, because it's actual real crypto
nvidia _choose_ to not fix any of this
don't buy nvidia if you don't like this
realizing I need Emacs for playing around with Agda, I spent a good chunk of today declaring Emacs bankruptcy and setting up a new
I have a much more lightweight but functional Emacs config now
I still don’t know Agda