undefined | Better HN

0 pointsjs82y ago0 comments

I haven't really studied it in detail, but my motivation is similar, I see SAT as a simplified version of the marginal problem, and I want to solve marginal problem (or at least approximate) because I am interested in representing knowledge intensionally.

I played with propagation a lot in the past, but I don't think local propagation (that resolves conditions of a bounded number of variables at a time, until everything stabilizes) can ever work, because it would contradict Razborov result on monotone circuits. I don't remember the exact argument, but I think it would imply a polynomial monotone circuit capable of resolving the instance. Also, XORSAT is not really amenable to this either, to solve arbitrary XORSAT instance you have to add together arbitrary number of linear equations, so the number of variables per equation can balloon up.

That's why more recently I focused on understanding what exactly is the role of XORSAT, and by serendipity, I stumbled upon the above-mentioned reduction (which I think is a really exciting result). XORSAT is great for testing different algorithms, because despite the fact we have a nice polynomial algorithm (Gaussian elimination), one can easily create arbitrary (and loopy) instances where propagation is difficult.

The way I see it, to avoid the problems with the bound, you need to preprocess the linear equations "inherent" in the instance by adding extra variables. The exact way to add variables depends on the instance, but it can be done by solving the linear equations. Propagation algorithms that go into the process blindly, without understanding the underlying linear structure, will mysteriously fail.

However, my current approach through logic, basically building up theorems about the instance, until it is decided, can be considered a generalization of the propagation approaches. The messages are true statements about variables, which are propagated by deduction rules of the logic. But this is done only after we have discerned the linear structure in the problem, which is addressed globally, as described above.

0 comments

theGnuMe2y ago

That jives with my intuition. I had forgotten about the connection between Gaussian elimination and xor sat. That does sound like a good direction to reason from.

How do you prevent an exponential increase in linear terms though?

Good luck!

js8OP2y ago

I am still not sure about the exact role of Gaussian elimination. I thought that it will be somehow necessary, but it seems that if you only break linear equations to 3 variables per equation (by adding extra variables), you can get away without it. Although it certainly doesn't hurt to do it, I think for efficient algorithms, it will be required (and so the whole endeavor will be at least O(n^3)).

To prevent exponential increase in linear terms, I work within a sort of limited logic that only allows formulas that are ORs of (implications between) two linear equations of up to 2 variables. This logic accommodates both 2-SAT clauses and linear clauses of 3 variables, and seems to be able to emulate Gaussian elimination to some extent, but I am not yet completely sure how. Last week, I think I was able to generalize Krom's proof of refutable-completeness for 2-SAT logic (that has linear equations on 1 variable) to this logic, but I am in the process of double checking my result for gotchas like this.

There are other ideas how to control the linear terms, once you have the linear equations solved, it's easy to verify whether some variables are linearly dependent, because you have the basis, and modify the ordinary 2-SAT algorithm accordingly (2-SAT works by propagation via transitive dependency of literals, but if the 3 variables involved are linearly dependent, then you can derive lot more). These are mainly ideas how to make the polynomial algorithm even more efficient.

And thanks for encouragement!

j / k navigate · click thread line to collapse