npycomp.problems.

SAT

class npycomp.problems.SAT(clauses: list)

A Boolean Satisfiability (SAT) problem.

A SAT Problem is a classical decision problem in computer science that asks whether there exists an assignment of variables that satisfies a given Boolean formula.

Formally, a 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 one or more literals. A literal is either a variable \(x_j\) or its negation \(\neg x_j\). Concretely,

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

The 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.