FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

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

0
0-1 integer linear decision problem	Certified CNF Translations for Pseudo-Boolean Solving
A
almost-sat	On the Parallel Parameterized Complexity of MaxSAT Variants
Anytime MaxSAT	Introducing Intel(R) SAT Solver
API	Incremental Maximum Satisfiability
assumptions	Incremental Maximum Satisfiability
Awards	Awards / Competition Results - I (with Live Broadcast) Awards and Competition - II (with Live Broadcast)
B
Backtracking	Introducing Intel(R) SAT Solver
BDD	(BDD event)
Best paper award
Best student paper award
bi-objective optimization	MaxSAT-Based Bi-Objective Boolean Optimization
Blake Canonical Form	A generalization of the Satisfiability Coding Lemma and its applications
Bryant	(BDD event)
C
CDCL	Quantified CDCL with Universal Resolution 25 years of SAT: Conflict-Driven SAT Solving 25 years of SAT: Modern SAT Techniques / Remembering Hans van Maaren
Certificates	Pedant: A Certifying DQBF Solver
CNF	25 years of SAT: Trusting SAT Solvers
CNF Encoding	Certified CNF Translations for Pseudo-Boolean Solving
CNF translation	Certified CNF Translations for Pseudo-Boolean Solving
Competitions	Awards / Competition Results - I (with Live Broadcast)
conflicts	25 years of SAT: Conflict-Driven SAT Solving
core extraction	Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
correction sets	Analysis of Core-Guided MaxSAT Using Cores and Correction Sets
Counting Proof Systems	Proofs for Propositional Model Counting
cutting planes	Certified CNF Translations for Pseudo-Boolean Solving
D
decision procedure	Quantifier Elimination in Stochastic Boolean Satisfiability Pedant: A Certifying DQBF Solver
deep generative models	On the performance of deep generative models of realistic SAT instances
deep learning	On the performance of deep generative models of realistic SAT instances
Design Automation	Towards a SAT Encoding for Quantum Circuits
DQBF	Pedant: A Certifying DQBF Solver
DQBF Solver	Pedant: A Certifying DQBF Solver
dynamic symmetry breaking	A SAT Attack on Rota's Basis Conjecture
E
Emaj-SAT	A New Exact Solver for (Weighted) Max#SAT
encoding	The packing chromatic number of the infinite square grid is at least 14
F
fixed-parameter tractability	On the Parallel Parameterized Complexity of MaxSAT Variants
G
graph isomorphism	SAT Preprocessors and Symmetry
H
heuristics	25 years of SAT: Modern SAT Techniques / Remembering Hans van Maaren
I
implicit hitting set approach	Incremental Maximum Satisfiability Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
incremental MaxSAT	Incremental Maximum Satisfiability
incremental SAT	MaxSAT-Based Bi-Objective Boolean Optimization
instantiation	Towards Learning Quantifier Instantiation in SMT
integer programming	A Comprehensive Study of k-Portfolios of Recent SAT Solvers
K
k-SAT	A generalization of the Satisfiability Coding Lemma and its applications
L
Leximax	SAT-based Leximax Optimisation Algorithms
Library of encodings	QBF Programming with the Modeling Language Bule
lower bounds	Should decisions in QCDCL follow prefix order? Classes of Hard Formulas for QBF Resolution
M
machine learning	Towards Learning Quantifier Instantiation in SMT A Comprehensive Study of k-Portfolios of Recent SAT Solvers
matroid	A SAT Attack on Rota's Basis Conjecture
Max#SAT	A New Exact Solver for (Weighted) Max#SAT
max-sat	On the Parallel Parameterized Complexity of MaxSAT Variants 25 years of SAT: Maximum Satisfiability for Real-World Optimization
maximum satisfiability	Analysis of Core-Guided MaxSAT Using Cores and Correction Sets Incremental Maximum Satisfiability MaxSAT-Based Bi-Objective Boolean Optimization
MaxSAT	Incremental Maximum Satisfiability Introducing Intel(R) SAT Solver
MC Competition	Awards and Competition - II (with Live Broadcast)
minimum hitting sets	Analysis of Core-Guided MaxSAT Using Cores and Correction Sets
model counting	Proofs for Propositional Model Counting
Modeling	QBF Programming with the Modeling Language Bule
Modelling	OptiLog v2: Model, Solve, Tune And Run
Multi-Objective Optimisation	SAT-based Leximax Optimisation Algorithms
Multi-objective optimization	MaxSAT-Based Bi-Objective Boolean Optimization
O
OBDD	Changing Partitions in Rectangle Decision Lists
OBDD-based proof systems	Tight Bounds for Tseitin Formulas
optimization	25 years of SAT: Maximum Satisfiability for Real-World Optimization
P
packing coloring	The packing chromatic number of the infinite square grid is at least 14
parallel algorithms	On the Parallel Parameterized Complexity of MaxSAT Variants
parameterized complexity	Weighted Model Counting with Twin-Width
pareto front enumeration	MaxSAT-Based Bi-Objective Boolean Optimization
presentations	Awards / Competition Results - I (with Live Broadcast)
Prime Implicants	A generalization of the Satisfiability Coding Lemma and its applications
proof checking	Migrating Solver State
proof complexity	QBF Merge Resolution is powerful but unnatural Should decisions in QCDCL follow prefix order? Relating existing powerful proof systems for QBF Tight Bounds for Tseitin Formulas Classes of Hard Formulas for QBF Resolution 25 years of SAT: Proof complexity and SAT solving
proof logging	Certified CNF Translations for Pseudo-Boolean Solving
Proofs	25 years of SAT: Trusting SAT Solvers 25 years of SAT: Proof complexity and SAT solving
Propositional satisfiability	A Comprehensive Study of k-Portfolios of Recent SAT Solvers
Pseudo-Boolean optimization	Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
pseudo-Boolean reasoning	Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
pseudo-Boolean solving	Certified CNF Translations for Pseudo-Boolean Solving
pseudo-industrial random SAT	On the performance of deep generative models of realistic SAT instances
Q
Q-resolution	Quantified CDCL with Universal Resolution
QBF	Quantified CDCL with Universal Resolution QBF Merge Resolution is powerful but unnatural Should decisions in QCDCL follow prefix order? Relating existing powerful proof systems for QBF Classes of Hard Formulas for QBF Resolution
QBF Competition	Awards and Competition - II (with Live Broadcast)
QBF Programming	QBF Programming with the Modeling Language Bule
QBF proof complexity	Changing Partitions in Rectangle Decision Lists
QCDCL	Should decisions in QCDCL follow prefix order?
QU-resolution	Quantified CDCL with Universal Resolution
quantifier elimination	Quantifier Elimination in Stochastic Boolean Satisfiability
quantifiers	Towards Learning Quantifier Instantiation in SMT
Quantum Computing	Towards a SAT Encoding for Quantum Circuits
R
Realistic SAT generators	On the performance of deep generative models of realistic SAT instances
rectangle decision lists	Changing Partitions in Rectangle Decision Lists
Reimplication	Introducing Intel(R) SAT Solver
resolution	QBF Merge Resolution is powerful but unnatural Should decisions in QCDCL follow prefix order? Tight Bounds for Tseitin Formulas Classes of Hard Formulas for QBF Resolution
restrictions	QBF Merge Resolution is powerful but unnatural
Rota's basis conjecture	A SAT Attack on Rota's Basis Conjecture
runtime prediction	A Comprehensive Study of k-Portfolios of Recent SAT Solvers
S
SAT	Weighted Model Counting with Twin-Width Introducing Intel(R) SAT Solver 25 years of SAT: Conflict-Driven SAT Solving 25 years of SAT: Maximum Satisfiability for Real-World Optimization 25 years of SAT: Trusting SAT Solvers 25 years of SAT: Proof complexity and SAT solving 25 years of SAT: Modern SAT Techniques / Remembering Hans van Maaren
SAT competition	Awards and Competition - II (with Live Broadcast)
SAT modulo Symmetry (SMS)	A SAT Attack on Rota's Basis Conjecture
SAT preprocessing	SAT Preprocessors and Symmetry
SAT solver	The packing chromatic number of the infinite square grid is at least 14
SAT solving	Towards a SAT Encoding for Quantum Circuits Migrating Solver State
Satisfiability	OptiLog v2: Model, Solve, Tune And Run
Satisfiability Coding Lemma	A generalization of the Satisfiability Coding Lemma and its applications
Sequent Calculus	Relating existing powerful proof systems for QBF
SMT	Towards Learning Quantifier Instantiation in SMT
solution reconstruction	Migrating Solver State
solution-improving search	Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
solver portfolios	A Comprehensive Study of k-Portfolios of Recent SAT Solvers
Solving	OptiLog v2: Model, Solve, Tune And Run
Sorting Networks	SAT-based Leximax Optimisation Algorithms
Special event	(BDD event)
SSAT	A New Exact Solver for (Weighted) Max#SAT
Stochastic Boolean Satisfiability	Quantifier Elimination in Stochastic Boolean Satisfiability
strategy extraction	Relating existing powerful proof systems for QBF
symmetry detection	SAT Preprocessors and Symmetry
T
Tool framework	OptiLog v2: Model, Solve, Tune And Run
Treewidth	Tight Bounds for Tseitin Formulas
Tseitin formulas	Tight Bounds for Tseitin Formulas
twin-width	Weighted Model Counting with Twin-Width
U
unsatisfiable cores	Analysis of Core-Guided MaxSAT Using Cores and Correction Sets
V
Verification	Proofs for Propositional Model Counting Relating existing powerful proof systems for QBF
W
weakening	QBF Merge Resolution is powerful but unnatural
Weighted Max#SAT	A New Exact Solver for (Weighted) Max#SAT
weighted model counting	Weighted Model Counting with Twin-Width
Weighted Projected Model Counting	A New Exact Solver for (Weighted) Max#SAT

Disclaimer | Powered by EasyChair Smart Program