1
$\begingroup$

Modern CDCL SAT solvers often can return partial assignments where missing literals mean that the value of that variable is not important for the satisfaction of the formula (i.e. it is a don't care).

What I can't understand is which guarantee do I have that such don't cares are identified.

So, are state-of-the-art solvers (e.g. CryptoMiniSAT or Glucose or whatever) always able to identify the don't cares and give me a partial assignment instead of a single specific one, or how can they be used to obtain that?

$\endgroup$
1
  • $\begingroup$ I think they return the result as soon as (if that happens) all clauses are satisfied, so if a partial assignment $p(X)\land y$ and $p(X)\land\overline y$ both are satisfying, I think it would always return just $p(X)$. That does not guarantee that you get the smallest satisfying partial assignment though. $\endgroup$
    – rus9384
    Commented Jul 8, 2023 at 18:04

1 Answer 1

2
$\begingroup$

State-of-the-art CDCL SAT solvers typically use sophisticated algorithms and techniques to identify and return partial assignments with don't cares. These solvers are designed to maximize their efficiency in identifying the don't care assignments to minimize the amount of time it takes to solve a problem. Depending on the solver, users can configure certain parameters that impact the solver's ability to identify don't cares. By tweaking these parameters, users can increase the likelihood that the solver will return a partial assignment with don't cares.

$\endgroup$
3
  • $\begingroup$ Many thanks! Is there any resource to learn about those techniques? $\endgroup$ Commented Mar 24, 2023 at 11:48
  • $\begingroup$ @gigabytes Short answer: Any variables that didn't require an assignment to satisfy all clauses are "don't cares", and any others can be tested, but they do need to be tested somewhat sequentially. In a clause like $A \vee B$, you could have $A$ true and $B$ don't care, or $A$ don't care and $B$ true, and the clause would be satisfied. But they can't both be don't care. $\endgroup$
    – Pseudonym
    Commented Mar 26, 2023 at 1:13
  • 1
    $\begingroup$ Hi @Pseudonym, thanks. Sure, variables that are not touched during the search are don't care, but you may be unlucky and start the search by choosing a variable that is not relevant after all. So it seems CDCL solvers can often come up with some don't cares, but finding a minimal assignment is hard (coNP-hard, I think). $\endgroup$ Commented Mar 27, 2023 at 2:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.