Using Binary Patterns for Counting Falsifying Assignments of Conjunctive Forms
Guillermo De Ita Luna, J. Raymundo Marcial‐Romero, Pilar Pozos-Parra, José Antonio Hernández Servín · Electronic Notes in Theoretical Computer Science · 2015
The representation of the set of falsifying assignments of clauses via binary patterns has been useful in the design of algorithms for solving #FAL (counting the number of falsifying assignments of conjunctive forms (CF)). Given as input a CF formula F expressed by m clauses defined over n variables, we present a deterministic algorithm for computing #FAL(F). Principally, our algorithm computes non-intersecting subsets of falsifying assignments of F until the space of falsifying assignments defined by F is covered. Due to #SAT(F) = 2n-#FAL(F), results about #FAL can be established dually for #SAT. The time complexity of our proposals for computing #FAL(F) is established according to the number of clauses and the number of variables of F.