A new SAT solving algorithm

 Hello,

I am interested in P vs NP and other complexity questions. For now, there is a new SAT solving algorithm that you can read about:

pldecomposition.pdf

 Update: The above paper has a slight bug in rare cases, although the safe choice conjecture might still hold. Consider it retracted. I will post an updated version.

Komentáře

Okomentovat

Populární příspěvky z tohoto blogu

My current strategy to prove P=NP

Since I have already opened up about my intent and strategy to prove P=NP in some HN comments ( https://news.ycombinator.com/item?id=36082578 and https://news.ycombinator.com/item?id=35729626 ), I decided I should explain it in a series of posts. After all, this was my original goal when I started the blog, to explain more the exciting possibility that P=NP (with a nice constructive algorithm), so that more people could get involved and contribute to that approach. As for my motivation, that's probably a topic for another blog post, let's just say I think it is an extremely important problem to work on. I have been working on understanding P vs NP question as a serious hobby for about 6 years now, however, it was a discovery I made about a year ago that made me really optimistic about P=NP, and that a proof can be close. (Up to that point, I was always trying to be agnostic about the question, although I do admit I don't really buy many arguments or intuitions for P!=NP, a...
Další informace

Will trilinear logic help with the completeness obstacle?

In the previous blogpost , we have seen that the poset-linear logic is not refutation complete for certain theories in it. This is a major obstacle in building a (possibly polynomial) algorithm that decides satisfiability problem by constructing the set of tautologies, as I explained there. Here I discuss my plan to fix this problem, which is to build a larger logic (I will call it trilinear), and try to show refutation completeness of all theories of poset-linear logic within trilinear logic. Despite trilinear logic being larger, it's only slightly so, and hopefully it will not present an obstacle for the step 3 of the grand strategy. Trilinear Logic So let's start with definition of the new trilinear deductive system $\mathcal{TL}$. The formulas are going to be expressions $\alpha\vee\beta\vee\gamma$, where $\alpha,\beta,\gamma$ are (as usual) any generalized literals. The generalized literals are essentially linear equations over $\mathbb{Z}_2$, and for variables $x_1,\ldots...
Další informace