SAT'05 COMPETITION: BENCHMARK SUBMISSION CONTACT AUTHOR: Matti J\"arvisalo, matti.jarvisalo@tkk.fi BRIEF DESCRIPTION: Very small but hard instances based on linear equations modulo 2 where the underlying structure is derived from 3-regular graphs. Both random bipartite graphs and small graphs with large girth (cages) are used. So-called "camouflaged" versions of the instances are also provided; the camouflage fools equivalence reasoners. Both unsatisfiable and satisfiable instances are provided. For the satisfiable instances, a satisfying truth assignment is included in the cnf-file as comments. Use hjkn-mod2/perl/checkmodel.pl to confirm the included satisfying truth assignments. See description in hjkn-mod-2/description.pdf for details on the constructions and some experimental results. NOTE: mod2-3cage & mod2-3g14 (mod2c-3cage & mod2c-3g14 for equivalence reasoners) are the hardest considering the number of variables; if all instances are not used, we recommend using them. Please notice, however, that also rand instances seem considerably hard considering their size. DESCRIPTIONS OF BENCHMARKS/SUBDIRECTORIES: Satisfiable Instances --------------------- hjkn-mod2/mod2-rand3bip-sat/ Files: mod2-rand3bip-sat--.cnf Satisfiable instances with the number of variables = 200,210,...,300. For each there are 15 instances numbered by = 1,...,15 Underlying graphs are random 3-regular bipartite graphs. hjkn-mod2/mod2c-rand3bip-sat/ Files: mod2c-rand3bip-sat--.cnf As mod2-rand3bip-sat/ but with "simple camouflage" applied on the instances; see HJKN.hard.pdf for details. Due to camouflage, the number of variables in the instances is somewhat greater than = 150,160,...,250. The camouflage fools equivalence reasoners. hjkn-mod2/mod2-3g14-sat/ File: mod2-3g14-sat.cnf A satisfiable instance with 192 variables. The underlying graph is the smallest known 3-regular graph with girth 14. hjkn-mod2/mod2c-3g14-sat/ File: mod2c-3g14-sat.cnf As mod2-3g14-sat/ but with "simple camouflage" applied on the instance; see HJKN.hard.pdf for details. The number of variables is 266. The camouflage fools equivalence reasoners. Unsatisfiable Instances ----------------------- hjkn-mod2/mod2-rand3bip-unsat/ Files: mod2-rand3bip-unsat--.cnf Unsatisfiable instances with the number of variables = 90,105,120,135,150. For each there are 15 instances numbered by = 1,...,15. Underlying graphs are random 3-regular bipartite graphs. hjkn-mod2/mod2c-rand3bip-unsat/ Files: mod2c-rand3bip-unsat--.cnf As mod2-rand3bip-unsat/ but with "simple camouflage" applied on the instances; see HJKN.hard.pdf for details. Due to camouflage, the number of variables in the instances is somewhat greater than . The camouflage fools equivalence reasoners. hjkn-mod2/mod2-3cage-unsat/ Files: mod2-3cage-unsat--.cnf Underlying graphs are (3,)-cages with girth \in 9,10,11,12. 18 (3,9)-cages, 3 (3,10)-cages, 1 (3,11)-cages, and 1 (3,12)-cage exist. hjkn-mod2/mod2c-3cage-unsat/ Files: mod2c-3cage-unsat--.cnf As mod2-3cage-unsat/ but with "simple camouflage" applied on the instances; see HJKN.hard.pdf for details. The camouflage fools equivalence reasoners.