Using the Groebner basis algorithm to find proofs of unsatisfiability

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Using the Groebner basis algorithm to find proofs of unsatisfiability

Full text

Pdf (1.08 MB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the twenty-eighth annual ACM symposium on Theory of computing table of contents

Philadelphia, Pennsylvania, United States

Pages: 174 - 183

Year of Publication: 1996

ISBN:0-89791-785-5

Authors

Matthew Clegg	Computer Science Dept., UCSD 9500 Gilman Drive, La Jolla, CA
Jeffery Edmonds	Computer Science Dept., York University, Toronto, Ontario, Canada
Russell Impagliazzo	Computer Science and Engineering, UC, San Diego 9500 Gilman Drive, La Jolla, CA

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 56, Citation Count: 26

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/237814.237860 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	BIK+94	P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi, and P. Pudlak Lower bounds on Hilbert's Nullstellensatz and propositional proofs in 35th Annual Symposium on Foundations o/Computer Science, pages 794-806, Santa Fe, November 1994.
	BCE+95	Paul Beame , Stephen Cook , Jeff Edmonds , Russell Impagliazzo , Toniann Pitassi, The relative complexity of NP search problems, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.303-314, May 29-June 01, 1995, Las Vegas, Nevada, United States [doi>10.1145/225058.225147]
	B65	B. Buchberger, Ein Algorithmus zum Auftinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal, (An algorithm for finding a basis for the residue class ring of a zerodimensional polynomial ideal). Doctoral Dissertation Math. Inst. University of Innsbruck, Austria.
	B79	Bruno Buchberger, A criterion for detecting unnecessary reductions in the construction of Groebner bases, Proceedings of the International Symposiumon on Symbolic and Algebraic Computation, p.3-21, June 01, 1979
	BP	S. Buss and T. Pitassi, to appear in ll~th Computational Complexity, 1996.
	CI	M. Clegg and R. Impagliazzo. "Homogenization and Nullstellensatz Degrees". In preparation.
	CW	M. Clegg and N. Wallach, "Groebner: A Commutative Algebra Package for Distributed Networks of Workstations". In preparation.
	CLO	D. Cox, J. Little, D. O'Shea, Ideals, Varieties and Algorithms, Springer, 1992.
	IM	K. Iwama , E. Miyano, Intriactability of Read-Once Resolution, Proceedings of the 10th Annual Structure in Complexity Theory Conference (SCT'95), p.29, June 19-22, 1995
	KS	S. Kirkpatrick and B. Selman, Critical Behavior in the Satisfiability of Random Boolean Expressions. Science, Vol. 264, May 1994, 1297-1301.
	L	L. Lovasz, On the Shannon Capacity of a graph, Transactions on Information Theory, vol. 25, No. 1, January, 1979
	P	T. Pitassi, personal communication, 1995.
	RR	Alexander A. Razborov , Steven Rudich, Natural proofs, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.204-213, May 23-25, 1994, Montreal, Quebec, Canada [doi>10.1145/195058.195134]
	S	B. Selman, personal communication, 1995.

CITED BY 26

	Paul Beame , Richard Karp , Toniann Pitassi , Michael Saks, On the complexity of unsatisfiability proofs for random k-CNF formulas, Proceedings of the thirtieth annual ACM symposium on Theory of computing, p.561-571, May 24-26, 1998, Dallas, Texas, United States
	Eli Ben-Sasson , Avi Wigderson, Short proofs are narrow—resolution made simple, Proceedings of the thirty-first annual ACM symposium on Theory of computing, p.517-526, May 01-04, 1999, Atlanta, Georgia, United States
	Alexis Maciel , Toniann Pitassi, On ACC0[pk] Frege proofs, Proceedings of the twenty-ninth annual ACM symposium on Theory of computing, p.720-729, May 04-06, 1997, El Paso, Texas, United States
	David Eppstein, Fast hiearchical clustering and other applications of dynamic closet pairs, Proceedings of the ninth annual ACM-SIAM symposium on Discrete algorithms, p.619-628, January 25-27, 1998, San Francisco, California, United States
	Sam Buss , Dima Grigoriev , Russell Impagliazzo , Toniann Pitassi, Linear gaps between degrees for the polynomial calculus modulo distinct primes, Proceedings of the thirty-first annual ACM symposium on Theory of computing, p.547-556, May 01-04, 1999, Atlanta, Georgia, United States
	Dima Grigoriev , Edward A. Hirsch, Algebraic proof systems over formulas, Theoretical Computer Science, v.303 n.1, p.83-102, 28 June 2003
	Juan Luis Esteban , Jacobo Torán, A combinatorial characterization of treelike resolution space, Information Processing Letters, v.87 n.6, p.295-300, 30 September 2003
	Maria Luisa Bonet , Nicola Galesi, Optimality of size-width tradeoffs for resolution, Computational Complexity, v.10 n.4, p.261-276, May 2002
	Eli Ben-Sasson , Avi Wigderson, Short proofs are narrow—resolution made simple, Journal of the ACM (JACM), v.48 n.2, p.149-169, March 2001
	Juan Luis Esteban , Jacobo Torán, Space bounds for resolution, Information and Computation, v.171 n.1, p.84-97, November 25, 2001
	Alexander A. Razborov, Resolution lower bounds for the weak functional pigeonhole principle, Theoretical Computer Science, v.303 n.1, p.233-243, 28 June 2003
	David Eppstein, Fast hierarchical clustering and other applications of dynamic closest pairs, Journal of Experimental Algorithmics (JEA), 5, p.1-es, 2000
	Joshua Buresh-Oppenheim , Matthew Clegg , Russell Impagliazzo , Toniann Pitassi, Homogenization and the polynomial calculus, Computational Complexity, v.11 n.3/4, p.91-108, March 2003
	Eli Ben-Sasson, Size space tradeoffs for resolution, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada
	K. Subramani, Optimal length tree-like resolution refutations for 2SAT formulas, ACM Transactions on Computational Logic (TOCL), v.5 n.2, p.316-320, April 2004
	Russell Impagliazzo , Nathan Segerlind, Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations, ACM Transactions on Computational Logic (TOCL), v.7 n.2, p.199-218, April 2006
	Paul Beame , Joseph Culberson , David Mitchell , Cristopher Moore, The resolution complexity of random graphk-colorability, Discrete Applied Mathematics, v.153 n.1, p.25-47, 1 December 2005
	Sivaram Gopalakrishnan , Priyank Kalla , M. Brandon Meredith , Florian Enescu, Finding linear building-blocks for RTL synthesis of polynomial datapaths with fixed-size bit-vectors, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
	Oliver Kullmann, Upper and Lower Bounds on the Complexity of Generalised Resolution and Generalised Constraint Satisfaction Problems, Annals of Mathematics and Artificial Intelligence, v.40 n.3-4, p.303-352, March 2004
	Quocnam Tran , Moshe Y. Vardi, Groebner bases computation in Boolean rings for symbolic model checking, Proceedings of the 18th conference on Proceedings of the 18th IASTED International Conference: modelling and simulation, p.440-445, May 30-June 01, 2007, Montreal, Canada
	Albert Atserias , Víctor Dalmau, A combinatorial characterization of resolution width, Journal of Computer and System Sciences, v.74 n.3, p.323-334, May, 2008
	Michael L. Littman , Stephen M. Majercik , Toniann Pitassi, Stochastic Boolean Satisfiability, Journal of Automated Reasoning, v.27 n.3, p.251-296, October 2001
	Misha Alekhnovich , Mark Braverman , Vitaly Feldman , Adam R. Klivans , Toniann Pitassi, The complexity of properly learning simple concept classes, Journal of Computer and System Sciences, v.74 n.1, p.16-34, February, 2008
	Toniann Pitassi , Nathan Segerlind, Exponential lower bounds and integrality gaps for tree-like Lovász-Schrijver procedures, Proceedings of the Nineteenth Annual ACM -SIAM Symposium on Discrete Algorithms, p.355-364, January 04-06, 2009, New York, New York
	Giordano Fusco , Eric Bach, Phase transition of multivariate polynomial systems, Mathematical Structures in Computer Science, v.19 n.1, p.9-23, February 2009
	Heidi E. Dixon , Matthew L. Ginsberg , Andrew J. Parkes, Generalizing Boolean satisfiability I: background and survey of existing work, Journal of Artificial Intelligence Research, v.21 n.1, p.193-243, January 2004