fcholf

5 ms·

1.
by fcholf 1mo ago
Late answer but I need to be pointlessly pedantic again, because it is apparently what it is called to correct something that does not make sense. That said, I agree with your way of reformulating your point. To first address the pedanticne
2.
by fcholf 1mo ago
I agree with 1 but: > 2. When there's some large set of instances of some NP-hard problem that are tractably solvable in practice (like SAT), the importance of that is that there's some non-NP-hard subset here. Indeed, SAT is F
3.
by fcholf 5mo ago
Well that is the norm if you use acronyms that are not well-known for the target audience. The paper you see is a submission to the SAT'26 conference, a conference dedicated to the problem SAT and related questions. For most people the
4.
by fcholf 5mo ago
I did not know about Ternary Decision Diagrams, sorry for the name clash. I had a look. You can always reencode Ternary Decision Diagrams into Binary ones by just encoding variable x with two bits x^1 and x^2, so Ordered Ternary Decision Di
5.
by fcholf 5mo ago
In my comment, it was for Sentential Decision Diagrams.
6.
by fcholf 5mo ago
We are still waiting for the reviews. The rebuttal phase should start soon, we'll see!
7.
by fcholf 5mo ago
Hey, author here, so clearly I'm biased. There is a branch of computer science (close to SAT/constraints solving communities) studying data structures allowing to represent Boolean functions succinctly yet in a way that allows you
8.
by fcholf 5mo ago
Hi, author here! Also positively surprised to see this on HN haha We (well mainly Guy, if he's around) are working on an implementation, which will be made open source at some point (still rounding the edges a bit). We have very encour
9.
by fcholf 8mo ago
I agree, though, you can still work toward understanding using an LLM (and take it from a skeptical) by, e.g., using them as challengers to your ideas. That said, I think it requires a lot of self discipline and should be complemented with
10.
by fcholf 11mo ago
To efficiently encode XOR-constraint you will necessarily need extra variables (as you proposed) because we know that no bounded depth and polynomial size Boolean circuit can encode parity ("parity is not in AC0"). The problem wit
11.
by fcholf 11mo ago
I would also add that #SAT solvers, aiming at counting the number of solutions, are often implicitly solving the ALL-SAT in a more efficient manner than what you would have with modified CDCL solvers because they use other caching and decom
12.
by fcholf 11mo ago
Hi Alixander Thanks for the good work! I am late to the party, but let me add my grain of salt. I think animations could be a killer feature when preparing for talks. This is something I already do with a modified version of graphviz (I exp
13.
by fcholf 4y ago
You may use xslt for this kind of operation ( https://en.wikipedia.org/wiki/XSLT ) but it is often overkilled. I would love a language that allows to easily write transductions of HTML documents but I think that combinin
14.
by fcholf 4y ago
Actually, this has been done: https://arxiv.org/abs/1903.11391
15.
by fcholf 4y ago
> #P complete is at least as difficult as NP complete. This is an euphemism :)! It is quite likely that #P is way harder than NP as witnessed by Toda's Theorem https://en.wikipedia.org/wiki/Toda%27s_theorem
16.
by fcholf 4y ago
I would be curious to know examples of SAT solvers you have in mind for approximate counting. The only tools I am aware of for approximate counting are dedicated to this task (and usually use SAT solvers as oracles under the hood).
17.
by fcholf 4y ago
Well this is true but CDCL SAT solvers do not materialize this BDD and they stop as soon as they find a satisfying assignment. If they do not find any satisfying assignment, they do not return the BDD as unsat proof but roughly the list of
18.
by fcholf 4y ago
This is not the same goal as SAT. SAT looks for one satisfying assignment while OBDD tries to represent the full set of satisfying assignment in a factorized way to be analyzed later. For example, trying to count the number of satisfying as
19.
by fcholf 4y ago
Interesting to see it posted on HN. My favourite book on the subject is Branching Programs and Binary Decision Diagrams by Ingo Wegener: https://doi.org/10.1137/1.9780898719789 . There have been recent exciting develo