Now showing items 1-4 of 4

• #### Clique is hard on average for regular resolution ﻿

(Association for Computing Machinery (ACM), 2018)
Conference report
Open Access
We prove that for k ≪4√n regular resolution requires length nΩ(k) to establish that an Erdős–Rényi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative ...
• #### Narrow proofs may be maximally long ﻿

(2016-07-03)
Article
Open Access
We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n(Omega(w)). This shows that the simple counting argument that any formula refutable ...
• #### Narrow proofs may be maximally long ﻿

(Institute of Electrical and Electronics Engineers (IEEE), 2014)
Conference report
Open Access
We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n¿(w). This shows that the simple counting argument that any formula refutable in ...
• #### Trade-offs between time and memory in a tighter model of CDCL SAT solvers ﻿

(2016)
Conference report
Open Access
A long line of research has studied the power of conflict- driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially ...