Repair Exercise

13.6 Repair Exercise

Write a predicate min_conflicts(Vars,Count) that takes two arguments:

Vars - a list of variables, with tentative 0/1 values
Count - a variable, with a tentative integer value

The specification of min_conflicts(Vars,Count) is as follows:

If conflict set cs is empty, instantiate Vars to their tentative values
Otherwise find a variable, V, in a conflict constraint
Instantiate V to the value (0 or 1) that maximises the tentative value of Count
On backtracking instantiate V the other way.

This can be tested with the following propositional satisfiability program.

cons_clause(Clause,Bool) :-
    Clause =:= 1 r_conflict cs,
    Bool tent_is Clause.

prop_sat(Vars,List) :-
    ( foreach(N,List),
      foreach(Cl,Clauses),
      param(Vars)
    do
        cl(N,Vars,Cl)
    ),
    init_tent_values(Vars),
    ( foreach(Cl,Clauses), 
      foreach(B,Bools) 
    do 
      cons_clause(Cl,B)
    ),
    Count tent_is sum(Bools),
    min_conflicts(Vars,Count).

init_tent_values(Vars) :- 
    ( foreach(V,Vars) do V tent_set 1).

cl(1,[X,Y,Z], (X or neg Y or Z)).
cl(2,[X,Y,Z], (neg X or neg Y)).
cl(3,[X,Y,Z], (Y or neg Z)).
cl(4,[X,Y,Z], (X or neg Z)).
cl(5,[X,Y,Z], (Y or Z)).

To test your program try the following queries:

?- prop_sat([X,Y,Z],[1,2,3]).
?- prop_sat([X,Y,Z],[1,2,3,4]).
?- prop_sat([X,Y,Z],[1,2,3,4,5]).