Boolean Ring Satisfiability

We propose a method for testing satisfiability based on Boolean rings. It makes heavy use of simplification, but avoids the potential size increase associated with application of the distributive law by employing a combined linear and binomial representation. Several complexity results suggest why the method may be relatively effective in many cases. The framework is also amenable to learning from intersections, as in Stålmarck’s method. Some experiments have been undertaken.

Authors

• Nachum Dershowitz
• Jieh Hsiang
• Guan-Shieng Huang
• Daher Kaiss

Keywords

No keywords are indexed for this paper.