A stochastic non-CNF SAT solver

Rafiq Muhammad, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

7 Citations (Scopus)


Stochastic local search techniques have been successful in solving propositional satisfiability (SAT) problems encoded in conjunctive normal form (CNF). Recently complete solvers have shown that there are advantages to tackling propositional satisfiability problems in a more expressive natural representation, since the conversion to CNF can lose problem structure and introduce significantly more variables to encode the problem. In this work we develop a non-CNF SAT solver based on stochastic local search techniques. Crucially the system must be able to represent how true a proposition is and how false it is, as opposed to the usual stochastic methods which represent simply truth or degree of falsity (penalty). Our preliminary experiments show that on certain benchmarks the non-CNF local search solver can outperform highly optimized CNF local search solvers as well as existing CNF and non-CNF complete solvers.

Original languageEnglish
Title of host publicationPRICAI 2006
Subtitle of host publicationTrends in Artificial Intelligence - 9th Pacific Rim International Conference on Artificial Intelligence, Proceedings
Number of pages10
ISBN (Print)3540366679, 9783540366676
Publication statusPublished - 1 Jan 2006
Externally publishedYes
Event9th Pacific Rim International Conference on Artificial Intelligence - Guilin, China
Duration: 7 Aug 200611 Aug 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4099 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference9th Pacific Rim International Conference on Artificial Intelligence

Cite this