SAT 2004: Accepted Papers

A Comparative Study of 2QBF Algorithms (Poster / Short Paper)   Darsh P. Ranjan, Daijue Tang, Sharad Malik

A Note on Satisfying Truth-Value Assignments of Boolean Formulas   Zbigniew Stachniak

A Random Constraint Satisfaction Problem That Seems Hard for DPLL   Harold Connamacher

A SAT Based Scheduler for Fair Tournament Schedules   Hantao Zhang, Dapeng Li, and Haiou Shen

A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints   Alessandro Armando and Claudio Castellini and Enrico Giunchiglia and Marco Maratea

Adding a New Conflict Based Branching Heuristic in two Evolved DPLL SAT Solvers (Poster / Short Paper)   Renato Bruni, Andrea Santori

Algorithms for Satisfiability using Independent Sets of Variables   Ravi Gummadi, N.S. Narayanaswamy, Venkatakrishnan Ramaswamy

Aligning CNF- and Equivalence-Reasoning   Marijn Heule and Hans van Maaren

An algebraic approach to the complexity of generalized conjunctive queries   Michael Bauland, Philippe Chapdelaine, Nadia Creignou, Miki Hermann, Heribert Vollmer

Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems   Daijue Tang, Yinlei Yu, Darsh P. Ranjan, Sharad Malik

Approximation algorithm for random MAX-KSAT   Yannet Interian

Automatic extraction of functional dependencies   Éric Grégoire, Richard Ostrowski, Bertrand Mazure and Lakhdar Saïs

Boolean Ring Satisfiability (Poster / Short Paper)   Nachum Dershowitz, Jieh Hsiang, Guan-Shieng Huang, and Daher Kaiss

CirCUs : Hybrid Satifiability solver   HoonSang Jin, Fabio Somenzi

Combining Component Caching and Clause Learning for Effective Model Counting   Tian Sang, Fahiem Bacchus, Paul Beame, Henry Kautz, Toniann Pitassi

Computing Unsatisfiable k-SAT Instances with Few Occurrences per Variable   Shlomoh Hoory, Stefan Szeider

Computing Unsatisfiable k-SAT Instances with Few Occurrences per Variable   Shlomoh Hoory, Stefan Szeider

Dealing with symmetries in Quantified Boolean Formulas (Poster / Short Paper)   Gilles Audemard, Bertrand Mazure and Lakhdar Saïs

Derandomization of Schuler’s Algorithm for SAT   Evgeny Dantsin and Alexander Wolpert

Detecting Backdoor Sets with Respect to Horn and Binary Clauses   Naomi Nishimura, Prabhakar Ragde, and Stefan Szeider

EARLY CONFLICT DETECTION BASED BCP FOR SAT SOLVING   Matthew D. T. Lewis, Tobias Schubert, Bernd W. Becker

Efficient Implementations of SAT Local Search (Poster / Short Paper)   Alex Fukunaga

Encoding Global Unobservability for Efficient Translation to SAT   Miroslav N. Velev

Engineering an Efficient Max-SAT Solver (Poster / Short Paper)   Xiao Yu Li and Matthias F. Stallmann and Franc Brglez

Equivalence Models for Quantified Boolean Formulas   Hans Kleine Buening, Xishun Zhao

From spin glasses to hard satisfiable formulas   Haixia Jia, Cris Moore and Bart Selman

Game-SAT: A Preliminary Report (Poster / Short Paper)   Ling Zhao and Martin Mueller

Improving First-order Model Searching by Propositional Reasoning and Lemma Learning (Poster / Short Paper)   Zhuo Huang, Hantao Zhang and Jian Zhang

Incremental Compilation-to-SAT procedures   Marco Benedetti and Sara Bernardini

Local Search for Very Large SAT Problems (Poster / Short Paper)   Steven Prestwich and Colin Quirke

Local search with bootstrapping (Poster / Short Paper)   Lengning Liu and Miroslaw Truszczynski

Looking Algebraically at Tractable Quantified Boolean Formulas   Hubie Chen and Victor Dalmau

Mapping problems with finite-domain variables into problems with Boolean variables   Carlos Ansotegui and Felip Manya

NiVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT instances (Poster / Short Paper)   Sathiamoorthy Subbarayan and Dhiraj K Pradhan

On Computing Minimum Unsatisfiable Cores (Poster / Short Paper)   Inês Lynce and João P. Marques-Silva

Polynomial time SAT decision, hypergraph transversals and the Hermitian rank   Nicola Galesi and Oliver Kullmann

Problem encoding into SAT : the counting constraints case (Poster / Short Paper)   Olivier Bailleux and Yacine Boufkhad

QBF reasoning on real-world instances   Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella

Resolve and Expand   Armin Biere

Satisfiability Threshold of the Skewed Random k-SAT (Poster / Short Paper)   Danila A. Sinopalnikov

Search vs. Symbolic Techniques in Satisfiability Solving   Guoqiang Pan, Moshe Y. Vardi

Solving Non-Clausal Formulas with DPLL search   Christian Thiffault, Fahiem Bacchus, Toby Walsh

The Optimality of a Fast CNF Conversion and its use with SAT (Poster / Short Paper)   Daniel Sheridan

UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT   Dave A. D. Tompkins and Holger H. Hoos

Using DPLL for Efficient OBDD Construction   Jinbo Huang and Adnan Darwiche

Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization   Vasco M. Manquinho, João Marques-Silva

Using Rewarding Mechanisms for Improving Branching Heuristics (Poster / Short Paper)   Elsa Carvalho & João Marques-Silva

Verifying the On-Line Help System of SIEMENS Magnetic Resonance Tomographs using SAT (Poster / Short Paper)   Carsten Sinz and Wolfgang Küchlin

Visualizing the Internal Structure of SAT Instances (Preliminary Report) (Poster / Short Paper)   Carsten Sinz

Worst case bounds for some NP-complete modified Horn-SAT problems (Poster / Short Paper)   Stefan Porschen, Ewald Speckenmeyer