Nachum Dershowitz
Abstract
We study—within the framework of propositional proof complexity—the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where many stands for an explicitly specified function Λ in the number of variables n. To this end, we develop propositional proof systems under different measures of promises (i.e., different Λ) as extensions of resolution. This is done by augmenting resolution with axioms that, roughly, can eliminate sets of truth assignments defined by Boolean circuits. We then investigate the complexity of such systems, obtaining an exponential separation in the average case between resolution under different size promises:
(1) Resolution has polynomial-size refutations for all unsatisfiable 3CNF formulas when the promise is ϵ…2n, for any constant 0<ϵ<1.
(2) There are no subexponential size resolution refutations for random 3CNF formulas, when the promise is 2Δ n, for any constant 0<δ<1 (and the number of clauses is O(n3/2-ϵ), for 0<ϵ<1/2).
“Goods Satisfactory or Money Refunded”
—The Eaton Promise
- Alekhnovich, M., Ben-Sasson, E., Razborov, A. A., and Wigderson, A. 2004. Pseudorandom generators in propositional proof complexity. SIAM J. Comput. 34, 1, 67--88. Google Scholar
Digital Library
- Beame, P., Karp, R., Pitassi, T., and Saks, M. 2002. The efficiency of resolution and Davis-Putnam procedures. SIAM J. Comput. 31, 4, 1048--1075. Google ScholarDigital Library
- Ben-Sasson, E. 2001. Expansion in proof complexity. Ph.D. dissertation. Hebrew University, Jerusalem, Israel.Google Scholar
- Ben-Sasson, E. and Wigderson, A. 2001. Short proofs are narrow—resolution made simple. J. ACM 48, 2, 149--169. Google ScholarDigital Library
- Cook, S. A. 1971. The complexity of theorem proving procedures. In Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing. ACM Press, New York, NY, 151--158. Google ScholarDigital Library
- Cook, S. A. and Reckhow, R. A. 1979. The relative efficiency of propositional proof systems. J. Symbol. Log. 44, 1, 36--50.Google ScholarCross Ref
- Feige, U., Kim, J. H., and Ofek, E. 2006. Witnesses for non-satisfiability of dense random 3CNF formulas. In Proceedings of the IEEE 47th Annual Symposium on Foundations of Computer Science. Google ScholarDigital Library
- Hirsch, E. 1998. A fast deterministic algorithm for formulas that have many satisfying assignments. Log. J. IGPL 6, 1, 59--71.Google ScholarCross Ref
- Krajíček, J. 2007a. Personal communication.Google Scholar
- Krajíček, J. 2007b. Substitutions into propositional tautologies. Inform. Process. Lett. 101, 163--167. Google ScholarDigital Library
- Pitassi, T. 2006. Using hardness in proof complexity. Talk given in New Directions in Proof Complexity, an Isaac Newton institute workshop, Cambridge.Google Scholar
- Razborov, A. A. and Rudich, S. 1997. Natural proofs. J. Comput. Syst. Sci. 55, 1, part 1, 24--35. Google ScholarDigital Library
- Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 1 (Jan.), 23--41. Google ScholarDigital Library
- Trevisan, L. 2004. A note on approximate counting for k-DNF. In Proceedings of the 7th International Workshop on Approximation Algorithms for Combinatorial Optimization Problems (APPROX 2004). Lecture Notes in Computer Science, vol. 3122. Springer, Berlin, Germany, 417--426.Google ScholarCross Ref
Index Terms
- Complexity of propositional proofs under a promise
Recommendations
Complexity of propositional proofs under a promise
ICALP'07: Proceedings of the 34th international conference on Automata, Languages and ProgrammingWe study - within the framework of propositional proof complexity - the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where "many" stands for an explicitly ...
On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs
CCC '08: Proceedings of the 2008 IEEE 23rd Annual Conference on Computational ComplexityWe show that tree-like OBDD proofs of unsatisfiability require an exponential increase (s 7! 2s(1)) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase (s 7! 22(...
MaxSAT resolution for regular propositional logic
AbstractProof systems for SAT are unsound for MaxSAT because they preserve satisfiability but fail to preserve the minimum number of unsatisfied clauses. Consequently, there has been a need to define cost-preserving resolution-style proof systems for ...
Comments