Dependent and Independent Variables in Propositional Satisfiability

摘要: Propositional reasoning (SAT) is central in many applications of Computer Science. Several decision procedures for SAT have been proposed, along with optimizations and heuristics to speed them up. Currently, the most effective implementations are based on Davis, Logemann, Loveland method. In this method, input formula represented as a set clauses, space truth assignments searched by iteratively assigning literal until all clauses satisfied, or clause violated backtracking occurs. Once new assigned, pruning techniques (e.g., unit propagation) used cut search inferring values other variables.In paper, we investigate "independent variable selection (IVS) heuristic", i.e., given variables N, restricted - possibly small subset S which sufficient determine value N. During phase, scoring assign next S, remaining determined solver. We discuss possible advantages disadvantages IVS heuristic. Our experimental analysis shows that obtaining either positive negative results strictly depends type problems considered, underlying technique, also scheme.