7. SAT 2004: Vancouver, BC, Canada

Hard instances

• Harold S. Connamacher:
  A Random Constraint Satisfaction Problem That Seems Hard for DPLL.
  
• Haixia Jia, Cristopher Moore, Bart Selman:
  From Spin Glasses to Hard Satisfiable Formulas.
  

SAT Solvers

• Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, Toniann Pitassi:
  Combining Component Caching and Clause Learning for Effective Model Counting.
  
• Matthew D. T. Lewis, Tobias Schubert, Bernd Becker:
  Early Conflict Detection Based BCP for SAT Solving.
  
• Dave A. D. Tompkins, Holger H. Hoos:
  UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT & MAX-SAT.
  
• HoonSang Jin, Fabio Somenzi:
  CirCUs: A Hybrid Satisfiability Solver.
  

Algorithms & Bounds I

• Shlomo Hoory, Stefan Szeider:
  Computing Unsatisfiable k-SAT Instances with Few Occurrences per Variable.
  
• Ravi Gummadi, N. S. Narayanaswamy, Venkatakrishnan Ramaswamy:
  Algorithms for Satisfiability using Independent Sets of Variables.
  

SAT Solvers Competition & QBF Solvers Evaluation

Algorithms & Bounds II

• Evgeny Dantsin, Alexander Wolpert:
  Derandomization of Schuler's Algorithm for SAT.
  
• Nicola Galesi, Oliver Kullmann:
  Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank.
  
• Yannet Interian:
  Approximation Algorithm for Random MAX-kSAT.
  

Properties of Formulae / Non-Boolean Problems

• Naomi Nishimura, Prabhakar Ragde, Stefan Szeider:
  Detecting Backdoor Sets with Respect to Horn and Binary Clauses.
  
• Zbigniew Stachniak:
  A Note on Satisfying Truth-Value Assignments of Boolean Formulas.
  
• Carlos Ansótegui, Felip Manyà:
  Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables.
  
• Vasco M. Manquinho, João P. Marques Silva:
  Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization.
  

Poster Overview Session I

• Stefan Porschen, Ewald Speckenmeyer:
  Worst Case Bounds for some NP-Complete Modified Horn-SAT Problems.
  
• Danila A. Sinopalnikov:
  Satisfiability Threshold of the Skewed Random k-SAT.
  
• Steven David Prestwich, Colin Quirke:
  Local Search for Very Large SAT Problems.
  
• Lengning Liu, Miroslaw Truszczynski:
  Local Search with Bootstrapping.
  
• Alex S. Fukunaga:
  Efficient Implementations of SAT Local Search.
  
• Renato Bruni, Andrea Santori:
  Adding a New Conflict Based Branching Heuristic in two Evolved DPLL SAT Solvers.
  
• Elsa Carvalho, João P. Marques Silva:
  Using Rewarding Mechanisms for Improving Branching Heuristics.
  
• Inês Lynce, João P. Marques Silva:
  On Computing Minimum Unsatisfiable Cores.
  
• Carsten Sinz:
  Visualizing the Internal Structure of SAT Instances (Preliminary Report).
  

Non-CNF SAT I

• Jinbo Huang, Adnan Darwiche:
  Using DPLL for Efficient OBDD Construction.
  
• Guoqiang Pan, Moshe Y. Vardi:
  Search vs. Symbolic Techniques in Satisfiability Solving.
  
• Christian Thiffault, Fahiem Bacchus, Toby Walsh:
  Solving Non-clausal Formulas with DPLL search.
  
• Éric Grégoire, Richard Ostrowski, Bertrand Mazure, Lakhdar Sais:
  Automatic Extraction of Functional Dependencies.
  

Non-CNF SAT II

• Alessandro Armando, Claudio Castellini, Enrico Giunchiglia, Marco Maratea:
  A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints.
  
• Marijn Heule, Hans van Maaren:
  Aligning CNF- and Equivalence-reasoning.
  
• Michael Bauland, Philippe Chapdelaine, Nadia Creignou, Miki Hermann, Heribert Vollmer:
  An Algebraic Approach to the Complexity of Generalized Conjunctive Queries.
  
• Hantao Zhang, Dapeng Li, Haiou Shen:
  A SAT Based Scheduler for Tournament Schedules.
  

Bounded Model Checking

• Marco Benedetti, Sara Bernardini:
  Incremental Compilation-to-SAT Procedures.
  
• Daijue Tang, Yinlei Yu, Darsh Ranjan, Sharad Malik:
  Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems.
  

QBF

• Hubie Chen, Víctor Dalmau:
  Looking Algebraically at Tractable Quantified Boolean Formulas.
  
• Hans Kleine Büning, Xishun Zhao:
  Equivalence Models for Quantified Boolean Formulas.
  
• Miroslav N. Velev:
  Encoding Global Unobservability for Efficient Translation to SAT.
  
• Armin Biere:
  Resolve and Expand.
  
• Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella:
  QBF Reasoning on Real-World Instances.
  

Poster Overview Session II

• Darsh P. Ranjan, Daijue Tang, Sharad Malik:
  A Comparative Study of 2QBF Algorithms.
  
• Gilles Audemard, Bertrand Mazure, Lakhdar Sais:
  Dealing with Symmetries in Quantified Boolean Formulas.
  
• Zhuo Huang, Hantao Zhang, Jian Zhang:
  Improving First-order Model Searching by Propositional Reasoning and Lemma Learning.
  
• Nachum Dershowitz, Jieh Hsiang, Guan-Shieng Huang, Daher Kaiss:
  Boolean Ring Satisfiability.
  
• Ling Zhao, Martin Müller:
  Game-SAT: A Preliminary Report.
  
• Carsten Sinz, Wolfgang Küchlin:
  Verifying the On-Line Help System of SIEMENS Magnetic Resonance Tomographs using SAT (Extended Abstract).
  
• Sathiamoorthy Subbarayan, Dhiraj K. Pradhan:
  NiVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT instances.
  
• Daniel Sheridan:
  The Optimality of a Fast CNF Conversion and its Use with SAT.
  
• Olivier Bailleux, Yacine Boufkhad:
  Full CNF Encoding: The Counting Constraints Case.
  

Last update Fri May 25 08:35:22 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page