Tag Info

48

SAT, CP, SMT, (much of) ASP all deal with the same set of combinatorial optimisation problems. However, they come at these problems from different angles and with different toolboxes. These differences are largely in how each approach structures information about the exploration of the search space. My working analogy is that SAT is machine code, while the ...

35

It is an Unordered Constraint Satisfaction game and it is PSPACE-complete and it has been proved to be PSPACE-complete only recently; a proof can be found in: Lauri Ahlroth and Pekka Orponen, Unordered Constraint Satisfaction Games. Lecture Notes in Computer Science Volume 7464, 2012, pp 64-75. Abstract: We consider two-player constraint satisfaction ...

31

Indeed, as wwjohnsmith1 said, you can get a square root speed-up over Schöning's algorithm for 3-SAT, but also more generally for Schöning's algorithm for k-SAT. In fact, many randomized algorithms for k-SAT can be implemented quadratically faster on a quantum computer. The reason for this general phenomenon is the following. Many randomized algorithms for ...

30

No. If the 3-SAT instance has $m$ clauses, then you can test satisfiability in $O(m 2^N)$ time. Since $N$ is a fixed constant, this is a polynomial-time algorithm that solves all instances of your problem. The algorithm works in $m$ stages. Let $\varphi_i$ denote the formula consisting of the clauses that use only variables from $x_1,\dots,x_i$. Let $... 27 It may also be worthwhile to note that this problem was also solved in the 70's by Thomas Schaefer in ￼Complexity of decision problems based on finite two-person perfect-information games. In fact, he proves a slightly stronger result in that the language remains PSPACE-complete even when restricted to positive CNF formulas. 26 Yes, there has been. Moshe Vardi recently gave a survey talk at BIRS Theoretical Foundations of Applied SAT Solving workshop: Moshe Vardi, Phase transitions and computational complexity, 2014. (Moshe presents the graph of their experiment a bit after minute 14:30 in his talk linked above.) Let$\rho$denote the clause ratio. As the value of$\rho$... 26 You can just take the oracle A s.t. NP$^A$=EXP$^A$since EXP is not in i.o.-subexp. For SAT$^A$it depends on the encoding, for example if the only valid SAT instances have even length then it is easy to solve SAT on odd-length strings. But if you use a language like$L=\{\phi 01^*\ |\ \phi\in SAT^A\}$then you should be fine. 23 You need to understand that$\mathsf{CSP}$problems have a structure that generic$\mathbf{SAT}$problems do not have. I will give you a simple example. Let$\Gamma=\{\{(0,0),(1,1)\},\{(0,1),(1,0)\}\}$. This language is such that you can only express equality and inequality between two variables. Clearly any such set of constraints is ... 22 If I may, quite blatantly, advertise myself, we wrote an article about this last year Abstraction-Based Algorithm for 2QBF. I've got an implementation for qdimacs, which I can provide if you wish but from my experience, one can benefit greatly from specializing the algorithm for a particular problem. There is also an older paper A Comparative Study of 2QBF ... 22 I think one can obtain a non-trivial upper bound from quantum computing by speeding up the randomized algorithms of Schöning for 3-SAT. The algorithm of Schöning runs in time$(4/3)^n$and using standard amplitude amplification techniques one can obtain a quantum algorithm that runs in time$(2/\sqrt{3})^n=1.15^n$which is significantly faster than ... 21 You can find a preprint by following this link http://eccc.hpi-web.de/report/2016/002/ EDIT (1/24) By request, here is a quick summary, taken from the paper itself, but glossing over many things. Suppose Merlin can prove to Arthur that for a$k$-variable arithmetic circuit$C$, its value on all points in$\{0,1\}^k$is a certain table of$2^k$field ... 21 I am assuming that you are referring to CDCL SAT solvers on benchmark data sets like those used in the SAT Competition. These programs are based on many heuristics and lots of optimization. There were some very good introductions to how they work at Theoretical Foundations of Applied SAT Solving workshop at Banff in 2014 (videos). These algorithms are based ... 20 This is still #P-complete [1]. This problem is usually referred to as montone (#)SAT. Monotone #2-SAT is already #P-complete (this is equivalent to counting vertex covers of a graph). [1] Roth, Dan. "On the hardness of approximate reasoning." Artificial Intelligence 82.1-2 (1996): 273-302. 19 There are at least two lines of research concerning random$k\text-\mathsf{SAT}$for formulas with a clause/variable-ratio larger than the satisfiability threshold: For such formulas lower bounds on the length of refutations in resolution and stronger propositional proof systems have been shown, starting with the paper "Many hard examples for resolution" by ... 19 A family of bitvectors is the class of solutions to a 2-SAT problem if and only if it has the median property: if you apply the bitwise majority function to any three solutions you get another solution. See e.g. https://en.wikipedia.org/wiki/Median_graph#2-satisfiability and its references. So if you can find three solutions for which this is not true, then ... 18 SETH says that for all$\delta < 1$there is a$k$such that$k$-SAT requires$2^{\delta n}$time to be solved in the worst-case. The computational model is generally taken to be the random-access machine or pointer machine model, which allows for$O(\log N)$time access to a storage of$N$items, and is generally assumed to also be probabilistic with ... 17 (Making comment an answer as requested and expanding a bit.) "A curious mind" should read Schaefer's dichotomy theorem and the generalization by Allender et al. that shows that every possible SAT variant is either trivial or in one of six well-known complexity classes: NP-complete P-complete NL-complete L-complete ⊕L-complete co-NLOGTIME 17 This list will be very long;) Here are some of my favourite (NP-complete) variants of SAT: PLANAR($\le 3, 3$)-SAT (each clause contains at least two and at most three literals, each variable appears in exactly three clauses; twice in its non-negated form, and once in its negated form, and the bipartite incidence graph is planar.) See: Dahlhaus, Johnson, ... 17 It is possible ;-) It would give new circuit lower bounds. Since you are making a pretty strong assumption this could follow from the seminal work by Impagliazzo, Kabanets, and Wigderson, I haven't checked. If you use Williams' approach, tightened here, you get a lower bound of$n^{1+\Omega(1)}$for a function on$n$bits in the class E$^{NP}$. (For this ... 17 I am typing this quite quickly due to severe time constraints (and didn't even get to responding earlier for the same reason), but I thought I would try to at least chip in with my two cents. I think this is a truly great question, and have spent a nontrivial amount of time over the last few years looking into this. (Full disclosure: I have received a big ... 16 A monotone 1-in-2 clause demands that the two variables have different values. Thus, you can model the problem as a graph problem, with one vertex per variable which is to be colored black or white, and an edge for a clause indicating the colors need to be different. Thus, the question is to make the graph bipartite by deleting a minimum number of edges. ... 16 You don't have to go to the lengths Lance was suggesting. For example, relative to a random oracle, using the oracle as a one-way function (say, evaluated on consecutive bit postions) is exponentially hard to invert on all but finitely many lengths. This problem directly reduces to SAT on the same length input, so it does follow that SAT^A is not in ... 16 Given a satisfiable 2-CNF$\phi$, you can compute a particular satisfying assignment$e$by an NL-function (that is, there is an NL-predicate$P(\phi,i)$that tells you whether$e(x_i)$is true). One way to do that is described below. I will freely use the fact that NL is closed under$\mathrm{AC}^0$-reductions, hence NL-functions are closed under ... 16 Let me add my two cents of understanding to this, even though I've never actually worked in the area. You're asking one of two questions, "what are all the known approaches to proving theoretical efficiency of some SAT solver for some type of instances" and "why are SAT solvers efficient in reality". For the former question, I'll just direct you to the ... 16 Incident graph of a SAT formula is a bipartite graph that has a vertex for each clause and each variable. We add edges between a clause and all of its variables. If the incident graph has bounded treewidth then we can decide the SAT formula in P, actually we can do much more. Your incident graph is very restricted. E.g it is a bounded pathwidth graph, so it ... 15 As Massimo Lauria states, problems of the form CSP($\Gamma$) are rather special. So there is no contradiction. Any constraint satisfaction problem instance can be represented as a pair$(S,T)$of relational structures$S$and$T$, and one has to decide if there exists a relational structure homomorphism from the source$S$to the target$T$. CSP($\Gamma$... 15 As was pointed out at the beginning of this discussion in the comments, there is not necessarily a single "right" definition for random$k$-SAT. That said, the two most common variants of random$k$-SAT are both fixed clause length (FCL) models, meaning that exactly$k\$ literals appear in each clause. These variants both disallow repeated variables and ...

15

#3-Regular Bipartite Planar Vertex Cover is #P-Complete As counting vertex covers is exactly the same as counting satisfying assignments of a monotone #2-SAT instance, the above result implies that it is #P-complete to count satisfying assignments of a #2-SAT instance which is monotone and 3-regular and bipartite and planar. This in turn means that, in ...

15

There is a paper "Relating Proof Complexity Measures and Practical Hardness of SAT" by Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný in CP '12 that attempts to link the hardness or easiness of solving certain formulas by CDCL solvers with resolution proof complexity measures, in particular resolution proof space. The results are ...

Only top voted, non community-wiki answers of a minimum length are eligible