"""Authored small CNF DPLL: signed integer literals, real backtrack and truth-table oracle."""
import itertools,json

def solve(clauses):
    if any(type(x)is not int or x==0 or abs(x)>8 for c in clauses for x in c):raise ValueError('nonzero signed literals 1..8 required')
    names=sorted({abs(x)for c in clauses for x in c});trace=[]
    def search(model,depth):
        remaining=[]
        for clause in clauses:
            if any(abs(x)in model and model[abs(x)]==(x>0)for x in clause):continue
            unknown=[x for x in clause if abs(x)not in model]
            if not unknown:trace.append({'event':'conflict_empty_clause','depth':depth,'model':model.copy(),'clause':clause});return None
            remaining.append(unknown)
        if not remaining:
            complete={u:model.get(u,False)for u in names};trace.append({'event':'success_all_clauses','depth':depth,'model':complete.copy()});return complete
        unit=next((c[0]for c in remaining if len(c)==1),None)
        if unit is not None:
            nxt={**model,abs(unit):unit>0};trace.append({'event':'unit','depth':depth,'literal':unit});return search(nxt,depth)
        signs={u:{x>0 for c in remaining for x in c if abs(x)==u}for u in names if u not in model}
        pure=next((u for u in signs if len(signs[u])==1),None)
        if pure is not None:
            value=next(iter(signs[pure]));trace.append({'event':'pure','depth':depth,'variable':pure,'value':value});return search({**model,pure:value},depth)
        u=next(u for u in names if u not in model)
        for value in [True,False]:
            trace.append({'event':'branch','depth':depth,'variable':u,'value':value});ans=search({**model,u:value},depth+1)
            if ans is not None:return ans
            trace.append({'event':'backtrack','depth':depth,'variable':u,'rejected_value':value})
        return None
    ans=search({},0)
    if ans is not None:assert all(any(ans[abs(x)]==(x>0)for x in c)for c in clauses)
    return {'clauses':clauses,'satisfiable':ans is not None,'assignment':ans,'trace':trace}

def oracle(clauses):
    names=sorted({abs(x)for c in clauses for x in c})
    return [dict(zip(names,values))for values in itertools.product([False,True],repeat=len(names)) if all(any(dict(zip(names,values))[abs(x)]==(x>0)for x in c)for c in clauses)]

def demo():
    sat=[[1,2],[-1,2],[-1,-2]];unsat=sat+[[1,-2]];a=solve(sat);b=solve(unsat);oa=oracle(sat);ob=oracle(unsat)
    assert a['assignment']=={1:False,2:True} and oa==[a['assignment']] and b['assignment']is None and not ob
    assert any(x['event']=='backtrack'and x['variable']==1 and x['rejected_value']for x in a['trace'])
    assert any(x['event']=='unit'for x in a['trace'])
    pure=solve([[1,2],[-1,2]]);assert pure['satisfiable']and any(x['event']=='pure'for x in pure['trace'])
    empty=solve([]);empty_clause=solve([[]]);assert empty['satisfiable']and empty['assignment']=={} and not empty_clause['satisfiable']
    try:solve([[0]])
    except ValueError:invalid=True
    else:raise AssertionError('zero is not a literal')
    return {'variable_names':{'1':'A','2':'B'},'authored_sat_example':a,'independent_all_four_assignments_sat_solutions':oa,'authored_unsat_example':b,'independent_all_four_assignments_unsat_solutions':ob,'pure_literal_case':pure,'empty_conjunction':empty,'contains_empty_clause':empty_clause,'zero_literal_rejected':invalid,'external_sat_solver_or_language_model_executed':False}

if __name__=='__main__':print(json.dumps(demo(),indent=2))