SAT2024: INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING

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

#
#SAT	The Relative Strength of #SAT Proof Systems
(
(k s)-SAT	Small unsatisfiable k-CNFs with bounded literal occurrence
A
Algorithms	Logical Algorithmics: From Relational Queries to Boolean Reasoning
AllSAT	Entailing Generalization Boosts Enumeration
AllSAT-CT	Entailing Generalization Boosts Enumeration
alternating automata	Antichain with SAT and Tries
antichain	Antichain with SAT and Tries
B
Bandwidth Coloring Problem	SAT Encoding of Partial Ordering Models for Graph Coloring Problems
Benchmark Metadata	Global Benchmark Database
Benchmarking	Global Benchmark Database
Binary Decision Diagrams	Hierarchical Stochastic SAT and Quality Assessment of Logic Locking
binary pigeonhole principle	On Limits of Symbolic Approach to SAT Solving
blocked clause elimination	Dynamic Blocked Clause Elimination for Projected Model Counting
boolean satisfiability	satsuma: Structure-based Symmetry Breaking in SAT
Branch-and-bound	MaxSAT Resolution with Inclusion Redundancy
C
CDCL	Lazy Reimplication in Chronological Backtracking
Certification	Scalable Proof Production and Checking in SMT
Chronological Backtracking	Lazy Reimplication in Chronological Backtracking
Circuit Minimization	eSLIM: Circuit Minimization with SAT Based Local Improvement
Clause Learning	Parallel Clause Sharing Strategy based on Graph Structure of SAT Problem
Combinational Equivalence Checking	Clausal Congruence Closure
Congruence Closure	Clausal Congruence Closure
Conjunctive Normal Form	Clausal Congruence Closure
D
Data-driven Empirical Research	Global Benchmark Database
Decision Procedure	Hierarchical Stochastic SAT and Quality Assessment of Logic Locking
Decision-DNNF Circuits	On the Relative Efficiency of Dynamic and Static Top-Down Compilation to Decision-DNNF
Distributed algorithms	Scalable Trusted SAT Solving with on-the-fly LRAT Checking
Domain-wise Evaluation	Global Benchmark Database
dominance	The strength of the dominance rule
DRAT	The strength of the dominance rule
E
Enumeration	Entailing Generalization Boosts Enumeration
error-correcting codes	On Limits of Symbolic Approach to SAT Solving
Exact Synthesis	eSLIM: Circuit Minimization with SAT Based Local Improvement
Expansion	Strategy Extraction by Interpolation
Experimental Evaluation	Speeding-up Pseudo-Boolean Propagation
Explainable AI	Anytime Approximate Formal Feature Attribution
Extension variables	New lower bounds for Polynomial Calculus over non-Boolean bases
F
feature extraction	Revisiting SATZilla Features in 2024
Finite fields	New lower bounds for Polynomial Calculus over non-Boolean bases
Formal Feature Attribution	Anytime Approximate Formal Feature Attribution
Fourier basis	New lower bounds for Polynomial Calculus over non-Boolean bases
G
Generalization	Entailing Generalization Boosts Enumeration
Graph Coloring Problem	SAT Encoding of Partial Ordering Models for Graph Coloring Problems
Graph Theory	SAT Encoding of Partial Ordering Models for Graph Coloring Problems
H
Hall	Entailing Generalization Boosts Enumeration
Hardware Equivalence Checking	Clausal Congruence Closure
Hierarchical Stochastic SAT	Hierarchical Stochastic SAT and Quality Assessment of Logic Locking
HPC	Scalable Trusted SAT Solving with on-the-fly LRAT Checking
I
Implementation-level details	Speeding-up Pseudo-Boolean Propagation
Incremental solving	Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving
Instance Features	Global Benchmark Database
Integer Linear Programming	SAT Encoding of Partial Ordering Models for Graph Coloring Problems
Interpolation	Strategy Extraction by Interpolation
K
k-CNF	Small unsatisfiable k-CNFs with bounded literal occurrence
Knowledge Compilation	The Relative Strength of #SAT Proof Systems On the Relative Efficiency of Dynamic and Static Top-Down Compilation to Decision-DNNF
L
Layout Synthesis	Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
Lazy Reimplication	Lazy Reimplication in Chronological Backtracking
Local Search Method	Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme
Logic	Logical Algorithmics: From Relational Queries to Boolean Reasoning
Lower Bounds	The Relative Strength of #SAT Proof Systems
M
MaxSAT	MaxSAT Resolution with Inclusion Redundancy
MaxSAT resolution	MaxSAT Resolution with Inclusion Redundancy
Minimal Unsatisfiable Subsets	Anytime Approximate Formal Feature Attribution
minimally unsatisfiable formulas	Small unsatisfiable k-CNFs with bounded literal occurrence
Model Counting	The Relative Strength of #SAT Proof Systems
MUS Enumeration	Anytime Approximate Formal Feature Attribution
O
OBDD	On Limits of Symbolic Approach to SAT Solving
P
Parallel Plans	Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
Parallel solving	Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving
Parallel strategy	Parallel Clause Sharing Strategy based on Graph Structure of SAT Problem
Parity principle	MaxSAT Resolution with Inclusion Redundancy
Pigeonhole principle	MaxSAT Resolution with Inclusion Redundancy
Polynomial Calculus	New lower bounds for Polynomial Calculus over non-Boolean bases
Practical Applicability	Towards Universally Accessible SAT Technology
practical graph isomorphism	satsuma: Structure-based Symmetry Breaking in SAT
Prime implicants	Entailing Generalization Boosts Enumeration
projected model counting	Dynamic Blocked Clause Elimination for Projected Model Counting
Proof complexity	On Limits of Symbolic Approach to SAT Solving The Relative Strength of #SAT Proof Systems New lower bounds for Polynomial Calculus over non-Boolean bases
Proof generation	Scalable Proof Production and Checking in SMT
Proof Systems	The Relative Strength of #SAT Proof Systems
Proofs	Scalable Trusted SAT Solving with on-the-fly LRAT Checking
propositional logic	Dynamic Blocked Clause Elimination for Projected Model Counting
Propositional Satisfiability	Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
Prototyping	Towards Universally Accessible SAT Technology
Pseudo-Boolean Solving	Speeding-up Pseudo-Boolean Propagation
PySAT	Towards Universally Accessible SAT Technology
Python	Towards Universally Accessible SAT Technology
Q
QBF	Strategy Extraction by Interpolation eSLIM: Circuit Minimization with SAT Based Local Improvement
Quantified Boolean Formula	Models and Counter-Models of Quantified Boolean Formulas
Quantum Circuits	Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
Quantum compilation	Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving
Quantum computing	Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving
Qubit Mapping and Routing	Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
R
Redundancy	MaxSAT Resolution with Inclusion Redundancy
Relational queries	Logical Algorithmics: From Relational Queries to Boolean Reasoning
running time prediction	Revisiting SATZilla Features in 2024
S
SAT	Lazy Reimplication in Chronological Backtracking Antichain with SAT and Tries
SAT Encoding	SAT Encoding of Partial Ordering Models for Graph Coloring Problems
SAT Solvers	Parallel Clause Sharing Strategy based on Graph Structure of SAT Problem
SAT solving	Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving Scalable Trusted SAT Solving with on-the-fly LRAT Checking
SAT Sweeping	Clausal Congruence Closure
Satisfiability	Revisiting SATZilla Features in 2024
Satisfiability modulo theories	Scalable Proof Production and Checking in SMT
satisfiability prediction	Revisiting SATZilla Features in 2024
Satisfiability Solving	Clausal Congruence Closure
SLIM	eSLIM: Circuit Minimization with SAT Based Local Improvement
SMT solving	Cooking String-Integer Conversions with Noodles
Solution Counting	Models and Counter-Models of Quantified Boolean Formulas
Solution Extraction	Models and Counter-Models of Quantified Boolean Formulas
Stochastic Boolean Satisfiability	Hierarchical Stochastic SAT and Quality Assessment of Logic Locking
Strategy Extraction	Strategy Extraction by Interpolation
string conversions	Cooking String-Integer Conversions with Noodles
string solving	Cooking String-Integer Conversions with Noodles
Structural Hashing	Clausal Congruence Closure
Structure of SAT	Parallel Clause Sharing Strategy based on Graph Structure of SAT Problem
Symbolic quantifier elimination	On Limits of Symbolic Approach to SAT Solving
symmetry breaking	Small unsatisfiable k-CNFs with bounded literal occurrence The strength of the dominance rule
symmetry detection	satsuma: Structure-based Symmetry Breaking in SAT
symmetry exploitation	satsuma: Structure-based Symmetry Breaking in SAT
T
Top-down compilation	On the Relative Efficiency of Dynamic and Static Top-Down Compilation to Decision-DNNF
Transpiling	Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
tree-like resolution	On Limits of Symbolic Approach to SAT Solving
trie	Antichain with SAT and Tries
V
Variable selection heuristics	On the Relative Efficiency of Dynamic and Static Top-Down Compilation to Decision-DNNF
W
Weighted Partial MaxSAT	Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme
Weighting Scheme	Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme

Disclaimer | Powered by EasyChair Smart Program