Loading teze.org 0 → 100644 +92 −0 Original line number Original line Diff line number Diff line * Preliminaries (2 strany) *** Propositional logic *** First-order logic * Propositional satisfiability (4 strany) - Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedur (Nieuwenhuis et al.) *** DP60 - A computing procedure for quantification theory (Davis, Putnam) *** DPLL - A machine program for theorem-proving (Davis at al.) *** CDCL - GRASP: A Search Algorithm for Propositional Satisfiability (Marques-Silva, Sakallah) ***** implication graph, UIP *** Note about lookeahead and cube-and-conquer - [[http://link.springer.com/chapter/10.1007/978-3-642-34188-5_8][Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads (Heule et al.)]] *** Effect of techniques used in CDCL - Empirical Study of the Anatomy of Modern Sat Solvers (Marques-Silva, Sakallah) - Chaff: Engineering an Efficient SAT Solver (Moskewicz et al.) ***** Branching heuristics - Evaluating CDCL Variable Scoring Schemes (Biere) - Learning Rate Based Branching Heuristic for SAT Solvers (Ganesh et al.) ***** Restarts - Evaluating CDCL Restart Schemes (Biere) - Optimal Speedup of Las Vegas Algorithms (Luby) * Satisfiability modulo theories (3 strany) *** DPLL(T) *** Natural domain SMT ***** mc-SAT - The Design and Implementation of the Model Constructing Satisfiability Calculus (Jovanovic) - A Model-Constructing Satisfiability Calculus (Jovanovic) ***** Abstract DPLL(T) - Abstract conflict driven learning (D'Silva et al.) - Abstract satisfaction (D'Silva et al.) - Deciding floating-point logic with abstract conflict driven clause learning (Kroening, Griggio) *** Theory combination - Nelson-Oppen - Being careful about theory combination (Jovanovic) - Sharing is Caring: Combination of Theories (Jovanovic) * Satisfiability of quantifier-free bit-vector formulas (4 strany) *** Definition of bit-vector theory *** Simplifications ***** unconstrained variables - Boolector: An efficient SMT solver for bit-vectors and arrays (Brummayer, Biere) - RTL Verification: From SAT to SMT(BV) (Bruttomesso) *** Core theory of bit-vectors - An efficient decision procedure for the theory of fixed-sized bit-vectors - A scalable decision procedure for fixed-width bit-vectors (Bruttomesso, Sharygina) *** Bit-blasting, eager and lazy - Decision Procedures: An Algorithmic Point of View (Kroening, Strichman) - A tale of two solvers: eager and lazy approaches to bit-vectors (Jovanovic, Hadarean) - Handling bit-propagating operations in bit-vector reasoning (Nadel) *** mcBV - Deciding Bit-Vector Formulas with mcSAT (Wintersteiger et al.) *** Stochastic local search - Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories (Biere) - Improving Local Search For Bit-Vector Logics in SMT with Path Propagation (Biere) - Stochastic Local Search for Satisfiability Modulo Theories (Biere) * Satisfiability of quantified bit-vector formulas (3 strany) - Boolector at the SMT competition 2016 (Biere, Niemetz, Preiner) *** MBQI - Efficiently Solving Quantified Bit-Vector Formulas (Wintersteiger et al.) *** CBQI (nastudovat) *** E-matching * Computational complexity (2 strany) *** SAT - The complexity of theorem-proving procedures (Cook) *** unary encoded QFBV and BV *** binary encoded QFBV and BV - On the complexity of fixed-size bit-vector logics with binary encoded bit-width (Kovázsnai et al.) - On the complexity of symbolic verification and decision problems in bit-vector logic (Kovázsnai et al.) - More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding (Fröhlich et al.) Loading
teze.org 0 → 100644 +92 −0 Original line number Original line Diff line number Diff line * Preliminaries (2 strany) *** Propositional logic *** First-order logic * Propositional satisfiability (4 strany) - Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedur (Nieuwenhuis et al.) *** DP60 - A computing procedure for quantification theory (Davis, Putnam) *** DPLL - A machine program for theorem-proving (Davis at al.) *** CDCL - GRASP: A Search Algorithm for Propositional Satisfiability (Marques-Silva, Sakallah) ***** implication graph, UIP *** Note about lookeahead and cube-and-conquer - [[http://link.springer.com/chapter/10.1007/978-3-642-34188-5_8][Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads (Heule et al.)]] *** Effect of techniques used in CDCL - Empirical Study of the Anatomy of Modern Sat Solvers (Marques-Silva, Sakallah) - Chaff: Engineering an Efficient SAT Solver (Moskewicz et al.) ***** Branching heuristics - Evaluating CDCL Variable Scoring Schemes (Biere) - Learning Rate Based Branching Heuristic for SAT Solvers (Ganesh et al.) ***** Restarts - Evaluating CDCL Restart Schemes (Biere) - Optimal Speedup of Las Vegas Algorithms (Luby) * Satisfiability modulo theories (3 strany) *** DPLL(T) *** Natural domain SMT ***** mc-SAT - The Design and Implementation of the Model Constructing Satisfiability Calculus (Jovanovic) - A Model-Constructing Satisfiability Calculus (Jovanovic) ***** Abstract DPLL(T) - Abstract conflict driven learning (D'Silva et al.) - Abstract satisfaction (D'Silva et al.) - Deciding floating-point logic with abstract conflict driven clause learning (Kroening, Griggio) *** Theory combination - Nelson-Oppen - Being careful about theory combination (Jovanovic) - Sharing is Caring: Combination of Theories (Jovanovic) * Satisfiability of quantifier-free bit-vector formulas (4 strany) *** Definition of bit-vector theory *** Simplifications ***** unconstrained variables - Boolector: An efficient SMT solver for bit-vectors and arrays (Brummayer, Biere) - RTL Verification: From SAT to SMT(BV) (Bruttomesso) *** Core theory of bit-vectors - An efficient decision procedure for the theory of fixed-sized bit-vectors - A scalable decision procedure for fixed-width bit-vectors (Bruttomesso, Sharygina) *** Bit-blasting, eager and lazy - Decision Procedures: An Algorithmic Point of View (Kroening, Strichman) - A tale of two solvers: eager and lazy approaches to bit-vectors (Jovanovic, Hadarean) - Handling bit-propagating operations in bit-vector reasoning (Nadel) *** mcBV - Deciding Bit-Vector Formulas with mcSAT (Wintersteiger et al.) *** Stochastic local search - Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories (Biere) - Improving Local Search For Bit-Vector Logics in SMT with Path Propagation (Biere) - Stochastic Local Search for Satisfiability Modulo Theories (Biere) * Satisfiability of quantified bit-vector formulas (3 strany) - Boolector at the SMT competition 2016 (Biere, Niemetz, Preiner) *** MBQI - Efficiently Solving Quantified Bit-Vector Formulas (Wintersteiger et al.) *** CBQI (nastudovat) *** E-matching * Computational complexity (2 strany) *** SAT - The complexity of theorem-proving procedures (Cook) *** unary encoded QFBV and BV *** binary encoded QFBV and BV - On the complexity of fixed-size bit-vector logics with binary encoded bit-width (Kovázsnai et al.) - On the complexity of symbolic verification and decision problems in bit-vector logic (Kovázsnai et al.) - More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding (Fröhlich et al.)
