4
$\begingroup$

This might be a very basic question.

I am interested in all atoms of a propositional formula that can be removed from a particular formula, while the derived formula has the same satisfiability characteristics.

Consider:

$(\lnot a\lor b) \land (a \lor b)$

Here the atom a can be removed, as the formula can be reduced to simply b.

Is there a name for atoms that can be removed from a formula? I.e., atoms like a that can be removed from a formula? (Informally I would call them "don't care" atoms.)

There are certain tools like lingeling and minisat2 that can simplify or preprocess a SAT problem, given a CNF formula (see another answer). Do this approaches reliably remove all atoms (like aabove) from the formula that can be removed? My rough guess would be that finding a minified formula is as complex as finding all the prime implicants of a formula? (Minification in my sense would be a formula with the least number of atoms.)

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ Using resolution, all atoms (variables) appearing as both positive and negated literals can be removed from a propositional formula and leave it equisatisfiable. So for your question to have meaning a restriction needs to be added, such as not increasing the number of CNF clauses (assuming CNF is being used). AFAIK, there is no name for such variables and minisat makes no guarantee that it will remove all that are possible to remove. $\endgroup$
    – Kyle Jones
    Commented May 26, 2014 at 2:51

3 Answers 3

Reset to default
4
$\begingroup$

As Kyle Jones has mentioned, the example you provided is called (restricted) resolution.

Beside that, pure literals can also be safely removed from a SAT problem. Unit clauses can be assigned a truth value. Check this paper:

The Puzzling Role of Simplification in Propositional Satisfiability. Inês Lynce and João Marques-Silva.

It discusses several preprocessing techniques for SAT, and its experiments showed that applying preprocessing for SAT leads to mix results. However, this paper might not be state-of-the-art.

Improve this answer
$\endgroup$
1
$\begingroup$

These things are called variable and literal (in)dependence. To check that a literal/variable is dependent is in NP [1].

[1] Propositional Independence - Formula-Variable Independence and Forgetting. available at arxiv

Improve this answer
$\endgroup$
0
$\begingroup$

(extended comment) the "preprocessing" you mention is covered by several standard algorithms. see unit propagation/pure literal elimination in DPLL algorithm & the Quine-Mccluskey CNF minimization algorithm (somewhat more studied in EE context than CS) where pairs of minterms with Hamming distance 1 are combined to find prime implicants. next, essential prime implicants are found. however finding essential prime implicants in the latter algorithm leads to another NP complete minimum set cover problem. most SAT solvers use heuristics for the CNF preprocessing/minimization although some implement the complete/optimal Quine-Mcclusky minimization on demand, which can succeed only for small formulas—the enumeration of all prime implicants can result in "exponential blowup" in size.

see also Shortest Equivalent CNF Formula tcs.se which has refs & defines its complexity class etc.

Improve this answer
$\endgroup$

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.