Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2015 | 10.1016/j.entcs.2015.06.003 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
#SAT,#FAL,Binary Patterns,Enumerative Combinatorics | #SAT,Discrete mathematics,Combinatorics,Enumerative combinatorics,Deterministic algorithm,Time complexity,Mathematics,Binary number | Journal |
Volume | Issue | ISSN |
315 | C | 1571-0661 |
Citations | PageRank | References |
1 | 0.36 | 9 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Guillermo De Ita Luna | 1 | 29 | 16.57 |
José Raymundo Marcial-Romero | 2 | 5 | 12.87 |
Pilar Pozos Parra | 3 | 69 | 11.08 |
José A. Hernández | 4 | 1 | 0.70 |