FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

Disclaimer | Powered by EasyChair Smart Program