. . . . . . . "The Boolean satisfiability problem (frequently abbreviated SAT) can be stated formally as:given a Boolean expression with variables, finding an assignment of the variables such that is true. It is seen as the canonical NP-complete problem. While no efficient algorithm is known to solve this problem in the general case, there are certain heuristics, informally called 'rules of thumb' in programming, that can usually help solve the problem reasonably efficiently."@en . . . . . . "The Boolean satisfiability problem (frequently abbreviated SAT) can be stated formally as:given a Boolean expression with variables, finding an assignment of the variables such that is true. It is seen as the canonical NP-complete problem. While no efficient algorithm is known to solve this problem in the general case, there are certain heuristics, informally called 'rules of thumb' in programming, that can usually help solve the problem reasonably efficiently. Although no known algorithm is known to solve SAT in polynomial time, there are classes of SAT problems which do have efficient algorithms that solve them. These classes of problems arise from many practical problems in AI planning, circuit testing, and software verification. Research on constructing efficient SAT solvers has been based on various principles such as resolution, search, local search and random walk, binary decisions, and Stalmarck's algorithm. Some of these algorithms are deterministic, while others may be stochastic. As there exist polynomial-time algorithms to convert any Boolean expression to conjunctive normal form such as Tseitin's algorithm, posing SAT problems in CNF does not change their computational difficulty. SAT problems are canonically expressed in CNF because CNF has certain properties that can help prune the search space and speed up the search process."@en . . . . . "13904"^^ . . . "48777793"^^ . . . . . . . . "1115292947"^^ . . . . . . . . . "Boolean satisfiability algorithm heuristics"@en . . . . . .