CODEWITHSUNDEEP
constraint-programmingsatisfiabilityoperations-research
Albert Hendriks
Albert Hendriks

Reputation: 2142

real world SAT instances

I'm designing and implementing a SAT solver. It would be particularly good if all clauses are of the form

a AND b = c
a OR b = c
a XOR b = c
a = NOT b

In literature they use CNF form, which is I think would be a less efficient representation of the original real world problem in practice. They do that because existing SAT solvers can handle CNF better. This would not hold for my SAT solver however, which would cause an unfair disadvantage for me. Is anybody aware of any real world instances in the above form?

Upvotes: 1

Views: 936

Answers (2)

CliffordVienna
CliffordVienna

Reputation: 8255

The theory and application of SAT solvers is very tightly coupled to the CNF representation. If your solver is using boolean formulas instead of CNF you might want to think about your solver not as a "SAT solver" but as an "SMT solver with no support for theories except quantifier free first-order logic".

Many SMT solvers support SMT-LIBv2 as input language. In SMT-LIB the feature-set of the solver is configured by setting a "logic" using the set-logic statement. The QF_UF logic only supports basic quantifier free boolean formulas and should be equivalent to what you want. E.g. your example clauses in SMT-LIB syntax:

(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (= (and a b) c))
(assert (= (or a b) c))
(assert (= (xor a b) c))
(assert (= a (not b)))
(check-sat)
(exit)

Which will print unsat when passed to an SMT solver.

The SMT-LIB QF_UF benchmark contains a large collection of problems in this fomat (6647 "crafted" and 3 "industrial"):

The SMT competitions are divided in logic divisions. So it is possible to enter a solver in a competition that only supports QF_UF. (In fact, the OpenSMT2 solver only supports QF_UF and participated in the SMT-COMP 2014.)

Upvotes: 2

Axel Kemper
Axel Kemper

Reputation: 11332

You raise a valid point. Peter Stuckey had a presentation "There Are No CNF Problems" on the SAT Conference 2013. You'll find the slides here.

For practical applications it would be nice to have a high-level problem description language like Stuckey's MiniZinc. Encoding the problem in CNF is all too often tedious and error-prone.

To answer your question:
Yes, most real-world problems are described as Boolean or mathematical expressions rather than as CNF. An encoding step is needed to let them be solved by some solver.

There are a lot solver "schools" on the scientific market to make the problem encoding less problematic. Examples are Answer Set Programming (ASP) like Gringo/Clasp and Constraint Programming Solvers (CSP) like MiniZinc.

Another option is to use "Circuit-SAT" rather than CNF-SAT. A "circuit" is described in terms of logical gates and connections between them. That is a sort of nested system of Boolean expressions. My favorite tool to translate circuits to CNF is bc2cnf.

There are some good points to mention about CNF:

  1. CNF (in DIMACS format) can be handled by many tools
  2. CNF is rather compact
  3. CNF can be parsed very easily

Upvotes: 3

Related Questions