March 11-13, 1996
DIMACS (Center for Discrete Mathematics and
Theoretical Computer Sciences), Rutgers University

Organizers: Ding-Zhu Du, Jun Gu, and Panos Pardalos
Advisory Committee:
            Bob Johnson, David Johnson, Christos Papadimitriou,
            Paul Purdom, Benjamin Wah

MONDAY, MARCH 11, 1996

08:50-09:00 Welcome from the DIMACS Director and the Organizers

09:00-09:05 Distinguished Speaker introduced by Ding-Zhu Du 

09:05-10:00 Distinguished Lecture 
             Stephen A. Cook, 
             "Finding Hard Instances of the Satisfiability Problem"

10:00-10:15 Break

 Session M.A  Chairman: Panos Pardalos

10:15-11:00 Jun Gu, Paul Purdom, John Franco, and Benjamin Wah, 
             "Algorithms for Satisfiability (SAT) Problem: A Survey"

11:00-11:30 Paul W. Purdom,
             "Selecting the Shortest Clause"

11:30-12:00 John Franco, John Schlipf, Ewald Speckenmeyer, and R. Swaminathan,
             "A O(2^m|F|) Algorithm for Determining the Falsifiability
              of Implication Formulas with m Occurrences of the Head Atom"

12:00-01:30 LUNCH

 Session M.B  Chairman: Jun Gu

01:30-02:00 Randy Bryant, 
             "Binary Decision Diagrams Applied to SAT and Related Problems"

02:00-02:30 Benjamin W. Wah, Alan Y.-J. Chang, and Yi Shang,
             "Lagrangian Methods for Satisfiability Problems"

02:30-03:00 A. Kamath, N. Karmarkar, K.G. Ramakrishnan, M.G.C. Resende,
             "Interior Point Algorithm for Approximate Solution of Maximum 
              Satisfiability Problem" 

03:00-03:30 Break 

 Session M.C  Chairman: Ding-Zhu Du

03:30-04:00 C.-J. Richard Shi,
             "Inclusive-OR Boolean Satisfiability for Via Minimization
              and Constrained Encoding in VLSI Design"

04:00-04:30 Craig K. Rushforth and Wei Wang, 
             "Local Search Algorithms for Channel Assignment 
              in Cellular Communication Networks" 

04:30-05:00 S.K. Shukla, Daniel Rosenkrantz, Harry Hunt III, and R.E. Stearns,
             "A HORNSAT Based Approach to the Polynomial Time Decidability
              of Simulation Relations for Finite State Processes"


 Session T.A  Chairman: Panos Pardalos

08:45-09:15 Henri Morel,
             "Some Results Concerning Minimally Unsatisfiable Conjunctive 
              Normal Forms"

09:15-09:45 Kazuo Iwama,
             "Proving Unsatisfiability of CNF Formulas using Partial Clauses"

09:45-10:15 Endre Boros,
             "If Simplifying Does Not Work, Try Complicating It"

10:15-10:30 Break 

 Session T.B  Chairman: Jun Gu

10:30-11:00 David A. Plaisted and Geoffrey Alexander, 
             "Propositional Search Spaces and First-Order Theorem Proving"

11:00-11:30 Allen Van Gelder,
             "Modoc: An Algorithm for Simultaneous Construction of 
              Refutations and Models"

11:30-12:00 Oliver Kullmann,
             "A Systematic Approach to 3-SAT-decision, Yielding
              3-SAT-Decision in Less Than 1.5045^n Steps"

12:00-01:30 LUNCH

 Session T.C  Chairman: Ding-Zhu Du

01:30-02:00 Yuejun Jiang, Henry Kautz, and Bart Selman,
             "Solving Problems with Hard and Soft Constraints
              Using a Stochastic Algorithm for MAX-SAT"

02:00-02:30 Ding-Zhu Du, Jun Gu, and Panos M. Pardalos, 
             "Local Search for Satisfiability (SAT) Problem: 
              Performance and Applications"

02:30-03:00 Arne Lokketangen and Fred Glover,
             "Surrogate Constraint Analysis and Probabilistic 
              Tabu Search for Satisfiability Problems" 

03:00-03:30 Break 

 Session T.D  Chairman: Jun Gu

03:30-04:00 Leonidas S. Pitsoulis and Mauricio G.C. Resende, 
             "A Parallel GRASP for SAT"

04:00-04:30 Ewald Speckenmeyer and Max B\"ohm,
             "Fast Satisfiability Solving"

04:30-05:00 Pierre Hansen, Dominique de Werra, and Michael Gerber,


 Session W.A  Chairman: Panos Pardalos

08:45-09:15 Jinchang Wang, 
             "A Branching Heuristic for Propositional Satisfiability Test"

09:15-09:45 Brigitte Jaumard and Mihnea Stan,
             "Decomposition vs Relaxation Methods to Solve 
              the Satisfiability Problem"

09:45-10:15 Allen Van Gelder and Yumi K. Tsuji,
             "Variable Elimination by Resolution Improves Model Search 
              for Satisfiability"

10:15-10:30 Break 

 Session W.B  Chairman: Jun Gu

10:30-11:00 Jieh Hsiang and Kuan-hsuen Huang,
             "On Boolean Ring Normal Form of Boolean Functions with
              Don't-Care Conditions"

11:00-11:30 M.V. Marathe, Harry Hunt III, R.E. Stearns, and V. Radhakrishnan,
             "Complexity of Hierarchically and 1-Dimensional Periodically 
              Specified Problems"
11:30-12:00 Roger Y. Gouin and Philip C. Jackson, Jr.,
             "Many-Worlds Quantum Computation of Satisfiability Problems"

12:00-01:30 LUNCH

 Session W.C  Chairman: Ding-Zhu Du

01:30-02:00 Shawki Areibi and Anthony Vannelli,
             "An Efficient Branch and Bound Technique for Circuit Partitioning"

02:00-02:30 Bin Du, 
             "Sequential Circuit Test Generation based on SAT Model" 
02:30-03:00 Jun Gu, Ruchir Puri, and Peter Vanbekbergen, 
             "A SAT Approach for Asynchronous Circuit Design"

03:00-03:30 F. Friedler, B. Imreh, and L.T. Fan,
             "Satisfiability for the Structural Model of Process
              Network Synthesis"  

03:30-04:00 Break 

 Session W.D  Chairman: Panos Pardalos

04:00-04:30 Roberto Battiti and Marco Protasi,
             "Solving MAX-SAT with History-Based Heuristics"

04:30-05:00 Vladimir Gurvich and Leonid Khachiyan,
             "On Generating the Irredundant Conjunctive and Disjunctive 
              Normal Forms of Monotone Boolean Functions"

05:00-05:30 Hans Maaren,
             "On the Use of Second Order Derivatives for the SAT Problem"

 Session W.E  Chairman: Jun Gu

05:30-06:00 O. Dubois and Y. Boufkhad,
             "What Influences Strongly the Satisfiability and the Hardness of SAT Instances"

06:00-06:30 Lefteris M. Kirousis, Evangelos Kranakis, and Danny Krizanc,
             "Approximating the Unsatisfiability Threshold Point of 
              Random Formulas"

06:30-07:00 John Mitchell, Steve Joy, and Brian Borchers,
             "Solving Weighted Max Sat Problems Using Branch and Cut"

Previous: Participation
Next: Registration
Workshop Index
DIMACS Homepage
Contacting the Center
Document last modified on February 26, 1996