A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings

This paper proposes a new hybrid encoding of finite linear CSP to SAT integrating order and log encodings. The former maintains bound consistency by unit propagation and works well for instances with small/middle domain sized variables and/or arity of constraints. The latter generates smaller CNF and is suitable for instances with larger domain sized variables, but its performance is not good in general because more inference steps are required to ripple carries. This paper describes the first attempt of hybridizing the order and log encodings without channeling. Each variable is encoded by either the order encoding or the log encoding, and each constraint can contain both types of variables. We evaluate its performance with two benchmark sets. The first one consists of our handmade instances to verify the synergy effect of the hybridization. The second one consists of 1002 instances from the 2009 CSP solver competition to have a comprehensive evaluation on a wide variety of problems. The result shows the proposed hybrid encoding solves several instances which cannot be solved by both two encodings and its performance is superior to them.