Capturing Structure with Satisfiability

  • Ramón Béjar
  • Alba Cabiscol
  • Cèsar Fernàndez
  • Felip Manyà
  • Carla Gomes
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2239)


We present Regular-SAT, an extension of Boolean Satisfiability basedon a class of many-valuedCNF formulas. Regular-SAT shares many properties with Boolean SAT, which allows us to generalize some of the best known SAT results and apply them to Regular-SAT. In addition, Regular-SAT has a number of advantages over Boolean SAT. Most importantly, it produces more compact encodings that capture problem structure more naturally. Furthermore, its simplicity allows us to develop Regular-SAT solvers that are competitive with SAT and CSP procedures. We present a detailed performance analysis of Regular-SAT on several benchmark domains. These results show a clear computational advantage of using a Regular-SAT approach over a pure Boolean SAT or CSP approach, at least on the domains under consideration. We therefore believe that an approach basedon Regular-SAT provides a compelling intermediate approach between SAT and CSPs, bringing together some of the best features of each paradigm.


Local Search Local Search Algorithm Interval Series Round Robin Schedule Phase Transition Boundary 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    D. Achlioptas, C. P. Gomes, H. Kautz, and B. Selman. Generating satisfiable problem instances. In Proc. of AAAI-2000, pages 256–261, 2000.Google Scholar
  2. 2.
    R. J. Bayardo and R. C. Schrag. Using CSP look-back techniques to solve realworldSA T instances. In Proc. of AAAI’97, pages 203–208, 1997.Google Scholar
  3. 3.
    B. Beckert, R. Hähnle and F. Manyà. The SAT problem of signedCNF formulas. In Labelled Deduction, pages 61–82, Kluwer, 2000.Google Scholar
  4. 4.
    R. Béjar. Systematic and Local Search Algorithms for Regular-SAT. PhD thesis, Universitat Autònoma de Barcelona, 2000.Google Scholar
  5. 5.
    R. Béjar and F. Manyà. Phase transitions in the regular random 3-SAT problem. In Proc. of ISMIS’99, pages 292–300. LNAI 1609, 1999.Google Scholar
  6. 6.
    R. Béjar and F. Manyà. A comparison of systematic andlo cal search algorithms for regular CNF formulas. In Proc. of ECSQARU’99, pages 22–31. LNAI 1638, 1999.Google Scholar
  7. 7.
    R. Béjar and F. Manyà. Solving combinatorial problems with regular local search algorithms. In Proc. of LPAR’99, pages 33–43. LNAI 1705, 1999.Google Scholar
  8. 8.
    J. C. Culberson and F. Luo. Exploring the k-colorable landscape with iterated greedy. In Cliques, Coloring and Satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. 1996.Google Scholar
  9. 9.
    M. Davis, G. Logemann, and D. Loveland. A machine program for theoremproving. Communications of the ACM, 5:394–397, 1962.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    A. M. Frisch and T. J. Peugniez. Solving non-Boolean satisfiability problems with stochastic local search. In Proc. of IJCAI’01, pages 282–288, 2001.Google Scholar
  11. 11.
    C. Gomes, H. Kautz, and Y. Ruan. QWH-A structuredb enchmark domain for local search. Technical Report, Intelligent Information Systems Institute (IISI), Cornell University, 2001.Google Scholar
  12. 12.
    C. Gomes, B. Selman, and N. Crato. Heavy-tailedd istributions in combinatorial search. In Proc. of CP’97, pages 121–135. Springer LNCS 1330, 1997.Google Scholar
  13. 13.
    C. P. Gomes and B. Selman. Problem structure in the presence of perturbations. In Proc. of AAAI’97, pages 221–226, 1997.Google Scholar
  14. 14.
    R. Hähnle. Short conjunctive normal forms in finitely-valuedlogics. Journal of Logic and Computation, 4(6):905–927, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    R. Hähnle. Exploiting data dependencies in many-valued logics. Journal of Applied Non-Classical Logics, 6:49–69, 1996.zbMATHMathSciNetGoogle Scholar
  16. 16.
    H. Hoos and T. Stützle. Local search algorithms for SAT: An empirical evaluation. Journal of Automated Reasoning, 24(4):421–481, 2000.zbMATHCrossRefGoogle Scholar
  17. 17.
    C. M. Li and Anbulagan. Look-aheadv ersus look-back for satisfiability problems. In Proc. of CP’97, pages 341–355. LNCS 1330, 1997.Google Scholar
  18. 18.
    F. Manyà. The 2-SAT problem in signedCNF formulas. Multiple-Valued Logic. An International Journal, 5(4):307–325, 2000.zbMATHMathSciNetGoogle Scholar
  19. 19.
    K. McAloon, C. Tretko., and G. Wetzel. Sports league scheduling. In Proc. of ILOG International Users Meeting, 1997.Google Scholar
  20. 20.
    R. Monasson, R. Zecchina, S. Kirkpatrick, B. Selman, and L. Troyansky. Determining computational complexity from characteristic ‘phase transitions’. Nature, 400(8), 1999.Google Scholar
  21. 21.
    J.-C. Régin. A filtering algorithm for constraints of difference in CSPs. In Proc. of AAAI’94, pages 362–367, 1994.Google Scholar
  22. 22.
    B. Selman, H. A. Kautz, and B. Cohen. Noise strategies for improving local search. In Proc. of AAAI’94, pages 337–343, 1994.Google Scholar
  23. 23.
    K. Stergiou and T. Walsh. The difference all-difference makes. In Proc. of IJCAI’ 99, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Ramón Béjar
    • 1
  • Alba Cabiscol
    • 2
  • Cèsar Fernàndez
    • 2
  • Felip Manyà
    • 2
  • Carla Gomes
    • 1
  1. 1.Dept. of Comp. ScienceCornell UniversityIthacaUSA
  2. 2.Dept. of Comp. ScienceUniversitat de LleidaLleidaSpain

Personalised recommendations