Sam Buss

SAT Conference 2025 Conference Paper

Redundancy Rules for MaxSAT

• Ilario Bonacina
• Maria Luisa Bonet
• Sam Buss
• Massimo Lauria

The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e. g. , able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et. al'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen et. al'22, Berg et. al'23, Bonacina et. al'24]. In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT. All our rules are polynomially checkable, unlike [Ihalainen et. al'22]. Moreover, they are simpler and weaker than [Berg et. al'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina et. al'24]. Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. This is easier to integrate with current solvers and proof checkers. We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle PHP^m_n falsifies at least m-n clauses.

STOC Conference 2023 Conference Paper

On the Consistency of Circuit Lower Bounds for Non-deterministic Time

• Albert Atserias
• Sam Buss
• Moritz Müller

We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory ‍V 2 0 is consistent with the conjecture that ‍NEXP ‍⊈ ‍P/poly, i.e., some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. Additionally, we establish a magnification result on the hardness of proving circuit lower bounds.

AIJ Journal 2021 Journal Article

Propositional proof systems based on maximum satisfiability

• Maria Luisa Bonet
• Sam Buss
• Alexey Ignatiev
• Antonio Morgado
• Joao Marques-Silva

The paper describes the use of dual-rail MaxSAT systems to solve Boolean satisfiability (SAT), namely to determine if a set of clauses is satisfiable. The MaxSAT problem is the problem of satisfying the maximum number of clauses in an instance of SAT. The dual-rail encoding adds extra variables for the complements of variables, and allows encoding an instance of SAT as a Horn MaxSAT problem. We discuss three implementations of dual-rail MaxSAT: core-guided systems, minimal hitting set (MaxHS) systems, and MaxSAT resolution inference systems. All three of these can be more efficient than resolution and thus than conflict-driven clause learning (CDCL). All three systems can give polynomial size refutations for the pigeonhole principle, the doubled pigeonhole principle and the mutilated chessboard principles. The dual-rail MaxHS MaxSat system can give polynomial size proofs of the parity principle. However, dual-rail MaxSAT resolution requires exponential size proofs for the parity principle; this is proved by showing that constant depth Frege augmented with the pigeonhole principle can polynomially simulate dual-rail MaxSAT resolution. Consequently, dual-rail MaxSAT resolution does not simulate cutting planes. We further show that core-guided dual-rail MaxSAT and weighted dual-rail MaxSAT resolution polynomially simulate resolution. Finally, we report the results of experiments with core-guided dual-rail MaxSAT and MaxHS dual-rail MaxSAT showing strong performance by these systems.

CSL Conference 2020 Conference Paper

Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs

• Sam Buss
• Anupam Das 0002
• Alexander Knop

This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs, deterministic or non-deterministic. Decision trees (DTs) are represented by a natural term syntax, inducing the system LDT, and non-determinism is modelled by including disjunction, ∨, as primitive (system LNDT). Branching programs generalise DTs to dag-like structures and are duly handled by extension variables in our setting, as is common in proof complexity (systems eLDT and eLNDT). Deterministic and non-deterministic branching programs are natural nonuniform analogues of log-space (L) and nondeterministic log-space (NL), respectively. Thus eLDT and eLNDT serve as natural systems of reasoning corresponding to L and NL, respectively. The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in LDT, LNDT, eLDT and eLNDT. We also compare them with Frege systems, constant-depth Frege systems and extended Frege systems.

SAT Conference 2019 Conference Paper

DRAT Proofs, Propagation Redundancy, and Extended Resolution

• Sam Buss
• Neil Thapen

Abstract We study the proof complexity of RAT proofs and related systems including BC, SPR, and PR which use blocked clauses and (subset) propagation redundancy. These systems arise in satisfiability (SAT) solving, and allow inferences which preserve satisfiability but not logical implication. We introduce a new inference SR using substitution redundancy. We consider systems both with and without deletion. With new variables allowed, the systems are known to have the same proof theoretic strength as extended resolution. We focus on the systems that do not allow new variables to be introduced. Our first main result is that the systems DRAT \({}^-\), DSPR \({}^-\) and DPR \({}^-\), which allow deletion but not new variables, are polynomially equivalent. By earlier work of Kiesl, Rebola-Pardo and Heule, they are also equivalent to DBC \({}^-\). Without deletion and without new variables, we show that SPR \({}^-\) can polynomially simulate PR \({}^-\) provided only short clauses are inferred by SPR inferences. Our next main results are that many of the well-known “hard” principles have polynomial size SPR \({}^-\) refutations (without deletions or new variables). These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies, and clique-coloring tautologies; SPR \({}^-\) can also handle or-fication and xor-ification. Our final result is an exponential size lower bound for RAT \({}^-\) refutations, giving exponential separations between RAT \({}^-\) and both DRAT \({}^-\) and SPR \({}^-\).

SAT Conference 2019 Conference Paper

DRMaxSAT with MaxHS: First Contact

• António Morgado 0001
• Alexey Ignatiev
• Maria Luisa Bonet
• João Marques-Silva 0001
• Sam Buss

Abstract The proof system of Dual-Rail MaxSAT (DRMaxSAT) was recently shown to be capable of efficiently refuting families of formulas that are well-known to be hard for resolution, concretely when the MaxSAT solving approach is either MaxSAT resolution or core-guided algorithms. Moreover, DRMaxSAT based on MaxSAT resolution was shown to be stronger than general resolution. Nevertheless, existing experimental evidence indicates that the use of MaxSAT algorithms based on the computation of minimum hitting sets (MHSes), i. e. MaxHS-like algorithms, are as effective, and often more effective, than core-guided algorithms and algorithms based on MaxSAT resolution. This paper investigates the use of MaxHS-like algorithms in the DRMaxSAT proof system. Concretely, the paper proves that the propositional encoding of the pigenonhole and doubled pigenonhole principles have polynomial time refutations when the DRMaxSAT proof system uses a MaxHS-like algorithm.

SODA Conference 2019 Conference Paper

Strategies for Stable Merge Sorting

• Sam Buss
• Alexander Knop

We introduce new stable natural merge sort algorithms, called 2-merge sort and α -merge sort. We prove upper and lower bounds for several merge sort algorithms, including Timsort, Shiver's sort, α -stack sorts, and our new 2-merge and α -merge sorts. The upper and lower bounds have the forms c · n log m and c · n log n for inputs of length n comprising m runs. For Timsort, we prove a lower bound of (1. 5 – o (1)) n log n. For 2-merge sort, we prove optimal upper and lower bounds of approximately (1. 089 ± o (1)) n log m. We state similar asymptotically matching upper and lower bounds for α -merge sort, when ϕ < α < 2, where ϕ is the golden ratio. Our bounds are in terms of merge cost; this upper bounds the number of comparisons and accurately models runtime. The merge strategies can be used for any stable merge sort, not just natural merge sorts. The new 2-merge and α -merge sorts have better worst-case merge cost upper bounds and are slightly simpler to implement than the widely-used Timsort; they also perform better in experiments.

AAAI Conference 2018 Conference Paper

MaxSAT Resolution With the Dual Rail Encoding

• Maria Luisa Bonet
• Sam Buss
• Alexey Ignatiev
• Joao Marques-Silva
• Antonio Morgado

Conflict-driven clause learning (CDCL) is at the core of the success of modern SAT solvers. In terms of propositional proof complexity, CDCL has been shown as strong as general resolution. Improvements to SAT solvers can be realized either by improving existing algorithms, or by exploiting proof systems stronger than CDCL. Recent work proposed an approach for solving SAT by reduction to Horn MaxSAT. The proposed reduction coupled with MaxSAT resolution represents a new proof system, DRMaxSAT, which was shown to enable polynomial time refutations of pigeonhole formulas, in contrast with either CDCL or general resolution. This paper investigates the DRMaxSAT proof system, and shows that DRMaxSAT p-simulates general resolution, that AC0 - Frege+PHP p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate AC0 -Frege+PHP or the cutting planes proof system.

TCS Journal 2015 Journal Article

Quasipolynomial size proofs of the propositional pigeonhole principle

• Sam Buss

Cook and Reckhow proved in 1979 that the propositional pigeonhole principle has polynomial size extended Frege proofs. Buss proved in 1987 that it also has polynomial size Frege proofs; these Frege proofs used a completely different proof method based on counting. This paper shows that the original Cook and Reckhow extended Frege proofs can be formulated as quasipolynomial size Frege proofs. The key point is that st-connectivity can be used to define the Cook–Reckhow construction.

MFCS Conference 2013 Conference Paper

Alternation Trading Proofs and Their Limitations

• Sam Buss

Abstract Alternation trading proofs are motivated by the goal of separating NP from complexity classes such as L ogspace or NL; they have been used to give super-linear runtime bounds for deterministic and co-nondeterministic sublinear space algorithms which solve the Satisfiability problem. For algorithms which use n o (1) space, alternation trading proofs can show that deterministic algorithms for Satisfiability require time greater than n cn for c < 2cos( π /7) (as shown by Williams [21, 19]), and that co-nondeterministic algorithms require time greater than n cn for \(c<\sqrt[3]{4}\) (as shown by Diehl, van Melkebeek and Williams [5]). It is open whether these values of c are optimal, but Buss and Williams [2] have shown that for deterministic algorithms, c < 2cos( π /7) is the best that can obtained using present-day known techniques of alternation trading. This talk will survey alternation trading proofs, and discuss the optimality of the unlikely value of 2cos( π /7).

IJCAI Conference 2013 Conference Paper

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)

• Maria Luisa Bonet
• Sam Buss

We establish the unexpected power of conflict driven clause learning (CDCL) proof search by proving that the sets of unsatisfiable clauses obtained from the guarded graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. We further show that, under the correct heuristic choices, these refutations can be carried out in polynomial time by CDCL proof search without restarts, even when restricted to greedy, unitpropagating search. The guarded graph tautologies had been conjectured to separate CDCL without restarts from resolution; our results refute this conjecture.

SAT Conference 2012 Conference Paper

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning

• Maria Luisa Bonet
• Sam Buss

Abstract We prove that the graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses and without degenerate resolution inferences. These graph tautology principles can be refuted by polynomial size DPLL proofs with clause learning, even when restricted to greedy, unit-propagating DPLL search.

FOCS Conference 2002 Conference Paper

A Switching Lemma for Small Restrictions and Lower Bounds for k - DNF Resolution

• Nathan Segerlind
• Sam Buss
• Russell Impagliazzo

We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to DNFs with small conjunctions. We use this to prove lower bounds for the Res(k) propositional proof system, an extension of resolution which works with k-DNFs instead of clauses. We also obtain an exponential separation between depth d circuits of bottom fan-in k and depth d circuits of bottom fan-in k+1. Our results for Res(k) are: 1. The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k), for k /spl les/ /spl radic/(log n/ log log n). 2. For each constant k, there exists a constant w > k so that random w-CNFs require exponential size to refute in Res(k). 3. For each constant k, there are sets of clauses which have polynomial size Res(k+1) refutations, but which require exponential size Res(k) refutations.

STOC Conference 1999 Conference Paper

Linear Gaps Between Degrees for the Polynomial Calculus Modulo Distinct Primes

• Sam Buss
• Dima Grigoriev
• Russell Impagliazzo
• Toniann Pitassi

MFCS Conference 1998 Conference Paper

Minimum Propositional Proof Length is NP-Hard to Linearly Approximate

• Michael Alekhnovich
• Sam Buss
• Shlomo Moran
• Toniann Pitassi

Abstract We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within any constant factor. These results hold for all Frege systems, for all extended Frege systems, for resolution and Horn resolution, and for the sequent calculus and the cut-free sequent calculus. Also, if NP is not in \(QP = DTIME(n^{log^{O(1)} n} )\), then it is impossible to approximate minimum propositional proof length within a factor of \(2^{log^{(1 - \varepsilon )} n}\) for any є > 0. All these hardness of approximation results apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and prove the same hardness results for Monotone Minimum (Circuit) Satisfying Assignment.

CSL Conference 1998 Conference Paper

Resolution and the Weak Pigeonhole Principle

• Sam Buss
• Toniann Pitassi

Abstract We give new upper bounds for resolution proofs of the weak pigeonhole principle. We also give lower bounds for tree-like resolution proofs. We present a normal form for resolution proofs of pigeonhole principles based on a new monotone resolution rule.

CSL Conference 1995 Conference Paper

How to Lie Without Being (Easily) Convicted and the Length of Proofs in Propositional Calculus

• Pavel Pudlák
• Sam Buss

Abstract We shall describe two general methods for proving lower bounds on the lengths of proofs in propositional calculus and give examples of such lower bounds. One of the methods is based on interactive proofs where one player is claiming that he has a falsifying assignment for a tautology and the second player is trying to convict him of a lie. The second method is based on boolean valuations. For the first method, a log n + log log n -O (logloglog n ) lower bound is given on the lengths of interactive proofs of certain permutation tautologies.

SODA Conference 1994 Conference Paper

Linear and O(n log n) Time Minimum-Cost Matching Algorithms for Quasi-Convex Tours

• Sam Buss
• Peter N. Yianilos

FOCS Conference 1990 Conference Paper

On the Predictability of Coupled Automata: An Allegory about Chaos

• Sam Buss
• Christos H. Papadimitriou
• John N. Tsitsiklis

The authors show a sharp dichotomy between systems of identical automata with symmetric global control whose behavior is easy to predict and those whose behavior is hard to predict. The division pertains to whether the global control rule is invariant with respect to permutations of the states of the automaton. It is also shown that testing whether the global control rule has this invariance property is an undecidable problem. It is argued that there is a natural analog between complexity in the present model and chaos in dynamical systems. >

STOC Conference 1987 Conference Paper

The Boolean Formula Value Problem Is in ALOGTIME

• Sam Buss

STOC Conference 1985 Conference Paper

The Polynomial Hierarchy and Fragments of Bounded Arithmetic (Extended Abstract)

• Sam Buss