Skip to main content
Theoretical Computer Science

Return to Question

replaced http://cstheory.stackexchange.com/ with https://cstheory.stackexchange.com/
Source Link
Community Bot
Community Bot
  • 1

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 answeranother 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.)

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.)

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.)

Tweeted twitter.com/#!/StackCSTheory/status/472327162935005184
Source Link
mrsteve
mrsteve
  • 443
  • 2
  • 12

Remove unneeded atoms in CNF minimalization (SAT preprocessing)

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.)