npycomp.problems.

ThreeSAT#

class npycomp.problems.ThreeSAT(clauses: list)#

A SAT Problem with at most three literals per clause.

3-SAT is a special case of the SAT problem where each clause has at most three literals. Like the SAT, The 3-SAT probleom asks whether there exists an assignment of variables that satisfies a given Boolean formula.

Formally, a 3-SAT problem is defined by a formula, \(\varphi\), over a set of boolean variables, \(X = \{x_1, x_2, \ldots, x_n\}\). A formula is said to be satisfiable if there exists an assignment of truth values (TRUE or FALSE) to \(X\) such that the formula evaluates to TRUE. A SAT formula, \(\varphi\), is typically given in Conjunction Normal Form (CNF). A formula is considered to be CNF if it is a conjunction (logical AND, \(\land\)) of clauses,

\[\varphi = C_i \land C_{i+1} \land \ldots \land C_m,\]

where each clause \(C_i\) is a disjunction (logical OR, \(\lor\)) of at most three literals. A literal is either a variable \(x_j\) or its negation \(\neg x_j\). Concretely,

\[C_i = (l_{i1} \lor l_{i2} \lor l_{i3})\]

The 3-SAT problem asks whether there exists an assignment of truth values (True or False) to the variables \(x_1, x_2, \ldots, x_n\) such that the entire formula \(\varphi\) evaluates to True. When such an assignment exists, the formula is said to be satisfiable.

Parameters:

clauseslist: A list of clauses in conjunctive normal form.

Attributes:

formulastr: The formula of the problem.

Methods

`from_dimacs`(path)	Load a SAT instance from a DIMACS file.
`reconstruct`(solution)	Reconstruct the solution.
`reduce`(target)	Reduce the problem to a specified target problem.
`solve`()	Solve the problem instance.