SAT 2023: 26TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING

This page contains an index consisting of author-provided keywords.

#
#SAT	Proof Complexity of Propositional Model Counting
A
Acyclicity	A Comparison of SAT Encodings for Acyclicity of Directed Graphs
Algebraic methods	Polynomial Calculus for MaxSAT
AllSAT	On CNF Conversion for Disjoint SAT Enumeration AllSAT for Combinational Circuits
AllSMT	On CNF Conversion for Disjoint SAT Enumeration
automatability	Algorithmic Complexity of Certified Unsatisfiability
auxiliary variables	Effective Auxiliary Variables via Structured Reencoding
B
Backbone Extraction	CadiBack: Extracting Backbones with CaDiCaL
binary decision diagrams	Bounds on BDD-Based Bucket Elimination
boolean satisfiability	Algorithms Transcending the SAT-Symmetry Interface Effective Auxiliary Variables via Structured Reencoding
Bottom-up Compilation	Separating Incremental and Non-Incremental Bottom-Up Compilation
bounded variable addition	Effective Auxiliary Variables via Structured Reencoding
bucket elimination	Bounds on BDD-Based Bucket Elimination
C
CaDiCaL	Faster LRAT Checking than Solving with CaDiCaL
Causality	Explaining SAT Solving Using Causal Reasoning
CDCL	Limits of CDCL Learning via Merge Resolution QCDCL vs QBF Resolution: Further Insights Solving Huge Instances with Intel(R) SAT Solver
Certificates	Validation of QBF Encodings with Winning Strategies
checking	Faster LRAT Checking than Solving with CaDiCaL
Circuits	AllSAT for Combinational Circuits
Clause Assumption	CadiBack: Extracting Backbones with CaDiCaL
Clause management	Explaining SAT Solving Using Causal Reasoning
CNF conversion	On CNF Conversion for Disjoint SAT Enumeration
Combinational Circuits	AllSAT for Combinational Circuits
Combinatorial Optimization	Cutting Planes Width and the Complexity of Graph Isomorphism Refutations
complexity	Bounds on BDD-Based Bucket Elimination Around the Fine-Grained Complexity of SAT
computational group theory	Algorithms Transcending the SAT-Symmetry Interface
Core-guided	An Analysis of Core-guided Maximum Satisfiability Solvers Using Linear Programming
Cutting Planes	Cutting Planes Width and the Complexity of Graph Isomorphism Refutations
D
Dependency quantified boolean formulas (DQBF)	On the complexity of k-DQBF
Directed graphs	A Comparison of SAT Encodings for Acyclicity of Directed Graphs
DNNF	Separating Incremental and Non-Incremental Bottom-Up Compilation
dynamic symmetry breaking	SAT-Based Generation of Planar Graphs
E
Earth-Moon Problem	SAT-Based Generation of Planar Graphs
Emerson-Lei automata	Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
Equivalence	Validation of QBF Encodings with Winning Strategies
extended resolution	Effective Auxiliary Variables via Structured Reencoding
F
fine-grained complexity	Around the Fine-Grained Complexity of SAT
formal verification	Certified Knowledge Compilation with Application to Verified Model Counting
Formula partitioning	UpMax: User partitioning for MaxSAT
G
graph coloring	Effective Auxiliary Variables via Structured Reencoding
graph colorings	A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture
Graph Isomorphism	Cutting Planes Width and the Complexity of Graph Isomorphism Refutations
Graph-based methods	UpMax: User partitioning for MaxSAT
H
Hitting set problem	An Analysis of Core-guided Maximum Satisfiability Solvers Using Linear Programming
hypergraphs	A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture
I
Incremental SAT	IPASIR-UP: User Propagators for CDCL
Incremental Solving	CadiBack: Extracting Backbones with CaDiCaL
Inprocessing	CadiBack: Extracting Backbones with CaDiCaL
Intel(R) SAT Solver	Solving Huge Instances with Intel(R) SAT Solver
IntelSAT	Solving Huge Instances with Intel(R) SAT Solver
Interactive Game Play	Validation of QBF Encodings with Winning Strategies
Interference	Even shorter proofs without new variables
IPASIR	IPASIR-UP: User Propagators for CDCL
Ising Machine	Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT
K
knowledge compilation	Certified Knowledge Compilation with Application to Verified Model Counting Separating Incremental and Non-Incremental Bottom-Up Compilation
Kuratowski's Theorem	SAT-Based Generation of Planar Graphs
L
Leaf elimination	A Comparison of SAT Encodings for Acyclicity of Directed Graphs
learning scheme	Limits of CDCL Learning via Merge Resolution
Linear Programming	Cutting Planes Width and the Complexity of Graph Isomorphism Refutations An Analysis of Core-guided Maximum Satisfiability Solvers Using Linear Programming
Local Search	LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem
lower bounds	QCDCL vs QBF Resolution: Further Insights Proof Complexity of Propositional Model Counting
LRAT	Faster LRAT Checking than Solving with CaDiCaL
M
Maximum Satisfiability	UpMax: User partitioning for MaxSAT
MaxSAT	An Analysis of Core-guided Maximum Satisfiability Solvers Using Linear Programming Learning Shorter Redundant Clauses in SDCL Using MaxSAT Polynomial Calculus for MaxSAT LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem
merge resolution	Limits of CDCL Learning via Merge Resolution
Minimal Satisfiable Core	QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas
Minimal Unsatisfiable Core	QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas
model counting	Certified Knowledge Compilation with Application to Verified Model Counting Proof Complexity of Propositional Model Counting
Model Rotation	CadiBack: Extracting Backbones with CaDiCaL
N
Natural Computation	Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT
NEXP-complete	On the complexity of k-DQBF
O
OBDD	Separating Incremental and Non-Incremental Bottom-Up Compilation
omega-automata reduction	Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
P
planarity testing	SAT-Based Generation of Planar Graphs
Polynomial Calculus	Polynomial Calculus for MaxSAT
proof complexity	Cutting Planes Width and the Complexity of Graph Isomorphism Refutations Limits of CDCL Learning via Merge Resolution QCDCL vs QBF Resolution: Further Insights Proof Complexity of Propositional Model Counting
Proof systems	Even shorter proofs without new variables Polynomial Calculus for MaxSAT Proof Complexity of Propositional Model Counting
proofs of unsatisfiability	Algorithmic Complexity of Certified Unsatisfiability
PSPACE-complete	On the complexity of k-DQBF
Q
QBF	Validation of QBF Encodings with Winning Strategies QCDCL vs QBF Resolution: Further Insights
QBF solving	Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
Quantified Boolean Formulas	QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas
R
resolution	Limits of CDCL Learning via Merge Resolution QCDCL vs QBF Resolution: Further Insights Algorithmic Complexity of Certified Unsatisfiability
S
SAT	IPASIR-UP: User Propagators for CDCL Learning Shorter Redundant Clauses in SDCL Using MaxSAT On the complexity of k-DQBF AllSAT for Combinational Circuits
SAT encoding	A Comparison of SAT Encodings for Acyclicity of Directed Graphs
SAT modulo symmetries	A SAT Solver’s Opinion on the Erdős-Faber-Lovász Conjecture
SAT modulo Symmetry	IPASIR-UP: User Propagators for CDCL
SAT modulo Symmetry (SMS)	SAT-Based Generation of Planar Graphs
SAT modulo Theories	IPASIR-UP: User Propagators for CDCL
SAT solver	Explaining SAT Solving Using Causal Reasoning Solving Huge Instances with Intel(R) SAT Solver
SAT solving	Faster LRAT Checking than Solving with CaDiCaL
Satisfiability	Explaining SAT Solving Using Causal Reasoning Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT Bounds on BDD-Based Bucket Elimination Around the Fine-Grained Complexity of SAT
Schnyder orderings	SAT-Based Generation of Planar Graphs
SDCL	Learning Shorter Redundant Clauses in SDCL Using MaxSAT
simulations	QCDCL vs QBF Resolution: Further Insights
Stochastic Heuristics	Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT
Substitution redundancy	Even shorter proofs without new variables
Subsumption	Validation of QBF Encodings with Winning Strategies
succinct representation	On the complexity of k-DQBF
symmetry exploitation	Algorithms Transcending the SAT-Symmetry Interface
T
TELA	Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
telatko	Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
Top-k	LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem
Turan's Theorem	SAT-Based Generation of Planar Graphs
U
universal point sets	SAT-Based Generation of Planar Graphs
Unsatisfiable cores	Even shorter proofs without new variables
V
Validation	Validation of QBF Encodings with Winning Strategies
Vertex elimination	A Comparison of SAT Encodings for Acyclicity of Directed Graphs
W
Weisfeiler-Leman Algorithm	Cutting Planes Width and the Complexity of Graph Isomorphism Refutations
Winning Strategy	Validation of QBF Encodings with Winning Strategies

Disclaimer | Powered by EasyChair Smart Program