Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Publisher: Springer-Verlag
Languages: English
Types: Part of book or chapter of book
Subjects: QA76

Classified by OpenAIRE into

A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solver is surprisingly powerful and its elegant use of Prolog constructs is presented as a programming pearl.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 1. M. Bruynooghe. Enhancing a Search Algorithm to Perform Intelligent Backtracking. Theory and Practice of Logic Programming, 4(3):371-380, 2004.
    • 2. M. Codish, V. Lagoon, and P. J. Stuckey. Logic Programming with Satisfiability. Theory and Practice of Logic Programming, 8(1):121-128, 2008.
    • 3. M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem Proving. Communications of the ACM, 5(7):394-397, 1962.
    • 4. N. E´en and A. Biere. Effective Preprocessing in SAT through Variable and Clause Elimination. In International Conference on Theory and Applications of Satisfiability Testing, volume 3569 of Lecture Notes in Computer Science, pages 61-75, 2005.
    • 5. N. E´en and N. S¨orensson. An Extensible SAT-solver. In Theory and Applications of Satisfiability Testing, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003.
    • 6. I. P. Gent, C. Jefferson, and I. Miguel. Watched Literals for Constraint Propagation in Minion. In Constraint Programming, volume 4204 of Lecture Notes in Computer Science, pages 182-197. Springer, 2006.
    • 7. H. H. Hoos and T. Stu¨tzle. SATLIB: An Online Resource for Research on SAT. In SAT 2000, pages 283-292. IOS Press, 2000. http://www.satlib.org.
    • 8. J. M. Howe and A. King. Positive Boolean Functions as Multiheaded Clauses. In International Conference on Logic Programming, volume 2237 of Lecture Notes in Computer Science, pages 120-134. Springer, 2001.
    • 9. J. M. Howe and A. King. Efficient Groundness Analysis in Prolog. Theory and Practice of Logic Programming, 3(1):95-124, 2003.
    • 10. A. King and J. C. Martin. Control Generation by Program Transformation. Fundamenta Informaticae, 69(1-2):179-218, 2006.
    • 11. R. A. Kowalski. Algorithm = Logic + Control. Communication of the ACM, 22(7):424-436, 1979.
    • 12. D. Le Berre, O. Roussel, and L. Simon. The International SAT Competitions Webpage, 2009. http://www.satcompetition.org/.
    • 13. J. P. Marques-Silva and K. A. Sakallah. GRASP - a New Search Algorithm for Satisfiability. In International Conference on Computer-Aided Design, pages 220- 227. ACM and IEEE Computer Society, 1996.
    • 14. M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In Design Automation Conference, pages 530-535. ACM Press, 2001.
    • 15. L. Naish. Negation and Control in Logic Programs. Springer-Verlag, 1986.
    • 16. L. Zhang and S. Malik. The Quest for Efficient Boolean Satisfiability Solvers. In Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 17-36. Springer, 2002.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article