Do you think that it is possible to compile a propositional formula towards a SAT problem of similar size whose solution allows us to find a valuation which satisfies the starting formula? If so, explain the method you would use. Thanks in advance.
0
votes
1 Answers
0
votes
This questions seems to be already answered here: How to convert a propositional formula to conjunctive normal form (CNF)? SAT-solvers usually take a CNF in dimcas format as input.
