I know from Schaefer's Dichotomy Theorem that only a few types of satisfiability problems are in P and any other problem is NP-complete. However, all of the algorithms I know for them use specific techniques unique to that type of problem- e.g. unit propagation for Hornsat, linear algebraic techniques mod 2 for XORSAT, and various other techniques for 2-sat. Is there one general polytime algorithm which works for all of these problems in P? Thanks.
1
-
$\begingroup$ the question is not actually all that meaningful because there is no technical way to differentiate "different algorithms". an algorithm that calls lots of different algorithms as subroutines is still an algorithm. however, there is a natural conjecture here that maybe a more unified approach exists. $\endgroup$– vznJan 27, 2015 at 18:31
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
4
Schaefer's dichotomy theorem is proved by dividing CSPs into two types: those that can be reduced to one of a few specific problems in P, and the other to which SAT can be reduced (and so are NP-complete). Specifically, every CSP of the former type is either trivial (always satisfied by the constant 0 or the constant 1 assignment), can be reduced to 2SAT, can be reduced to HORN-SAT, or can be reduced to XOR-SAT. These are the only algorithms you need to solve these CSPs. There is no one single algorithm – there is a finite list of algorithms.
answered Jan 27, 2015 at 1:09
-
$\begingroup$ Thanks. Is it provable that there are no other algorithms other than this finite list or is that just what we assume? $\endgroup$– AriJan 27, 2015 at 2:39
-
$\begingroup$ A more detailed statement of Schaefer's theorem includes this result. In the setting of the theorem, it is provable that this list is all that is required. $\endgroup$ Jan 27, 2015 at 2:41
-
$\begingroup$ Given a formula $f$, are there algorithms to determine which category $f$ falls into? $\endgroup$– hengxinJan 29, 2015 at 5:54
-
$\begingroup$ The algorithm doesn't depend on the formula but on the allowed predicates. I believe it is possible to determine which class a CSP type falls into, but I'm not an expert on this issue. $\endgroup$ Jan 29, 2015 at 7:12
$\begingroup$
$\endgroup$
1
Look for papers/books written by Vijay Chandru, John Hooker and John Franco. Some of their techniques use Integer Programming (looking at special structures in the matrix generated by the CNF clauses of the SAT instance). The "extended Horn" formulas have a special structure when represented as graphs which make them polynomially solvable.
To quote Franco from his 2009 survey: The reader may have the impression that the number of polynomial time solvable classes is quite small due to the famous dichotomy theorem of Schaefer. But this is not the case. Schaefer proposed a scheme for defining classes of propositional expressions with a generalized notion of “clause.” He proved that every class definable within his scheme was either NP-complete or polynomial-time solvable, and he gave criteria to determine which. But not all classes can be defined within his scheme. The Horn and XOR classes can be, but we will describe several others including q-Horn, extended Horn, CC-balanced and SLUR that cannot be so defined. The reason is that Schaefer’s scheme is limited to classes that can be recognized in log space.
answered Jan 28, 2015 at 1:10
-
$\begingroup$ A more refined picture is due to Allender et al.: eccc.hpi-web.de/report/2004/100/download. $\endgroup$ Jan 28, 2015 at 6:47