Viewing profile — fcholf

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…

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…

In my comment, it was for Sentential Decision Diagrams.

We are still waiting for the reviews. The rebuttal phase should start soon, we'll see!

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…

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 poin…

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 requir…

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 encod…

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 mo…

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 somet…

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 …

Actually, this has been done: https://arxiv.org/abs/1903.11391

> #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…

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 …

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 d…

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 lat…

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 . T…