Standard

On Limits of Symbolic Approach to SAT Solving. / Itsykson, D.; Ovcharov, S.; Chakraborty, S. (редактор); Jiang, J.-H.R. (редактор).

2024. Работа представлена на 27th International Conference on Theory and Applications of Satisfiability Testing, Индия.

Результаты исследований: Материалы конференций › материалы › Рецензирование

Harvard

Itsykson, D, Ovcharov, S, Chakraborty, S (ред.) & Jiang, J-HR (ред.) 2024, 'On Limits of Symbolic Approach to SAT Solving', Работа представлена на 27th International Conference on Theory and Applications of Satisfiability Testing, Индия, 21/08/24 - 24/08/24. https://doi.org/10.4230/LIPIcs.SAT.2024.19

APA

Itsykson, D., Ovcharov, S., Chakraborty, S. (Ред.), & Jiang, J-HR. (Ред.) (2024). On Limits of Symbolic Approach to SAT Solving. Работа представлена на 27th International Conference on Theory and Applications of Satisfiability Testing, Индия. https://doi.org/10.4230/LIPIcs.SAT.2024.19

Vancouver

Itsykson D, Ovcharov S, Chakraborty S, (ed.), Jiang J-HR, (ed.). On Limits of Symbolic Approach to SAT Solving. 2024. Работа представлена на 27th International Conference on Theory and Applications of Satisfiability Testing, Индия. https://doi.org/10.4230/LIPIcs.SAT.2024.19

Author

Itsykson, D. ; Ovcharov, S. ; Chakraborty, S. (редактор) ; Jiang, J.-H.R. (редактор). / On Limits of Symbolic Approach to SAT Solving. Работа представлена на 27th International Conference on Theory and Applications of Satisfiability Testing, Индия.

BibTeX

@conference{4e93b359cbaf480181d7eb5bf47fab5e,
title = "On Limits of Symbolic Approach to SAT Solving",
abstract = "We study the symbolic approach to the propositional satisfiability problem proposed by Aguirre and Vardi in 2001 based on OBDDs and symbolic quantifier elimination. We study the theoretical limitations of the most general version of this approach where it is allowed to dynamically change variable order in OBDD. We refer to algorithms based on this approach as OBDD(∧,∃,reordering) algorithms. We prove the first exponential lower bound of OBDD(∧,∃,reordering) algorithms on unsatisfiable formulas, and give an example of formulas having short tree-like resolution proofs that are exponentially hard for OBDD(∧,∃,reordering) algorithms. We also present the first exponential lower bound for natural formulas with clear combinatorial meaning: every OBDD(∧,∃,reordering) algorithm runs exponentially long on the binary pigeonhole principle BPHPnn+1 {\textcopyright} 2024 Elsevier B.V., All rights reserved.",
keywords = "binary pigeonhole principle, error-correcting codes, lower bounds, OBDD, proof complexity, Symbolic quantifier elimination, tree-like resolution, Boolean functions, Consensus algorithm, Binary pigeonhole principle, Error correcting code, Exponentials, Low bound, Pigeonhole principle, Proof complexity, Quantifier elimination, Tree-like resolution, Trees (mathematics)",
author = "D. Itsykson and S. Ovcharov and S. Chakraborty and J.-H.R. Jiang",
note = "Export Date: 01 November 2025; Cited By: 0; Conference name: 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024; Conference location: Pune; Sahyadri Park Facility of Tata Consultancy Services; Conference sponsors: Advanced Micro Devices; Amazon Web Services; Cadence Design Systems; Google; Microsoft; Synopsys; null ; Conference date: 21-08-2024 Through 24-08-2024",
year = "2024",
doi = "10.4230/LIPIcs.SAT.2024.19",
language = "Английский",

}

RIS

TY - CONF

T1 - On Limits of Symbolic Approach to SAT Solving

AU - Itsykson, D.

AU - Ovcharov, S.

A2 - Chakraborty, S.

A2 - Jiang, J.-H.R.

N1 - Export Date: 01 November 2025; Cited By: 0; Conference name: 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024; Conference location: Pune; Sahyadri Park Facility of Tata Consultancy Services; Conference sponsors: Advanced Micro Devices; Amazon Web Services; Cadence Design Systems; Google; Microsoft; Synopsys

PY - 2024

Y1 - 2024

N2 - We study the symbolic approach to the propositional satisfiability problem proposed by Aguirre and Vardi in 2001 based on OBDDs and symbolic quantifier elimination. We study the theoretical limitations of the most general version of this approach where it is allowed to dynamically change variable order in OBDD. We refer to algorithms based on this approach as OBDD(∧,∃,reordering) algorithms. We prove the first exponential lower bound of OBDD(∧,∃,reordering) algorithms on unsatisfiable formulas, and give an example of formulas having short tree-like resolution proofs that are exponentially hard for OBDD(∧,∃,reordering) algorithms. We also present the first exponential lower bound for natural formulas with clear combinatorial meaning: every OBDD(∧,∃,reordering) algorithm runs exponentially long on the binary pigeonhole principle BPHPnn+1 © 2024 Elsevier B.V., All rights reserved.

AB - We study the symbolic approach to the propositional satisfiability problem proposed by Aguirre and Vardi in 2001 based on OBDDs and symbolic quantifier elimination. We study the theoretical limitations of the most general version of this approach where it is allowed to dynamically change variable order in OBDD. We refer to algorithms based on this approach as OBDD(∧,∃,reordering) algorithms. We prove the first exponential lower bound of OBDD(∧,∃,reordering) algorithms on unsatisfiable formulas, and give an example of formulas having short tree-like resolution proofs that are exponentially hard for OBDD(∧,∃,reordering) algorithms. We also present the first exponential lower bound for natural formulas with clear combinatorial meaning: every OBDD(∧,∃,reordering) algorithm runs exponentially long on the binary pigeonhole principle BPHPnn+1 © 2024 Elsevier B.V., All rights reserved.

KW - binary pigeonhole principle

KW - error-correcting codes

KW - lower bounds

KW - OBDD

KW - proof complexity

KW - Symbolic quantifier elimination

KW - tree-like resolution

KW - Boolean functions

KW - Consensus algorithm

KW - Binary pigeonhole principle

KW - Error correcting code

KW - Exponentials

KW - Low bound

KW - Pigeonhole principle

KW - Proof complexity

KW - Quantifier elimination

KW - Tree-like resolution

KW - Trees (mathematics)

U2 - 10.4230/LIPIcs.SAT.2024.19

DO - 10.4230/LIPIcs.SAT.2024.19

M3 - материалы

Y2 - 21 August 2024 through 24 August 2024

ER -

ID: 143425333