Organizers: Ding-Zhu Du, Jun Gu, and Panos Pardalos
E-mails:    dzd@cs.umn.edu, gu@enel.ucalgary.ca, pardalos@ufl.edu
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"



TUESDAY, MARCH 12, 1996

 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,
             "Nesticity" 


WEDNESDAY, MARCH 13, 1996

 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