## John Franco

*Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing*

SAT-2002, 2002.

@proceedings{SAT-2002, address = "Cincinnati, Ohio, USA", editor = "John Franco", month = "may", pdfurl = "http://gauss.ececs.uc.edu/Conferences/SAT2002/program.html", title = "{Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing}", year = 2002, }

### Contents (46 items)

- SAT-2002-Schoening #bound #satisfiability
- New worst case bounds on k-SAT (US), p. 1.
- SAT-2002-CreignouD #problem #random #satisfiability
- Random generalized satisfiability problems (NC, HD), p. 2.
- SAT-2002-MatsuuraI
- Inclusion-exclusion for k-CNF formulas (AM, KI), p. 3.
- SAT-2002-SlaneyW #behaviour #optimisation
- Phase Transition Behavior: From Decision to Optimization (JS, TW), p. 4.
- SAT-2002-KaporisKL #algorithm #analysis #probability #satisfiability
- The Probabilistic Analysis of a Greedy Satisfiability Algorithm (ACK, LMK, EGL), p. 5.
- SAT-2002-FriezeW #named #satisfiability
- k-SAT: A tight threshold for moderately growing k (AF, NW), p. 6.
- SAT-2002-Szeider
- Generalizations of matched CNF formulas (SS), p. 7.
- SAT-2002-Kullmann #adaptation #branch #database #encryption #normalisation #random #satisfiability #standard #towards #using
- Towards an adaptive density based branching rule for SAT solvers, using a database for mixed random conjunctive normal forms built upon the Advanced Encryption Standard (AES) (OK), p. 8.
- SAT-2002-BueningX #complexity #morphism #satisfiability
- The complexity of homomorphisms and renamings of minimal unsatisfiable formulas (HKB, DX), p. 9.
- SAT-2002-PorschenRS #decidability #satisfiability
- X3SAT is decidable in time O(2n/5) (SP, BR, ES), p. 10.
- SAT-2002-MonassonC #algorithm #analysis #exponential #random #satisfiability #scalability
- Restart method and exponential acceleration of random 3-SAT instances resolutions: A large deviation analysis of the Davis-Putnam-Loveland-Logemann algorithm (RM, SC), p. 11.
- SAT-2002-Goldberg #satisfiability #testing
- Testing satisfiability of CNF formulas by computing a stable set of points (EG), p. 12.
- SAT-2002-BrglezLS #algorithm #benchmark #metric #satisfiability #testing
- The role of a skeptic agent in testing and benchmarking of SAT algorithms (FB, XYL, MFS), p. 13.
- SAT-2002-Marques-Silva #reasoning #satisfiability
- Hypothetical reasoning in propositional satisfiability (JMS), p. 14.
- SAT-2002-DuboisD #random #satisfiability
- Renormalization as a function of clause lengths for solving random k-SAT formulae (OD, GD), p. 15.
- SAT-2002-Gelder #reasoning #satisfiability #towards
- Toward leaner binary-clause reasoning in a satisfiability solver (AVG), p. 16.
- SAT-2002-RuessM #satisfiability
- Lemmas on demand for Satisfiability solvers (HR, LdM), p. 17.
- SAT-2002-LiJP #symmetry
- Integrating symmetry breaking into a DLL procedure (CML, BJ, PWP), p. 18.
- SAT-2002-GentP #encoding #problem #satisfiability
- SAT encodings of the stable marriage problem with ties and incomplete lists (IG, PP), p. 19.
- SAT-2002-LynceM #backtracking #data type #performance #satisfiability
- Efficient data structures for backtrack search SAT solvers (IL, JMS), p. 20.
- SAT-2002-Stachniak
- Going non-clausal (ZS), p. 21.
- SAT-2002-Bruni #satisfiability
- Exact selection of minimal unsatisfiable subformulae for special classes of propositional formulae (RB), p. 22.
- SAT-2002-AloulRMS #satisfiability #symmetry
- Solving difficult SAT instances in the presence of symmetry (FAA, AR, IM, KS), p. 23.
- SAT-2002-Roli #parallel #satisfiability
- Impact of structure on parallel local search for SAT (AR), p. 24.
- SAT-2002-AchlioptasM
- A bit of abstinence (provably) promotes satisfaction (DA, CM), p. 25.
- SAT-2002-Clarke #abstraction #logic #model checking #refinement #satisfiability
- SAT based abstraction refinement in temporal logic model checking (EC), p. 26.
- SAT-2002-MalerMNA #difference #logic #satisfiability
- A satisfiability checker for difference logic (OM, MM, PN, EA), p. 27.
- SAT-2002-AloulSS #backtracking
- A tool for measuring progress of backtrack-search solvers (FAA, BS, KS), p. 28.
- SAT-2002-LynceM1 #algorithm #backtracking #satisfiability #strict
- Complete unrestricted backtracking algorithms for satisfiability (IL, JMS), p. 29.
- SAT-2002-Pretolani #logic #modelling #probability
- Probabilistic logic: The PSAT and CPA models (DP), p. 30.
- SAT-2002-MotterM #on the #performance #proving #satisfiability
- On proof systems behind efficient SAT solvers (DM, IM), p. 31.
- SAT-2002-Kusper #linear #problem #satisfiability
- Solving the resolution-free SAT problem by hyper-unit propagation in linear time (GK), p. 32.
- SAT-2002-PrestwichB #approach #optimisation #query #satisfiability
- A SAT approach to query optimization in mediator systems (SP, SB), p. 33.
- SAT-2002-Bacchus #reasoning #trade-off
- Exploring the computational tradeoff of more reasoning and less searching (FB), p. 34.
- SAT-2002-LiB #empirical #satisfiability
- An empirical measure for characterizing 3-SAT (CML, HB), p. 35.
- SAT-2002-EglyWP #on the #problem
- On deciding subsumption problems (UE, SW, RP), p. 36.
- SAT-2002-AloulRMS1 #backtracking #named
- PBS: A backtrack-search psuedo-Boolean solver and optimizer (FAA, AR, IM, KS), p. 37.
- SAT-2002-HirschK #named #satisfiability
- UnitWalk: A new SAT solver that uses local search guided by unit clause elimination (EH, AK), p. 38.
- SAT-2002-Zhang #generative #satisfiability
- Generating college conference basketball schedules by a SAT solver (HZ), p. 39.
- SAT-2002-TakenakaH #algorithm #problem #satisfiability
- An analog algorithm for the satisfiability problem (YT, AH), p. 40.
- SAT-2002-Hoos #algorithm #modelling #satisfiability
- SLS algorithms for SAT: irregular instances, search stagnation, and mixture models (HH), p. 41.
- SAT-2002-ManyaABCL
- Resolution methods for many-valued CNF formulas (FM, CA, RB, AC, CML), p. 42.
- SAT-2002-ZhaoB #equivalence #problem
- Extension and equivalence problems for clause minimal formulas (XZ, HKB), p. 43.
- SAT-2002-DavydovaD #optimisation
- CNF application in discrete optimization (ID, GD), p. 44.
- SAT-2002-FormanS #named #parallel #random #satisfiability
- NAGSAT: A randomized, complete, parallel solver for 3-SAT (SF, AMS), p. 45.
- SAT-2002-DrakeFW #satisfiability
- Adding resolution to the DPLL procedure for satisfiability (LD, AF, TW), p. 46.

32 ×#satisfiability

6 ×#algorithm

6 ×#problem

5 ×#random

4 ×#backtracking

4 ×#named

3 ×#logic

3 ×#optimisation

3 ×#reasoning

2 ×#analysis

6 ×#algorithm

6 ×#problem

5 ×#random

4 ×#backtracking

4 ×#named

3 ×#logic

3 ×#optimisation

3 ×#reasoning

2 ×#analysis