1
$\begingroup$

I have a very complicated formula logical (CNF) in the file DIMACS.

The question is as follows. The formula has hundreds of millions of clauses (assume billion) and a lot of variables.

It is a reconstruction of a logic circuit.

MiniSAT returns me the result for the SAT problem very quickly (a few seconds).

Can I increase the amount of input logic circuit but time solving logical formula does not increase exponentially. It increases very slowly (and sometimes completely not increasing).

Is there any ready-made software / scripts that can help me understand why the SAT solver solves the problem so quickly?

For example, if there is the software that the input file will DIMACS, and writes the output if the formula is P class (and at which the condition?) of Schaefer's theorem dichotomy?

Schaefer's theorem dichotomy conditions:

all relations which are not constantly false are true when all its arguments are true;

all relations which are not constantly false are true when all its arguments are false;

all relations are equivalent to a conjunction of binary clauses;

all relations are equivalent to a conjunction of Horn clauses;

all relations are equivalent to a conjunction of dual-Horn clauses;

all relations are equivalent to a conjunction of affine formulae.

$\endgroup$
3
  • 1
    $\begingroup$ Which formulas are hard is poorly understood AFAIK. You could examine MiniSATs code to see why it happens to be so fast for your input. $\endgroup$ – adrianN Jan 6 '17 at 11:52
  • $\begingroup$ What is the point of mentioning the file DIMACS if we have no access to it? Do you think that perhaps the name itself helps MiniSAT? $\endgroup$ – Yuval Filmus Jan 6 '17 at 14:49
  • 1
    $\begingroup$ As Yuval says, why DPLL and descendants perform well on some examples but not others, isn't really understood. Given that you are dealing with billions of clauses, maybe your formulae are far from the phase transition point, i.e. they have a lot more clauses than variables (hence are false with high probability) or have a lot more variables than clauses (hence are true with high probability). See e.g. theses slides or this video. $\endgroup$ – Martin Berger Jan 6 '17 at 15:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.