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…
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…
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 functions succinctly yet in a way that…
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…
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…
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…
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…
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…
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 combining…
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.org/wiki/Toda%27s_theorem
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…
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…
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…
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…
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…
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…
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 functions succinctly yet in a way that…
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…
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…
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…
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…
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…
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 combining…
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.org/wiki/Toda%27s_theorem
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…
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…
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…
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…