Sat, 26 Jul 2008 06:32:45 BST CiteULike: johannsen's library [12 articles] http://www.citeulike.org/user/johannsen CiteULike.org en-gb Copyright © 2004-2008 citeulike.org http://www.citeulike.org/user/johannsen/article/272489 <i>Journal of Logic and Computation, Vol. 15, No. 4. (August 2005), pp. 433-446.</i> Uniform Proof Complexity Arnold Beckmann doi:10.1093/logcom/exi035 Journal of Logic and Computation, Vol. 15, No. 4. (August 2005), pp. 433-446. 2005-08-04T01:29:45-00:00 2005 Journal of Logic and Computation 0955-792X 15 4 433 446 Oxford University Press proof_complexity http://www.citeulike.org/user/johannsen/article/139140 <i>Theoretical Computer Science, Vol. 329, No. 1-3. (13 December 2004), pp. 1-45.</i><br /><br />We apply techniques from the theory of approximation algorithms to the problem of deciding whether a random k-SAT formula is satisfiable. Let Formn,k,m denote a random k-SAT instance with n variables and m clauses. Using known approximation algorithms for MAX CUT or MIN BISECTION, we show how to certify that Formn,4,m is unsatisfiable efficiently, provided that m[greater-or-equal, slanted]Cn2 for a sufficiently large constant C>0. In addition, we present an algorithm based on the Lovasz [theta] function that decides within polynomial expected time whether Formn,k,m is satisfiable, provided that k is even and m[greater-or-equal, slanted]C[middle dot]4knk/2. Finally, we present an algorithm that approximates random MAX 2-SAT on input Formn,2,m within a factor of 1-O(n/m)1/2 in expected polynomial time, for m[greater-or-equal, slanted]Cn. Techniques from combinatorial approximation algorithms yield efficient algorithms for random 2k-SAT Amin Coja-Oghlan Andreas Goerdt Andre Lanka Frank Schadlich doi:10.1016/j.tcs.2004.07.017 Theoretical Computer Science, Vol. 329, No. 1-3. (13 December 2004), pp. 1-45. 2005-03-24T15:08:29-00:00 2004 Theoretical Computer Science 329 1-3 1 45 sat http://www.citeulike.org/user/johannsen/article/131999 <i>Annals of Pure and Applied Logic, Vol. 126, No. 1-3. (April 2004), pp. 255-280.</i><br /><br />We define and study a new restricted consistency notion RCon*(T2j) for bounded arithmetic theories T2j. It is the strongest [forall][Pi]1b-statement over S21 provable in T2j, similar to Con(Gi) in Krajicek and Pudlak, (Z. Math. Logik Grundl. Math. 36 (1990) 29) or RCon(Ti1) in Krajicek and Takeuti (Ann. Math. Artificial Intelligence 6 (1992) 107). The advantage of our notion over the others is that RCon*(T2j) can directly be used to construct models of T2j. We apply this by proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The [forall][Pi]1b-separation of bounded arithmetic theories S2i from T2j (1[les]i[les]j) is equivalent to the existence of a model of S2i which does not have a [Delta]0b-elementary extension to a model of T2j.More specific, let M [vDash] [Omega]1nst denote that there is a nonstandard element c in M such that the function n |-> 2log(n)c is total in M. Let BL[Sigma]1b be the bounded collection schema for [Sigma]1b-formulas. We obtain the following preservation results: the [forall][Pi]1b-separation of S2i from T2j (1[les]i[les]j) is equivalent to the existence of 1. a model of S2i+[Omega]1nst which is 1b-closed w.r.t. T2j,2. a countable model of S2i+BL[Sigma]1b without weak end extensions to models of T2j. Preservation theorems and restricted consistency statements in bounded arithmetic Arnold Beckmann doi:10.1016/j.apal.2003.11.003 Annals of Pure and Applied Logic, Vol. 126, No. 1-3. (April 2004), pp. 255-280. 2005-03-18T11:21:04-00:00 2004 Annals of Pure and Applied Logic 126 1-3 255 280 bounded_arithmetic http://www.citeulike.org/user/johannsen/article/131998 <i>Annals of Pure and Applied Logic, Vol. 129, No. 1-3. (October 2004), pp. 1-37.</i><br /><br />We study the extension (introduced as BT by Krajicek in Fund. Math. 170 (2001) 123) of the theory S21 by instances of the dual (onto) weak pigeonhole principle for p-time functions, dWPHP(PV)x2x. We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie's witnessing theorem for S21+dWPHP(PV). We construct a propositional proof system WF (based on a reformulation of Extended Frege in terms of Boolean circuits), which captures the [forall][Pi]1b-consequences of S21+dWPHP(PV). We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of Buss et al. (Comput. Complexity 6 (1996/1997) 256).We prove that dWPHP(PV) is (over S21) equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan-Wigderson construction (derandomization of probabilistic p-time algorithms) in a conservative extension of S21+dWPHP(PV). Dual weak pigeonhole principle, Boolean complexity, and derandomization Emil Jerabek doi:10.1016/j.apal.2003.12.003 Annals of Pure and Applied Logic, Vol. 129, No. 1-3. (October 2004), pp. 1-37. 2005-03-18T11:18:24-00:00 2004 Annals of Pure and Applied Logic 129 1-3 1 37 bounded_arithmetic http://www.citeulike.org/user/johannsen/article/131997 <i>Annals of Pure and Applied Logic, Vol. In Press, Corrected Proof</i><br /><br />We present a new functional interpretation, based on a novel assignment of formulas. In contrast with Godel's functional "Dialectica" interpretation, the new interpretation does not care for precise witnesses of existential statements, but only for bounds for them. New principles are supported by our interpretation, including (a version of) the FAN theorem, weak Konig's lemma and the lesser limited principle of omniscience. Conspicuous among these principles are also refutations of some laws of classical logic. Notwithstanding, we end up discussing some applications of the new interpretation to theories of classical arithmetic and analysis. Bounded functional interpretation Fernando Ferreira Paulo Oliva doi:10.1016/j.apal.2004.11.001 Annals of Pure and Applied Logic, Vol. In Press, Corrected Proof 2005-03-18T11:15:37-00:00 Annals of Pure and Applied Logic In Press, Corrected Proof bounded_arithmetic http://www.citeulike.org/user/johannsen/article/131996 <i>Annals of Pure and Applied Logic, Vol. 133, No. 1-3. (May 2005), pp. 275-292.</i><br /><br />There is a very simple way in which the safe/normal variable discipline of Bellantoni-Cook recursion [S. Bellantoni, S. Cook, A new recursion theoretic characterization of the polytime functions, Computational Complexity 2 (1992) 97-110] can be imposed on arithmetical theories like PA: quantify over safes and induct on normals. This weakens the theory severely, so that the provably recursive functions become more realistically computable (slow growing rather than fast growing). Earlier results of D. Leivant [Intrinsic theories and computational complexity, in: D. Leivant (Ed.), Logic and Computational Complexity, Lecture Notes in Computer Science, vol. 960, Springer-Verlag, 1995, pp. 177-194] are re-worked and extended in this new context, giving proof-theoretic characterizations (according to the levels of induction used) of complexity classes between Grzegorczyk's E2 and E3. Elementary arithmetic G Ostrin S Wainer doi:10.1016/j.apal.2004.10.012 Annals of Pure and Applied Logic, Vol. 133, No. 1-3. (May 2005), pp. 275-292. 2005-03-18T11:13:37-00:00 2005 Annals of Pure and Applied Logic 133 1-3 275 292 bounded_arithmetic icc http://www.citeulike.org/user/johannsen/article/130316 <i>(1990), pp. 1-33.</i><br /><br />Many different methods have been devised for automatically verifying finite state systems by examining state-graph models of system behavior. These methods all depend on decision procedures that explicitly represent the state space using a list or a table that grows in proportion to the number of states. We describe a general method that represents the state space symbolically instead of explicitly. The generality of our method comes from using a dialect of the Mu-Calculus as the primary... Symbolic Model Checking: $10^20$ States and Beyond J Burch E Clarke K Mcmillan D Dill L Hwang (1990), pp. 1-33. 2005-03-16T23:06:31-00:00 1990 1 33 IEEE Computer Society Press modelchecking http://www.citeulike.org/user/johannsen/article/130909 <i></i><br /><br />We give a randomized algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. Its running time is at most $2^n(1-1/alpha)$ up to a polynomial factor, where $alpha = ln(m/n) + O(ln ln m)$ and $n$, $m$ are respectively the number of variables and the number of clauses in the input formula. This bound is asymptotically better than the previously best known $2^n(1-1/log(2m))$ bound for SAT. An Improved Upper Bound for SAT Evgeny Dantsin Alexander Wolpert 2005-03-17T09:28:22-00:00 sat http://www.citeulike.org/user/johannsen/article/80546 <i></i> Two-Sorted Theories for L, SL, NL and P Phuong Nguyen 2005-01-20T00:29:54-00:00 bounded_arithmetic icc http://www.citeulike.org/user/johannsen/article/130904 <i>Theoretical Computer Science, Vol. 329, No. 1-3. (13 December 2004), pp. 303-313.</i><br /><br />We slightly improve the pruning technique presented in Dantsin et al. (Theoret. Comput. Sci. 289 (2002) 69) to obtain an O*(1.473n) deterministic algorithm for 3-SAT. An improved deterministic local search algorithm for 3-SAT Tobias Brueggemann Walter Kern doi:10.1016/j.tcs.2004.08.002 Theoretical Computer Science, Vol. 329, No. 1-3. (13 December 2004), pp. 303-313. 2005-03-17T08:57:32-00:00 2004 Theoretical Computer Science 329 1-3 303 313 sat http://www.citeulike.org/user/johannsen/article/130903 <i>Theoretical Computer Science, Vol. 329, No. 1-3. (13 December 2004), pp. 159-176.</i><br /><br />We provide a natural characterization of the type two Mehlhorn-Cook-Urquhart basic feasible functionals as the provably total type two functionals of our (classical) applicative theory PT introduced in (Inform. Comput. 185 (2003) 263), thus providing a proof of a result claimed in the conclusion of Strahm (2003). This further characterization of the basic feasible functionals underpins their importance as a key candidate for the notion of type two feasibility. A proof-theoretic characterization of the basic feasible functionals Thomas Strahm doi:10.1016/j.tcs.2004.08.009 Theoretical Computer Science, Vol. 329, No. 1-3. (13 December 2004), pp. 159-176. 2005-03-17T08:55:52-00:00 2004 Theoretical Computer Science 329 1-3 159 176 icc http://www.citeulike.org/user/johannsen/article/130902 <i>Theoretical Computer Science, Vol. In Press, Uncorrected Proof</i><br /><br />(k,s)-SAT is the propositional satisfiability problem restricted to instances where each clause has exactly k distinct literals and every variable occurs at most s times. It is known that there exists an exponential function f such that for s[less-than-or-equals, slant]f(k) all (k,s)-SAT instances are satisfiable, but (k,f(k)+1)-SAT is already NP-complete (k[greater-or-equal, slanted]3). Exact values of f are only known for k=3 and 4, and it is open whether f is computable. We introduce a computable function f1 which bounds f from above and determine the values of f1 by means of a calculus of integer sequences. This new approach enables us to improve the best known upper bounds for f(k), generalizing the known constructions for unsatisfiable (k,s)-SAT instances for small k. Computing unsatisfiable k-SAT instances with few occurrences per variable Shlomo Hoory Stefan Szeider doi:10.1016/j.tcs.2005.02.004 Theoretical Computer Science, Vol. In Press, Uncorrected Proof 2005-03-17T08:51:55-00:00 Theoretical Computer Science In Press, Uncorrected Proof sat