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

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

<p><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.7.7458" rel="nofollow">The Puzzling Role of Simplification in Propositional Satisfiability</a>.  Inês Lynce and João Marques-Silva.</p>

<p>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.</p>

CC BY-SA 3.0
2014-05-26T23:12:57.730Z
2014-05-26T23:12:57.730Z
sean
<p>These things are called variable and literal (in)dependence. To check that a literal/variable is dependent is in NP [1].</p>

<p>[1] Propositional Independence - Formula-Variable Independence and Forgetting.
<a href="http://arxiv.org/abs/1106.4578" rel="nofollow">available at arxiv</a></p>

CC BY-SA 3.0
2014-05-27T16:53:20.180Z
2014-05-27T16:53:20.180Z
Mikolas
<p>(extended comment) the "preprocessing" you mention is covered by several standard algorithms. see <a href="http://en.wikipedia.org/wiki/DPLL_algorithm" rel="nofollow noreferrer">unit propagation/pure literal elimination in DPLL algorithm</a> &amp; the <a href="http://en.wikipedia.org/wiki/Quine_McCluskey" rel="nofollow noreferrer">Quine-Mccluskey CNF minimization algorithm</a> (somewhat more studied in EE context than CS) where pairs of minterms with Hamming distance 1 are combined to find prime implicants. next, <em>essential</em> prime implicants are found. however finding essential prime implicants in the latter algorithm leads to another NP complete minimum <a href="http://en.wikipedia.org/wiki/Set_cover_problem" rel="nofollow noreferrer">set cover</a> 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.</p>

<p>see also <a href="https://cstheory.stackexchange.com/questions/9839/shortest-equivalent-cnf-formula">Shortest Equivalent CNF Formula</a> tcs.se which has refs &amp; defines its complexity class etc.</p>

CC BY-SA 3.0
2014-05-29T15:05:46.300Z
2014-05-29T15:29:20.790Z
2017-04-13T12:32:28.117Z
vzn
<p>This might be a very basic question.</p>

<p>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.</p>

<p>Consider:</p>

<p>$(\lnot a\lor b) \land (a \lor b)$</p>

<p>Here the atom <code>a</code> can be removed, as the formula can be reduced to simply <code>b</code>.</p>

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

<p>There are certain tools like lingeling and minisat2 that can simplify or preprocess a SAT problem, given a CNF formula (see <a href="https://cstheory.stackexchange.com/questions/9839/shortest-equivalent-cnf-formula">another answer</a>). 
Do this approaches reliably remove all atoms (like <code>a</code>above) 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.)</p>

CC BY-SA 3.0
2014-05-26T02:51:18.277Z
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.
Kyle Jones
<time-complexity><sat><formulas><boolean-formulas>
Remove unneeded atoms in CNF minimalization (SAT preprocessing)
mrsteve
# Remove unneeded atoms in CNF minimalization (SAT preprocessing)

(Asked by: username_0 on 2014-05-25)

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](https://cstheory.stackexchange.com/questions/9839/shortest-equivalent-cnf-formula)).
Do this approaches reliably remove all atoms (like `a`above) 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.)

**Tags:** time-complexity, sat, formulas, boolean-formulas
> **Comments:**
> **username_1**: 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.  

---

## 3 answers

### Answer by username_2 on 2014-05-26. Score: 4

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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.7.7458). 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.


---

### Answer by username_3 on 2014-05-27. Score: 1

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](http://arxiv.org/abs/1106.4578)


---

### Answer by username_4 on 2014-05-29. Score: 0

(extended comment) the "preprocessing" you mention is covered by several standard algorithms. see [unit propagation/pure literal elimination in DPLL algorithm](http://en.wikipedia.org/wiki/DPLL_algorithm) & the [Quine-Mccluskey CNF minimization algorithm](http://en.wikipedia.org/wiki/Quine_McCluskey) (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](http://en.wikipedia.org/wiki/Set_cover_problem) 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](https://cstheory.stackexchange.com/questions/9839/shortest-equivalent-cnf-formula) tcs.se which has refs & defines its complexity class etc.


---

