Polarity-based Stochastic Local Search Algorithms for Non-clausal Satisfiability

  • Zbigniew Stachniak
Part of the Studies in Fuzziness and Soft Computing book series (STUDFUZZ, volume 114)


This paper discusses the use of polarity to guide a stochastic local search for a satisfying assignment for a free-form formula of a finitely-valued propositional logic.


Local Search Classical Logic Local Search Algorithm Satisfying Assignment Satisfiability Problem 
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.
    Béjar, R.: Systematic and Local Search Algorithms for Regular-SAT. PhD thesis, Universitat Autènoma de Barcelona (2000)Google Scholar
  2. 2.
    Béjar, R. and Manyà, F.: Solving combinatorial problems with regular local search algorithms. Proc. 6th Int. Conf. on Logic for Programming and Automated Reasoning, LPAR-99, Springer LNAI 1705 (1999) 33–43CrossRefGoogle Scholar
  3. 3.
    Du, D., Gu, J. and Pardalos, P. editors: Satisfiability Problem: Theory and Applications. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, American Mathematical Society (1997)Google Scholar
  4. 4.
    Johnson, D., Aragon, C. and McGeoch, L.: Optimization by simulated annealing: an experimental evaluation; part ii, graph coloring and number partioning. Operations Research, 39 (1991) 378–406MATHCrossRefGoogle Scholar
  5. 5.
    Hähnle, R.: Complexity of Many-Valued Logics. Proc. of the 31st IEEE Int. Symp. on Multiple-Valued Logic (2001) 137–146Google Scholar
  6. 6.
    Manna, Z. and Waldinger, R.: The Deductive Foundations of Computer Programming. Eddison-Wesley (1993)Google Scholar
  7. 7.
    McAllester, D., Selman, B. and Kautz, H.: Evidence for invariants in local search. Proc. AAAI-97 (1997) 321–326Google Scholar
  8. 8.
    Mitchell, D., Selman, B. and Levesque, H.: Hard and Easy Distribution of SAT Problems. Proc. AAAI-92 (1992) 459–465Google Scholar
  9. 9.
    Mundici, D.: Satisfiability in Many-Valued Sentential Logics is NP-Complete. Theoretical Computer Science, 52 (1987) 145–153MathSciNetMATHCrossRefGoogle Scholar
  10. 10.
    Murray, N.: Completely Non-Clausal Theorem Proving. Artificial Intelligence, 18 (1982) 67–85MathSciNetMATHCrossRefGoogle Scholar
  11. 11.
    Plaisted, D. and Greenbaum, S.: A structure-preserving clause form translation. J. of Symbolic Computation, 2 (1986) 293–304MathSciNetMATHCrossRefGoogle Scholar
  12. 12.
    Schuurmans, D. and Southey, F.: Local search characteristics of incomplete SAT procedures. Proc. AAAI-2000 (2000) 297–302Google Scholar
  13. 13.
    Sebastiani, R.: Applying GSAT to non-clausal formulas. J. of Artificial Intelligence Research, 1 (1994) 309–314MATHGoogle Scholar
  14. 14.
    Selman, B., Levesque, H. and Mitchell, D.: A new method for solving hard satisfiability problems. Proc. AAAI-92 (1992) 440–446Google Scholar
  15. 15.
    Selman, B., Kautz, H. and Cohen, B.: Noise strategies for improving local search. Proc. AAAI-94 (1994) 337–343Google Scholar
  16. 16.
    Stachniak, Z.: Exploiting Polarity in Multiple-Valued Inference Systems. Proc. of the 31st IEEE Int. Symp. on Multiple-Valued Logic (2001) 149–156Google Scholar
  17. 17.
    Stachniak, Z.: Resolution Proof Systems: An Algebraic Theory. Kluwer (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Zbigniew Stachniak
    • 1
  1. 1.York UniversityTorontoCanada

Personalised recommendations