FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

2
2-CNF	Minimal unsatisfiability and minimal strongly connected digraphs
A
Artificial Intelligence	QBF as an Alternative to Courcelle's Theorem
B
backdoor	ALIAS: A Modular Tool for Finding Backdoors for SAT
Backtracking	Chronological Backtracking
Betweenness Centrality	Centrality-Based Improvements to CDCL Heuristics
binarized neural network	Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Binary Analysis	Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
black-box optimization	ALIAS: A Modular Tool for Finding Backdoors for SAT
C
CAMUS	Finding all Minimal Safe Inductive Sets
Cardinality Constraint	Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
cardinality encodings	PySAT: A Python Toolkit for Prototyping with SAT Oracles
CDCL	Machine Learning-based Restart Policy for CDCL SAT Solvers Chronological Backtracking Centrality-Based Improvements to CDCL Heuristics
cdcl-cuttingplanes	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
Centrality	Centrality-Based Improvements to CDCL Heuristics
certificates	Polynomial-Time Validation of QCDCL Certificates
Chronological Backtracking	Chronological Backtracking
circuit	Circuit-based Search Space Pruning in QBF
Combinatorial benchmarks	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
Compilers	Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Complexity measures	Cops-Robber games and the resolution of Tseitin formulas
conflict-driven search	In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Core SAT	Chronological Backtracking
Counterexample-guided Algorithms	Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Crafted benchmarks	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
Curry-Howard correspondence	Local Soundness for QBF Calculi
cutting planes	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
D
Deficiency	Minimal unsatisfiability and minimal strongly connected digraphs
E
experimental analysis	Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
F
Filter	XORSAT Set Membership Filters
G
Games	Cops-Robber games and the resolution of Tseitin formulas
I
ic3	Finding all Minimal Safe Inductive Sets
Invariants	Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
IRM-calc	Local Soundness for QBF Calculi
Isomorphism type	Minimal unsatisfiability and minimal strongly connected digraphs
L
long-distance resolution	Local Soundness for QBF Calculi
M
Machine Learning	Machine Learning-based Restart Policy for CDCL SAT Solvers
MARCO	Finding all Minimal Safe Inductive Sets
MaxSAT	Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT Solving MaxSAT with Bit-Vector Optimization
MAXSAT application	Approximately Propagation Complete and Conflict Propagating Constraint Encodings
Minimal unsatisfiability	Minimal unsatisfiability and minimal strongly connected digraphs
Minimally strongly connected digraph	Minimal unsatisfiability and minimal strongly connected digraphs
Model Counting	Fast and Flexible Probabilistic Model Counting
model sampling	Fast Sampling of Perfectly Uniform Satisfying Assignments
Multi-Pass Dynamic Programming	Exploiting Treewidth for Projected Model Counting and its Limits
N
non-cnf	Circuit-based Search Space Pruning in QBF
nonlinear integer arithmetic	Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
novel applications domains	Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
O
Open-WBO	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
optimal propagation	Approximately Propagation Complete and Conflict Propagating Constraint Encodings
Optimization Modulo Bit-Vectors	Solving MaxSAT with Bit-Vector Optimization
P
Parameterized Algorithms	Exploiting Treewidth for Projected Model Counting and its Limits
parameterized complexity	QBF as an Alternative to Courcelle's Theorem
PDR	Finding all Minimal Safe Inductive Sets
perfect samplers	Fast Sampling of Perfectly Uniform Satisfying Assignments
power-law	Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
problem encodings and reformulations	Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Projected Model Counting	Exploiting Treewidth for Projected Model Counting and its Limits
proof complexity	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
propositional logic	Exploiting Treewidth for Projected Model Counting and its Limits
prototyping	PySAT: A Python Toolkit for Prototyping with SAT Oracles
Pseudo-Boolean Solving	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Python	PySAT: A Python Toolkit for Prototyping with SAT Oracles
Q
Q-resolution	Polynomial-Time Validation of QCDCL Certificates
QBF	QBF as an Alternative to Courcelle's Theorem Polynomial-Time Validation of QCDCL Certificates
QBF calculi	Local Soundness for QBF Calculi
quantified boolean formula	Circuit-based Search Space Pruning in QBF
Quantified Boolean Formulas	Symmetries for QBF
R
random parity equations	Fast and Flexible Probabilistic Model Counting
random SAT	Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
Randomized algorithms	Fast and Flexible Probabilistic Model Counting
resolution	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving Cops-Robber games and the resolution of Tseitin formulas
Restart	Machine Learning-based Restart Policy for CDCL SAT Solvers
S
SAT	ALIAS: A Modular Tool for Finding Backdoors for SAT Machine Learning-based Restart Policy for CDCL SAT Solvers Chronological Backtracking
SAT encoding	Approximately Propagation Complete and Conflict Propagating Constraint Encodings
SAT solver	Centrality-Based Improvements to CDCL Heuristics
SAT solvers	PySAT: A Python Toolkit for Prototyping with SAT Oracles
SAT solving	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
SAT-based Optimization	Solving MaxSAT with Bit-Vector Optimization
Sat4j	Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
satisfiability threshold	Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
semantics	Local Soundness for QBF Calculi
Separations	In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Set Membership	XORSAT Set Membership Filters
sharpness	Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
Singular DP-reduction	Minimal unsatisfiability and minimal strongly connected digraphs
Size	In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
SMT	Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Space	In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
strategies	Local Soundness for QBF Calculi
Symmetries	Symmetries for QBF
Symmetry breaking	Symmetries for QBF
T
toolkit	PySAT: A Python Toolkit for Prototyping with SAT Oracles
Totalizer	Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
Tree Decompositions	Exploiting Treewidth for Projected Model Counting and its Limits
treewidth	QBF as an Alternative to Courcelle's Theorem
Tseitin formulas	Cops-Robber games and the resolution of Tseitin formulas
U
unit propagation	Approximately Propagation Complete and Conflict Propagating Constraint Encodings
Unweighted Partial MaxSAT	Solving MaxSAT with Bit-Vector Optimization
V
validation	Polynomial-Time Validation of QCDCL Certificates
Verification	Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
W
Weighted MaxSAT	Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
witness generation	Fast Sampling of Perfectly Uniform Satisfying Assignments
X
XORSAT	XORSAT Set Membership Filters

Disclaimer | Powered by EasyChair Smart Program