% The 2-inverter puzzle. % % The problem is to build a combinational circuit with 3 inputs % and 3 outputs, such that the outputs negate the inputs; we can % use as many AND and OR gates as we wish, but at most 2 NOT gates. % % The clause P(function, inversion_list) represents a wire, whose % state is a function of the inputs, and which depends on negated % wires listed in inversion_list. % % The initial clauses are % P(00001111, v). % input 1 % P(00110011, v). % input 2 % P(01010101, v). % input 3 % which represent the three input wires. The goal clause is % -P(11110000, v) | -P(11001100, v) | -P(10101010, v). % That is, the three output functions with unifiable inversion lists. % % The inversion lists are tricky: each has a variable as its tail, which % means that two lists unify iff on is an initial sublist of the other. % Two wires can be input to an OR or AND gate if their inversion lists % are unifiable. (Note this means that the second NOT gate must depend % on the first.) % % For example, P(01000110,[11111000,11001110|x]) means that we % can acheive the function 01000110 with a circuit in which 11111000 and % 11001110 are inverted. % % The following clause is placed on the passive list to subsume % circuits with 3 or more NOT gates. % P(x, [y1,y2,y3|y4]). % % If a proof is found, the corresponding circuit can be constructed by % going through the proof; each step represents a gate, and the parent % lists show how to connect the wires. % % The original formulation is by Steve Winker and is documented in % "Automated Reasoning: Introduction and Applications" by Wos et al. % This formulation does not use the "reversion" heuristic of Winker's % formulation. % % This takes about 40 minutes and about 6 megabytes on McCune's 486. % set(hyper_res). clear(back_sub). clear(demod_history). clear(print_kept). clear(print_given). assign(max_mem, 9000). assign(min_bit_width, 8). list(usable). % Rules for building circuits. -P(x, v) | -P(y, v) | P($BIT_AND(x,y), v). -P(x, v) | -P(y, v) | P($BIT_OR(x,y), v). -P(x, v) | P($BIT_AND(11111111,$BIT_NOT(x)), append_inversion(v,x)). end_of_list. list(sos). P(00001111, v). % input 1 P(00110011, v). % input 2 P(01010101, v). % input 3 end_of_list. list(usable). % Denial of the goal. -P(11110000, v) | -P(11001100, v) | -P(10101010, v). end_of_list. list(demodulators). % The following pair of demodulators inserts an element y just before the % tail-variable. append_inversion([x1|x2],y) = [x1|append_inversion(x2,y)]. $VAR(x) -> append_inversion(x,y) = [y|x]. end_of_list. list(passive). % The following clause subsumes functions obtained with 3 (or more) inversions. P(x, [y1,y2,y3|y4]). end_of_list. % The following list of weight templates gives first priority to the % goal functions, regardless of the inversion list. Recall that with % a multiliteral denial, all of the goals must be selected as given % clauses before a proof is found by hyper. Without these templates, % the three goals can sit on sos for a long time, delaying a proof. weight_list(pick_given). weight(P(11110000, $(1)), -50). weight(P(11001100, $(1)), -50). weight(P(10101010, $(1)), -50). end_of_list.