Boolean Satisfiability

The Satisfiability Problem in propositional logic (SAT) is the quintessential NP-Complete problem. Hundreds of academic and industrial researchers are actively working on SAT algorithms (SAT-Solvers), and thousands of articles have been published to date. Over the past decade dramatic improvements in SAT research has given rise to SAT-Solvers that can solve industrial problems.

SAT-solving is now a commercially valuable and competitive activity, with widespread interest in academia and a growing user base in multiple industries. SAT-solvers are a disruptive technology, often delivering orders of magnitude speedup over traditional algorithms.

Propositional Formulae

Given a propositional formula on a set of Boolean variables, SAT asks whether or not there exists an assignment to the set of variables such that the formula evaluates to True. More specifically, SAT, in Conjunctive Normal Form (CNF), consists of the conjunction of a number of clauses, where a clause is a disjunction of a number of propositions or their negations. Given a set of clauses {C₀, C₀,..., C_m-1} on the propositions {x₀, x₁,.., x_n-1}, the problem is to determine whether the formula F = ∀_{j < m} C_j has an assignment of values to the propositions such that it evaluates to True.

Many optimization problems can be formulated as propositional formulae. The standard format is DIMACS CNF.  Satalia provides a wide range of products and services to help you represent your optimization problems as CNF. This means you are able to utilize the disruptive power of SAT-solvers and the Satalia SolveEngine.

DIMACS CNF Format

The DIMACS CNF format is a standard way to represent conjunctive normal form boolean formulae. Below are some basic examples.

Satalia solves SAT problems represented in DIMACS CNF format. Simply upload your SAT problems to our SolveEngine using our API or Web-Poral, and let Satalia do the solving.

All SAT instances submitted must be in DIMACS CNF Format and have the '.cnf' file extension.

To represent an instance of CNF problems, DIMACS has suggested a file format that contains all of the information needed to define a satisfiability problem. This should be an ASCII file consisting of a two major sections: the preamble and the clauses.

• Preamble: The preamble contains information about the instance. This information is contained in lines. Each line begins with a single character (followed by a space) that determines the type of line. The type of lines are as follows:

  • Comments: Comment lines give human-readable information about the file and are ignored by programs. Comment lines appear at the beginning of the preamble. Each comment line begins with a lower-case character 'c'

    c This is an example of a comment line.

  • Problem line: There is one problem line per input file. The problem line must appear before any node or arc descriptor lines. For CNF instances, the problem line has the format p FORMAT VARIABLES CLAUSES. The lower-case character 'p' signifies that this is the problem line. The FORMAT field allows programs to determine the format that will be expected, and should contain the word 'cnf'. The VARIABLES field contains an integer value specifying n, the number of variables in the instance. The CLAUSES field contains an integer value specifying m, the number of clauses in the instance. This line must occur as the last line of the preamble. The problem line of an instance that has 10 variables and 25 clauses would be

    p cnf 10 25

• Clauses: The clauses appear immediately after the problem line. The variables are assumed to be numbered from 1 up to n. It is not necessary that every variable appear in an instance. Each clause will be represented by a sequence of numbers, each separated by either a space, a tab, or a new line character. The non-negated version of a variable i is represented by i; the negated version is represented by -i.

  Each clause is terminated by the value 0. Unlike many formats that represent the end of a clause by a new-line character, this format allows clauses to be on multiple lines.

Using the example CNF formula:

(x1 ∨ x3 ∨ -x4) ∧ (x4) ∧ (x2 ∨ -x3)

A possible DIMACS formatteed input file would be:

c Example CNF format file
c 
p cnf 4 3
1 3 -4 0
4 0
2 -3 0

Another example

(x0 ∨ x1 ∨ x2) ∧ (-x0 ∨ x1 ∨ -x2) ∧ (x1 ∨ -x2 ∨ x3) ∧ (x0 ∨ -x1 ∨ x3) ∧ (-x0 ∨ -x2 ∨ -x3)

may look like:

c Another example CNF example.
c This is in 3CNF format.
c It has 3 literals per clause.
c 
p cnf 4 5
1 2 3 0
-1 2 -3 0
2 -3 4 0
1 -2 4 0
-1 -3 -4 0

Visit SATLIB and SAT-Competition for more information and access to a wide variety of SAT benchmark instances.